Skip to content

Commit

Permalink
Merge #201
Browse files Browse the repository at this point in the history
201: Demodal deconstruction r=nikomatsakis a=nikomatsakis

I've been coming back to Dada a bit lately as I've been on vacation and had more time for hacking. Looking at it with fresh eyes, I didn't like the direction of having specifiers on local variables (e.g., `my x = ...`) and so I've been revamping it to go back to postfix keywords only. Hence instead of `my x = y` we have...

```
x = y.give
```

...the big change in this branch is that just writing `x = y` is equivalent to `x = y.share`, and that the `shlease` keyword is removing. Instead,  it is called `share`, but if you want to create an "our' value (joinly owned), you have to share a vallue, not a place. e.g., either `x = Point(22, 44).share` or `x = y.give.share`.

I'm still in the progress of reworking the tutorial and a few other things to match.

I want to work my way towards a sample application.


Co-authored-by: Niko Matsakis <[email protected]>
  • Loading branch information
bors[bot] and nikomatsakis authored Aug 1, 2022
2 parents d713452 + 5284b1d commit 36b611e
Show file tree
Hide file tree
Showing 314 changed files with 2,780 additions and 4,529 deletions.
4 changes: 2 additions & 2 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

75 changes: 30 additions & 45 deletions book/docs/dyn_tutorial/class.md
Original file line number Diff line number Diff line change
Expand Up @@ -11,70 +11,55 @@ import Caveat from '../caveat.md'
The main data structures in Dada are classes. The full class syntax has various bells and whistles, but let's start off with the simplest form. We'll define a class `Point` for storing `(x, y)` values. It will have two fields, `x` and `y`:

```
class Point(our x, our y)
# ^^^^^ ^^^ ^
# | | |
# | | Field name
# | Permission
class Point(x, y)
# ^^^^^ ^ ^
# | | |
# | | Field name
# | Field name
# Class name
```

## The `our` permission

You can see that the fields are declared with an *permission* -- `our` in this case. There are several permissions (`my`, `our`, `leased`, and `shleased`); these permissions are a key part of how Dada works, and we'll be covering them throughout this tutorial. For now, it's enough to say that an `our` field stores an object that may be referenced by other fields or variables as well (it belongs to everyone, hence `our`). For points, we are expecting to store integers like `22` and `44`, so this is a good fit.

## Constructor functions

The `class Point(..)` syntax also creates a constructor function that creates an instance of `Point` when called. Try executing the following code:
The `class Point(..)` syntax also creates a constructor function that creates an instance of `Point` when called. To get a feel for how classes work in practice, work with the following code. Feel free to make changes and see what happens! You'll also notice that when you move your cursor, the code executes up until the line you selected.

```
class Point(our x, our y)
```dada ide
class Point(x, y)
# This function is declared as `async` because it
# awaits the result of print.
async fn print_point(p) {
# Note that you can use `{...}` to embed an expression
# into the value of a string (in this case, the
# variable `p`).
print("The point is: {p}").await
}
# This function is not declared as `async` because it
# doesn't await anything. The `->` indicates that it
# returns a value.
# Declares a function that computes a new value.
# (It doesn't await anything, so the function is not `async`.)
fn compute_new_value() -> {
# ^^ this `->` indicates that
# the function returns a value.
33
}
my p = Point(22, 44)
# Writing `p = ...` declares a new variable `p`
# and assigns its initial value (`Point(22, 44)`)
p = Point(22, 44)
# Invoke `print_point`; it's an `async` function,
# so await the result
print_point(p).await
# The `:=` operator is used to modify an existing
# field (remember, `=` declares a new variable).
p.x := compute_new_value()
# You can also use `+=` to modify an existing field
# (this time by adding to it). Other operators, like
# `-=`, `*=`, `/=`, also work.
p.x += 1
print_point(p).await
# prints:
# The point is: Point(x: 22, y: 44)
# The point is: Point(x: 34, y: 44)
# Print the new value.
print_point(p).await
```

Some things to note here:

* Comments are written `#`, like Python or Ruby, not `//` like JavaScript or Rust.
* The `my p = ...` statement declares a local variable `p` using another permission, `my`.
* `my` declares a variable that has *unique* access to its object: in this case, we just created the `Point`, so nobody else could possibly be referencing it, so that makes sense. If that doesn't make sense yet, don't worry, we're going to talk all about `my` in the next section.
* You create a class by invoking its constructor function `Point(22, 44)`.
* Strings can embed expressions with `{}`, and they get "stringified", so `"The point is {p}"` embeds `p` into the string.
* The default stringifier prints the values of each field.
* You write `:=` to reassign variables or fields (just `=` is for declaring a new variable).
* You can also use the `+=`, `-=`, `*=`, `/=`, `%=` operators you may be familiar with from other languages.
* Declaring a function with `async fn` means that it can await thunks, like the one from calling `print`.
* Declaring a function with `->` means that it returns a value; as in Rust, the final expression in the function is its return value.
* In this case, `compute_new_value()` returns `33`.

## Summary and key differences

So far, everything hopefully feels fairly familiar, except for the [permissions](./permissions.md), which we'll cover next. Some highlights:

* Declaring a class like `class Point(x, y)` also gives a constructor function `Point` that can be called (e.g., `Point(22, 44)`) to create an instance of the class.
* You can use `"{p}"` in strings to print the values of things.
* Use `=` to declare a new variable and `:=` or `+=` to update an existing one.
* Dada is based on async-await:
* When you `print` something (or do any I/O), you must `await` the result for it to take effect (`print("Hi").await`).
* You can only `await` things from inside an `async` fn.
18 changes: 6 additions & 12 deletions book/docs/dyn_tutorial/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,25 +4,19 @@ import Caveat from '../caveat.md'

<Caveat/>

The classic “Hello, World” program in Dada should be quite familiar:
You can see a classic “Hello, World” program in Dada below; it should be quite familiar. Note that this is a live-editing IDE -- try editing the program to see the new output!

```dada ide
# Print a classic quote
print("
I have forced myself to contradict myself
in order to avoid conforming to my own taste.
-- Marcel Duchamp
").await
```

When you run this (try it!) it prints:
Some interesting things:

```
I have forced myself to contradict myself
in order to avoid conforming to my own taste.
-- Marcel Duchamp
```

There are a few interesting things to note:

* Dada, like JavaScript, is based exclusively on **async-await**. This means that operations that perform I/O, like `print`, don't execute immediately. Instead, they return a *thunk*, which is basically "code waiting to run" (but not running yet). The thunk doesn't execute until you *await* it by using the `.await` operation.
* Strings in Dada can spread over multiple lines. Leading and trailing whitespace is stripped by default, and we also remove any common indentation from each line.
- Comments in Dada are written with `#`, like Python or Ruby, not `//` like JavaScript or Rust.
- Dada, like JavaScript, is based exclusively on **async-await**. This means that operations that perform I/O, like `print`, don't execute immediately. Instead, they return a _thunk_, which is basically "code waiting to run" (but not running yet). The thunk doesn't execute until you _await_ it by using the `.await` operation.
- Strings in Dada can spread over multiple lines. Leading and trailing whitespace is stripped by default, and we also remove any common indentation from each line.
47 changes: 23 additions & 24 deletions book/docs/dyn_tutorial/labeled_arguments.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,50 +4,49 @@ sidebar_position: 3

# Aside: Labeled arguments

Before we go further with the tutorial, it's worth nothing that Dada supports *labeled arguments*. That means that instead of writing `Point(22, 44)` one can also give labels to each argument, like `Point(x: 22, y: 44)`:
Before we go further with the tutorial, it's worth noting that Dada supports _labeled arguments_. That means that instead of writing `Point(22, 44)` one can also give labels to each argument, like `Point(x: 22, y: 44)`:

```
class Point(our x, our y)
```dada ide
class Point(x, y)
my p = Point(x: 22, y: 44)
print("The point is `{p}`").await
# prints:
# The point is `Point(x: 22, y: 44)`
```

Try changing the code above to give the parameters in another orde, such as `Point(y: 44, x: 22)` -- you will see that the output doesn't change.

Adding labels can help make it clearer what is going on. The rules are as follows:

* You must also give the arguments in the order in which they were declared in the function, whether or not labels were provided.
* Once you give a label to a parameter, you must give a label to all the remaining parameters (so you can't do `Point(x: 22, yy)` but you can do `Point(22, y: 44)`.
- You must also give the arguments in the order in which they were declared in the function, whether or not labels were provided.
- Once you give a label to a parameter, you must give a label to all the remaining parameters (so you can't do `Point(x: 22, yy)` but you can do `Point(22, y: 44)`.

Dada will also sometimes suggest you use labels if it thinks you might be making a mistake. For example, try this:

```
class Point(our x, our y)
```dada ide
class Point(x, y)
async fn print_line(my start, my end) {
print(start).await
print(end).await
async fn print_line(start, end) {
print("The start is {start}").await
print("The end is {end}").await
}
my start = Point(22, 44)
my end = Point(33, 55)
start = Point(22, 44)
end = Point(33, 55)
print_line(end, start).await
# ~~~~~~~~~~ warning: are these parameters in the right order?
```

See the squiggly line? That is Dada telling us that we may have reversed the order of `end` and `start`. We can disable this warning by giving explicit labels to the arguments, making it clear that we *meant* to switch the order:
See the squiggly line? That is Dada telling us that we may have reversed the order of `end` and `start`. We can disable this warning by giving explicit labels to the arguments, making it clear that we _meant_ to switch the order:

```
class Point(our x, our y)
```dada ide
class Point(x, y)
async fn print_line(my start, my end) {
print(start).await
print(end).await
async fn print_line(start, end) {
print("The start is {start}").await
print("The end is {end}").await
}
my start = Point(22, 44)
my end = Point(33, 55)
start = Point(22, 44)
end = Point(33, 55)
print_line(start: end, end: start).await
```
```
71 changes: 42 additions & 29 deletions book/docs/dyn_tutorial/permissions.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,45 +4,58 @@ sidebar_position: 4

# Permissions

In the previous chapter, we saw keywords like `my` and `our` attached to variables. These are examples of **permissions** -- permissions are a key part of Dada. Like Rust, Dada leverages permissions to avoid the need for a garbage collector, while retaining memory safety.
Dada hopefully feels familiar to you thus far, but if you played a lot with the programs, you may have noticed some errors you didn't expect. Consider this program...what do you expect it to print? Take a guess, and then hit the "Run" button to see what happens...

## Running example

As we explain permissions both here and over the next several chapters, we're going to work with variations on this example program. It builds on syntax that we [introduced previously](./class.md), so if anything is confusing you may want to check out that chapter.
```dada ide
class Point(x, y)
p = Point(22, 44)
q = p
q.x := 23
print(p).await
```
class Point(our x, our y)

async fn main() {
my p = Point(22, 44)
print("The point is ({p.x}, {p.y})").await
}
```
Surprise! It gets an error! What is going on? The answer lies in the key Dada concept of **permissions**.

## What is a permission?

## `my`, `our`, and other permissions
In Dada, variables don't just store a reference to an object, like they do in Python or Java. Instead, they store a reference to an object _with some permission_. These permissions determine whether you can read or write to the object.

This example already makes use of two permissions, `my` and `our`. There are four permissions in total, and they can be divided along two dimensions:
Permissions in Dada can be divided across two axes. We'll cover those two axes separately:

| | Unique | Shared |
| ------ | ---------- | ------------ |
| Owned | [`my`] | [`our`] |
| Leased | [`leased`] | [`shleased`] |
- **Read** vs **write** -- covered now!
- **Owned** vs **leased** -- covered later, in the chapters on ownership

The difference between these dimensions:
## Read permission is the default

* *Owned* permissions are permanent. They cannot be revoked through access to other variables.
* *Leased* permissions are temporary -- there is always a lessor (either an owner or another lease), and that lessor can reclaim full access to their object.
* *Unique* permissions are exclusive. When one variable has unique permission, no other variables can access the object while that variable is in use (without some kind of error occurring).
* *Shared* permissions can be copied freely, but they [require that the object is read-only](./sharing_xor_mutation.md). In other words, while you are reading from an object with a shared permission, nobody else can come and change it under your feet (except via an [atomic](./atomic.md) field).
When you write something like `q = p` in Dada, the default is that you get a **leased, read permission**. Leasing will be covered in more detail later, but for now it suffices to say that the permission for `q` is tied to the permission from `p`; when `p` goes out of scope, for example, then `q`'s permission will also be canceled.

## Overview of what's to come
As the name suggests, **read permissions** can only be used to read fields. This is why we get an error!

Over the next few chapters, we're going to look at each of the permissions in detail:
Dada comes equipped with a visual debugger that lets you visualize permissions. To see how it works, try hitting the "Debug" button and then position your cursor write after the line for `q = p`:

* We'll start with the *owned permissions*, [`my`] and [`our`].
* Then we'll cover the *leased permissions*, [`leased`] and [`shleased`].
```dada ide
class Point(x, y)
p = Point(22, 44)
q = p
# ▲
# ───┘
# put your cursor here -- you will see a diagram below
# that shows that while `p` and `q` reference the same
# point, `q` has read permisions (indicated with a blue
# line).
```

[`my`]: ./my
[`our`]: ./our
[`leased`]: ./lease
[`shleased`]: ./shlease
## Requesting write permission

You can explicitly request write permision by using the `lease` keyword, like `p.lease`. If you use the debugger and position it after `q = p.lease`, you will see that `q` is given write permission this time. As a result, `q.x := 23` succeeds and, when we print the variable `p`, we see the new value.

```dada ide
class Point(x, y)
p = Point(22, 44)
q = p.lease
q.x := 23
print(p).await
```
4 changes: 2 additions & 2 deletions book/src/components/Ide/editor.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ import React, { PropsWithChildren } from "react";
import AceEditor from "react-ace";
import { useColorMode } from "@docusaurus/theme-common";

import "ace-builds/src-noconflict/mode-rust";
import "ace-builds/src-noconflict/mode-python";
import "ace-builds/src-noconflict/theme-github";
import "ace-builds/src-noconflict/theme-twilight";

Expand All @@ -20,7 +20,7 @@ function Editor(props: PropsWithChildren<OutputProps>) {
const { colorMode } = useColorMode();
return (
<AceEditor
mode="rust"
mode="python" // need a dada mode!
editorProps={{ $blockScrolling: true }}
fontSize={18}
width="100%"
Expand Down
Loading

0 comments on commit 36b611e

Please sign in to comment.