Welcome

What the heck is Dada?

Dada is a thought experiment. What if we were making a language like Rust, but one that was meant to feel more like Java or JavaScript, and less like C++? One that didn't aspire to being used in kernels or tiny embedded devices and was willing to require a minimal runtime. What might that look like?

What is the state of Dada?

As of right now, Dada doesn't really exist, though we have some experimental prototypes:

There is an experimental operational semantics implemented in PLT Redex, which you can find at dada-lang/dada-model. More details are available (or will be eventually) in the calculus section of this site.
The interpreter, written in Rust, is found on the dada-lang/dada repository. You can try a WebAssembly-based build on the Dada playground. More details are available in the "Development Guide" section of this site.

OK, from here on out I'm going to pretend that Dada really exists in its full glory.

Dada in a nutshell

Dada is an ownership-based language that is in some ways similar to Rust:

Like Rust, Dada doesn't require a garbage collector.
Like Rust, Dada guarantees memory safety and data-race freedom.
Like Rust, Dada data structures can be allocated in the stack and use flat memory layouts.

In other ways, though, Dada is very different:

Like TypeScript, Dada is a gradually typed language:
- That means you can start out using Dada in the interpreter, with no type annotations, to get a feel for how it works.
- Once you've gotten comfortable with it, you can add type annotations and use the compiler for performance comparable to Rust.
Dada targets WebAssembly first and foremost:
- You can build native targets with Dada, but its FFI system is based on WebAssembly interface types.
Dada is object-oriented, though not in a purist way:
- Dada combines OO with nice features like pattern matching, taking inspiration from languages like Scala.

Dada also has some limitations compared to Rust:

Dada has a required runtime and does not target "bare metal systems" or kernels.
Dada does not support inline assembly or arbitrary unsafe code.

Curious to learn more?

Check out one of our tutorials:

Footnotes

Updated to use modern pronouns.

Goals

These are the things Dada is trying for.

Easy to learn, but not dumbed down

Dada is meant to be a language that experts want to use. It should be easy to learn, but it doesn't achieve that by hiding important concepts like ownership and borrowing. Rather, it brings them to the fore, but in a packaging that is (hopefully) easy to learn.

Does the right thing, not everything

Dada doesn't attempt to do everything. It's not really meant to run on a tiny sensor node, for example, and nobody is going to to put it in a kernel anytime soon. But it aims to expose the right things that most people building complex software really need. In other words, you can't always do what you want, but if you try sometimes, with Dada, you can do what you need.

Opinionated (in a good way)

Going along with the previous point, Dada is not afraid to make some choices on your behalf. For example, it has a builtin smart pointer type (the box) that supports both unique ownership and reference counting. It includes builtin support for vector and hashmap types as well.

Predictable and reasonably efficient

Dada's performance doesn't have to be micro-efficient, but it must be predictable. It's ok to call malloc, but not to run a garbage collector, which introduces variable latency. It should also be possible to learn the rules for when malloc will be called and to control that if you choose.

Fun, lightweight, and familiar

Coding in Dada should feel pretty similar to coding in JavaScript, Python, Ruby, or Go, at least a lot of the time.

Design principles

Some key design principles intended to create the above experience.

Type erasure

Dada's type system is meant to be "fully erasable", similar to the relationship between TypeScript and JavaScript. That is, given some Typed Dada program, you should be able to delete all the type annotations and have it run in exactly the same way in Dynamic Dada. Any type errors should manifest as runtime exceptions at some point.

(Caveat: we may want to use function parameter types as "hints", in which case the correct erasure would include applying those hints. Have to see.)

Values, not places or pointers

Like Java or Python, Dada encourages programmers just to think about the values they are working with. Dada doesn't have pointer types like * or & nor a "dereference" operator like *. Even though Dada doesn't require a GC, it's meant to encourage familiar, GC-like patterns. If you were to remove all of Dada's sharing and ownership annotations, the result should be a program that could run just fine with a GC, with the expected semantics.

RAII is for releasing resources, not side effects

Dada has destructors, but they are not expected to have side-effects apart from releasing resources. The Dada compiler is always free to drop values even before the variable that owns them has gone out of scope. So, things like freeing memory, closing files, database handles, and sockets? Perfect. Printing data onto the console or sending a message over the wire? Not so good.

Dada shares Rust's obsession with exposing sharing (aliasing) and mutability, but not both at the same time.

Longer term goals

Rust interop

We dream of the day that Dada programs interop smoothly with Rust and can (e.g.) live happily in crates.io. However, that's not something that we're currently focusing on, since we're still playing with the basic structure of Dada. Once we figure out what Dada wants to be, we can figure out how to connect that with Rust (which could involve proposing changes to Rust, if we find patterns in Dada that would be a nice fit). Another path that may be worth considering is leaning heavily on WebAssembly and Interface Types for interoperability, in which case it would work smoothly across not only Rust but all languages that compile to WebAssembly. (These things are not exclusive.)

Tutorial: Dynamic dada

Gradual ownership

Dada is a gradual, ownership-based language. Let's unpack those two things:

Ownership-based: Dada leverages the concept of ownership to ensure that (a) your memory is freed at the right times, without any garbage collection and (b) your parallel programs are data-race free.
- If you've used Rust, Dada's ownership system will be familiar, but keep in mind that there are some key differences between them. (If you've not used Rust, don't worry, we don't assume any prior knowledge in this tutorial.)
Gradual: Dada lets you smoothly transition from an interpreted, dynamic language (similar to Python or JavaScript) over to a statically typed, fully optimized one (similar to Rust). You can even mix code written in the two styles.

This tutorial covers the dynamic flavor of Dada and use that to introduce the concepts of ownership and the like. Once you've gotten familiar to that, the Typed Dada introduces Dada's type system and shows how you can use it to check that your Dada code is free of permission-related errors.

Ready to read?

OK, turn to Hello, Dada! to begin!

Hello, Dada!

The classic “Hello, World” program in Dada should be quite familiar:

async fn main() {
    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:

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.

Declaring the `Point` class

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(x, y)
#     ^^^^^ ^
#       |   |
#       |   Field name
#       |
#     Class name

Constructor functions

The class Point(..) syntax also creates a constructor function that creates an instance of Point when called. Try executing the following code:

class Point(x, y)

async fn main() {
    p = Point(22, 44)
    print("The point is `{p}`").await
    print("The point is `({p.x}, {p.y})`").await
    p.x := 33
    p.x += 1
    print("The point is now `({p.x}, {p.y})`").await
}

# prints:
# The point is `my Point(x: 22, y: 44)`
# The point is `(22, 44)`
# The point is now `(34, 44)`

Some things to note here:

The p = ... statement declares a local variable p.
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, but also the ownership mode (my, in this case). We'll talk about ownership next.
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.
Comments are written #, like Python or Ruby, not // like JavaScript or Rust.

Labeled arguments

One other thing worth nothing is that Dada supports labeled arguments. That means that instead of writing Point(x, y) one can also give labels to each argument:

class Point(x, y)
async fn main() {
    p = Point(x: 22, y: 44)
    print("The point is `{p}`").await
}

# prints:
# The point is `my Point(x: 22, y: 44)`

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).

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

async fn main() {
    var x = 22
    var y = 44
    var p = Point(y, x)
}

See how we reversed the order of y and x? If we try to compile this, Dada will warn us and suggest that this might've been a mistake. We can disable this warning by giving explicit labels to the arguments, making it clear that we meant to switch the order:

async fn main() {
    var x = 22
    var y = 44
    var p = Point(x: y, y: x)
}

Summary and key differences

OK, everything so far hopefully feels fairly familiar. Here are the main highlights:

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.

There is also this thing called ownership. What's that? (Go to the next chapter to find out!)

Creating, dropping, and scopes

Running example

For the next several chapters, we're going to work with variations on this example program:

class Point(x, y)

async fn main() {
    p = Point(x: 22, y: 44)
    print("The point is ({p.x}, {p.y})").await
}

Permissions and ownership

In Dada, variables always track both an object and a set of permissions that they have for using that object. These permissions control what you can do with the object:

Can you write to it or its fields?
Can you read from it?
Can you drop it, freeing its memory?

When you invoke a constructor, you get back a freshly created object with full permissions. We call this being the unique owner -- you're the only one who has access to that object, and you can do anything you want with it. In our code above, that means that p is the owner. Once we have finished using p, the variable is going to be dropped and the Point is going to be freed. Note that this is not like garbage collection, where the memory might get freed -- it is a guarantee. This is important both because it ensures that Dada programs have tight memory usage and because it means that you can rely on other sorts of resources, like files and sockets, being disposed of promptly.

Exploring ownership with the debugger

We can use the interactive debugger to explore permissions and watch how they evolve. To start, run the program below and move the cursor to the start of the print line. This will take you to the point right after p = Point(..) has executed. If you look at the state of the program, you will see:

┌───┐       ┌───────┐
│ p ├──my──►│ Point │
└───┘       │ ───── │
            │ x: 22 │
            │ y: 44 │
            └───────┘

The label my on the edge from p to the Point object is telling you that p owns the Point.

The Point is freed

If you step forward in the debugger past the print, you will see that p has been freed:

class Point(x, y)

async fn main() {
    p = Point(x: 22, y: 44)
    print("The point is ({p.x}, {p.y})").await
    //                                        ▲
    // ───────────────────────────────────────┘
}

┌───┐
│   │
└───┘

What is going on? The answer is that once you get to the point where there p won't be used again, the variable p is destroyed. If p owns its contents, then its contents are also destroyed (and this proceeds recursively; so e.g. if p stored a vector of owned objects, they would be destroyed too).¹

Footnotes

The precise time when p gets destroyed depends on the compiler's analysis, but it will always occur some time after the last use of p and some time before p goes out of scope.

Giving permissions away

At the end of the previous tutorial, we were working with this program:

async fn main() {
    p = Point(x: 22, y: 44)
    print("The point is ({p.x}, {p.y})").await
}

We observed that p owned the Point which was created and that the Point was automatically freed after p finished with it.

Assignments

Next, let's take a look at this program:

async fn main() {
    p = Point(x: 22, y: 44)
    q = p # <-- Added this line!
    print("The point is ({p.x}, {p.y})").await
}

If you run it, you will find that it gets an error:

error: `p` has no value
  > q = p # <-- Added this line!
        - value in `p` was given to `q` here
  > print("The point is ({p.x}, {q.y})).await
                          ^^^ `p` has no value

When you have an assignment like q = p, the default in Dada is that you are giving whatever permissions p has over to q. In this case, since p was the exclusive owner of the value, q becomes the exclusive owner of the value. You can't have two exclusive owners, so that means that p is empty. If you run the debugger, you can see this in action. Position the cursor at the end of the first line:

class Point(x, y)

async fn main() {
    p = Point(x: 22, y: 44)
    #                      ▲
    # ─────────────────────┘
    q = p
    print("The point is ({p.x}, {p.y})").await
}

If you look at the state of the program, you will see:

┌───┐       ┌───────┐
│ p ├──my──►│ Point │
│   │       │ ───── │
│ q │       │ x: 22 │
└───┘       │ y: 44 │
            └───────┘

Now position the cursor at the end of the next line and see how the state changes:

class Point(x, y)

async fn main() {
    p = Point(x: 22, y: 44)
    q = p
    #    ▲
    # ───┘
    print("The point is ({p.x}, {p.y})").await
}


┌───┐       ┌───────┐
│ p │       │ Point │
│   │       │ ───── │
│ q ├──my──►│ x: 22 │
└───┘       │ y: 44 │
            └───────┘

The Point is now owned by q!

Try changing the print to print from q instead of p...you will find the program works as expected.

Making this explicit: the `give` keyword

If you prefer, you can make the move from p to q explicit by using the give keyword:

async fn main() {
    p = Point(x: 22, y: 44)
    q = p.give
    print("The point is ({q.x}, {q.y})").await
}

Give can give more than ownership

Earlier, we said that the give keywords gives all the permissions from one place to another. That is true no matter how many or how few permissions you have. Right now, we're working with things we own, so give transfers ownership. As the tutorial proceeds, we're going to see ways that we can create variables with fewer permissions; using give on those variables will then give those fewer permissions.

Leasing permissions

In the previous chapter, we talked about giving permissions away. But sometimes we would just like to give temporary access; this is where the lease keyword comes in. Consider the following program:

class Point(x, y)

async fn main() {
    p = Point(x: 22, y: 44)
    q = p.lease
    q.x += 1
    print("The point is ({p.x}, {p.y})").await
}

Here, we added the line q = p.lease. What that does is to create a leased copy of the Point. When you lease an object, you are temporarily getting permission to access it.

Unique leases

The default lease is an unique lease. That means that the new variable has exclusive access to the object. So long as the lease is active, all reads and writes to that object have to go through the leased variable (q) or some sublease of q. In the next chapter, we'll talk about shared leases, which can be accessed from many variables (we actually saw a shared lease earlier, in the chapter on creating and dropping objects).

Because q has a unique lease to the Point, it is able to modify the fields of the Point. Let's explore this in the debugger. Position your cursor right before q.x += 1 and you will see:

┌───┐
│   │                  ┌───────┐
│ p ├╌my╌╌╌╌╌╌╌╌╌╌╌╌╌╌►│ Point │
│   │                  │ ───── │
│ q ├─leased(p)───────►│ x: 22 │
│   │                  │ y: 44 │
└───┘                  └───────┘

The leased(p) permission here says that q is leased from p (this implies a unique lease). If we then go to the next line, we see that the value of x changes:

  ┌───┐
  │   │                  ┌───────┐
  │ p ├─my╌╌╌╌╌╌╌╌╌╌╌╌╌╌►│ Point │
  │   │                  │ ───── │
  │ q ├─leased(p)───────►│ x: 23 │
  │   │                  │ y: 44 │
  └───┘                  └───────┘

Subleasing

When you have a leased value, you can lease it again, creating a sublease:

class Point(x, y)

async fn main() {
    p = Point(x: 22, y: 44)
    q = p.lease
    r = q.lease
    r.x += 1
    print("The point is ({p.x}, {p.y})").await
}

Here p was leased to create q, and q then leased its permission to r. If step through in the debugger to just before r.x += 1, we see:

┌───┐
│   │                  
│ p ├╌my╌╌╌╌╌╌╌╌╌╌╌╌╌╌►┌───────┐
│   │                  │ Point │
│ q ├╌leased(p)╌╌╌╌╌╌╌►│ ───── │
│   │                  │ x: 22 │
│ r ├─leased(q)───────►│ y: 44 │
│   │                  └───────┘
└───┘

This shows that the lessor for a lease can either be the owner of the object (p, in the case of q) or another leased value (q, in the case of r).

Ending a lease

Leases last until the lessor chooses to end them. Lessors end a lease by taking some action that violates the terms of the lease: here, since q has an exclusive lease, p can end the lease by reading or writing from the point, as that implies that q no longer has exclusive access. If we go back to our original example with just p and q:

class Point(x, y)

async fn main() {
    p = Point(x: 22, y: 44)
    q = p.lease
    q.x += 1
    print("The point is ({p.x}, {p.y})").await
}

Here the the print statement reads from p -- this will end the lease once it executes. Using the debugger, position the line just after the print and you will see:

┌───┐
│   │                  ┌───────┐
│ p ├─my──────────────►│ Point │
│   │                  │ ───── │
│ q │                  │ x: 22 │
│   │                  │ y: 44 │
└───┘                  └───────┘

What do you think will happen if we try to use q again? Try it and find out!

Giving a leased value

Earlier, we saw that the give keyword can be used to give ownership from one variable to another. Similarly, if you use the give keyword with a leased value, then this leased value is giving its permission to another. This is in fact equivalent to a sublease, and that is exactly what happens. That means that in this program, the q.give is equivalent to q.lease:

class Point(x, y)

async fn main() {
    p = Point(x: 22, y: 44)
    q = p.lease
    r = q.give
    r.x += 1
    print("The point is ({p.x}, {p.y})").await
}

Alternatively, we can even leave the give keyword away:

class Point(x, y)

async fn main() {
    p = Point(x: 22, y: 44)
    q = p.lease
    r = q
    r.x += 1
    print("The point is ({p.x}, {p.y})").await
}

If you step through to the line r.x, you will see the same picture that we saw with q.lease:

┌───┐
│   │                  ┌───────┐
│ p ├╌my╌╌╌╌╌╌╌╌╌╌╌╌╌╌►│ Point │
│   │                  │ ───── │
│ q ├╌leased(p)╌╌╌╌╌╌╌►│ x: 22 │
│   │                  │ y: 44 │
│ r ├─leased(q)───────►│ x: 22 │
│   │                  └───────┘
└───┘

Try modifying the program so that instead of printing from p, we print from q. What happens?

class Point(x, y)

async fn main() {
    p = Point(x: 22, y: 44)
    q = p.lease
    r = q
    r.x += 1
    print("The point is ({q.x}, {q.y})").await
}

(Answer: the sublease on r ends.)

We are now coming to the end of our tour of Dada's permissions. In the previous few chapters we saw:

When you first create an object, you are its owner. When the owning variable goes out of scope, the object is freed.
Owners can give their permissions to others, but then the owner no longer has permission.
Owners can lease their permission, giving other variables exclusive access to the object until the owner uses it again.

You may have noticed a theme here: access to the object is "linear", it moves along a line from variable to variable. There is no point where two variables can be used to access the value. It might seem like leases are an exception, but that's not quite true: with an (exclusive) lease, first the lessee gets access, and then later the lessor reclaims access, but at no point do both of them have access.

The share keyword is used to create a shared permission from a unique permission. Unlike unique permissions, shared permissions can be copied freely into many variables, and all of them are considered equivalent. Let's start with shared ownership, and later we'll talk about sharing a leased value.

Consider this program:

class Point(x, y)

async fn main() {
    p = Point(x: 22, y: 44).share
    q = p
    print("The point is ({p.x}, {p.y})").await
    print("The point is ({q.x}, {q.y})").await
}

The expression Point(x: 22, y: 44).share creates a Point, as we've seen before, but then immediately shares it. If we move the cursor to after the p = ... line, we will see that the ownership from p is marked as our, and not my:

┌───┐
│   │                  ┌───────┐
│ p ├─our─────────────►│ Point │
│   │                  │ ───── │
│ q │                  │ x: 22 │
│   │                  │ y: 44 │
└───┘                  └───────┘

This signals that p considers itself to have shared ownership of the Point. It may seem strange to call p a shared owner when there are no other owners yet. The difference shows up on the next line, when we execute q = p. As we saw before, this gives all the access from p into q -- but because p considers itself a shared owner, p can give its full access to q while retaining its own access. If we move the cursor to just after that line we will see that both of them have the our permission:

┌───┐
│   │                  ┌───────┐
│ p ├─our─────────────►│ Point │
│   │                  │ ───── │
│ q ├─our─────────────►│ x: 22 │
│   │                  │ y: 44 │
└───┘                  └───────┘

Joint ownership

Objects with multiple owners are freed once all of their owners have gone out of scope. Let's explore this with this example:

async fn main() {
    p = Point(x: 22, y: 44).share
    print("The point is ({p.x}, {p.y})").await
    q = p
    print("The point q is ({q.x}, {q.y})).await
}

Position the cursor right before q = p. You will see:

┌───┐
│   │                  ┌───────┐
│ p ├─our─────────────►│ Point │
│   │                  │ ───── │
│ q │                  │ x: 22 │
│   │                  │ y: 44 │
└───┘                  └───────┘

Now move the cursor right after q = p. You will see:

┌───┐
│   │                  ┌───────┐
│ p ├─our─────────────►│ Point │
│   │                  │ ───── │
│ q ├─our─────────────►│ x: 22 │
│   │                  │ y: 44 │
└───┘                  └───────┘

There are now two owners of the Point. OK, let's move one step forward, to right before the print. Now we see:

┌───┐
│   │                  ┌───────┐
│ p │                  │ Point │
│   │                  │ ───── │
│ q ├─our─────────────►│ x: 22 │
│   │                  │ y: 44 │
└───┘                  └───────┘

p is no longer in active use, so the value for p has been dropped, but the Point is not freed. That's because it still has one owner (q).

Notice that q still only has our permission, not my. Once an object is shared, it remains shared. This is because q doesn't know how many other variables there are that may have access to the Point, so it always acts "as if" there are more. There are ways to test at runtime whether you are the only owner left and convert an our permission back into a my permission, but we'll discuss that later.

If you like, step forward a few more steps in the debugger: you'll see that once q goes out of scope, the Point is dropped completely, since it no longer has any owners.

Once something is shared, we can go on and share it even further:

class Point(x, y)

async fn main() {
    p = Point(x: 22, y: 44).share
    q = p.share
    r = q.share
    s = r.share
    # ...and so on
}

Each time we share a jointly owned object like the Point here, we just add one more owner.

Similarly, since all shared variables are equal, when a shared variable gives its permissions to another, that is equivalent to sharing again. In the following program, p, q, and r are all shared owners of the same Point:

class Point(x, y)

async fn main() {
    p = Point(x: 22, y: 44).share
    q = p.give
    r = q        # equivalent to q.give
}

We just saw that, if you have shared ownership, then when you assign from one place to another, you just get two references to the same object. So if we have this program, and we put the cursor after q = p...

class Point(x, y)

async fn main() {
    p = Point(22, 44).share
    q = p
    #    ▲
    # ───┘
}

...then we see:

┌───┐
│   │                  ┌───────┐
│ p ├─our─────────────►│ Point │
│   │                  │ ───── │
│ q ├─our─────────────►│ x: 22 │
│   │                  │ y: 44 │
└───┘                  └───────┘

But what if we move the .share to the next line?

class Point(x, y)

async fn main() {
    p = Point(22, 44)
    q = p.share
    #          ▲
    # ─────────┘
}

What happens now? The answer is that we still see the same thing:

┌───┐
│   │                  ┌───────┐
│ p ├─our─────────────►│ Point │
│   │                  │ ───── │
│ q ├─our─────────────►│ x: 22 │
│   │                  │ y: 44 │
└───┘                  └───────┘

If we move the cursor up one line, though:

class Point(x, y)

async fn main() {
    p = Point(22, 44)
    #                ▲
    # ───────────────┘
    q = p.share
}

we will see that p has full ownership of the Point, and q is not yet initialized:

┌───┐
│   │                  ┌───────┐
│ p ├─my──────────────►│ Point │
│   │                  │ ───── │
│ q │                  │ x: 22 │
│   │                  │ y: 44 │
└───┘                  └───────┘

So what's going on here? The answer is that when you apply share, you are sharing the object, which means that you convert your unique ownership (my) into shared ownership (our), and then you can have multiple references to that jointly owned copy.

Sharing allows many variables to have equal access to the same object at the same time, but that comes with one key limitation: the fields of that object become immutable!

class Point(x, y)

async fn main() {
    p = Point(x: 22, y: 44).share
    p.x += 1 # Exception!
    print("The point is ({p.x}, {p.y})").await
}

This is, in fact, a core principle of Dada: sharing xor mutation. What it means is that we like sharing, and we like mutation, but we don't like having them both at the same time: that way leads to despair. Well, bugs anyway.

The idea of sharing xor mutability needs a bit of justification: it's a pretty big shift from how most languages work! To give you a feeling for why this is such a bedrock principle of Dada, let's look at two examples. For these examples, we'll be using Python, but the same kinds of examples can be constructed in basically any language that permits mutation.

Example 1: Data race

You're probably familiar with the concept of a data race: these occur when you have two threads running in parallel and modifying the same piece of data without any kind of synchronization or coordination. The end result is (typically) unpredictable and arbitrary. Here is some Python code that starts 10 threads, each of which increment the same counter 2 million times. At the end, it prints the counter. What do you think it will print? You'd like to think it will print 20 million. But it won't -- or at least, it might not.

import threading, os

counter = [0]

class MyThread(threading.Thread):
    def run(self):
        for i in range(2000000):
            v = counter[0]
            counter[0] = v + 1
    
    def launch():
        t = MyThread()
        t.start()
        return t

threads = [MyThread.launch() for i in range(10)]
for t in threads:
    t.join()
print(counter)

If you run this, you will likely see different values every time. Why? Because it is possible for another thread to "sneak in" in between these two steps:

v = counter[0]
counter[0] = v + 1

In other words, there might be two threads, both of which read a value of N, increment to N+1, and then store N+1 back. Now there were two counter increments, but the counter only changed by one.¹

Example 2: Iterator invalidation

"Ok", you're thinking, "I know data races are bad. But why should I avoid sharing and mutation in sequential code?" Good question. It turns out that data races are really just a one case of a more general problem. Consider this Python function, which copies all the elements from one list to another:

def transfer(source, target):
    for e in source:
        target.append(e)
    return target

Looks reasonable, right? Now, what do you think happens if I do this?

l = [1, 2, 3]
transfer(l, l)

Answer: in Python, you get an infinite loop. What about in Java? There, if you're lucky, you get an exception; otherwise, you get undefined results. What about in C++? There, this is called iterator invalidation, and it can lead to crashes or even security vulnerabilities.

Fundamentally, the problem here is that transfer was expecting to read from source and write to target; it was not expecting that those writes would also change source. This turns out to be a very general thing. Most of the time, when we are writing code that writes to one variable, we don't expect that it will caues other variables to change their state.

Functional languages respond to this problem by preventing all mutation. That certainly works. Languages like Rust and Dada respond by preventing mutation and sharing from happening at the same time. That works too, and it gives you more flexibility.

But... what if I want a shared counter?

"OK", you're thinking, "I get that sharing and mutation can be dangerous, but what if I want a shared counter? How do I do that?" That's another good question! Dada has a mechanism for doing this called transactions, and they're covered in a future section of this tutorial. The short version, though, is that you can declare when you want to have fields that are mutable even when shared and then modify them: but you can only do it inside a transaction. Inside of that transaction, the Dada runtime ensures that there aren't overlapping reads and writes to the same object from two different variables or two different threads. So we still have sharing xor mutation, but it is enforced differently.

Footnotes

In Python, it's a bit harder to observe this because of the Global Interpreter Lock, but as you can see, it's certainly possible.

Shared leases

Earlier, we saw that:

You can use the share keyword to convert unique ownership into joint ownership.
You can use the lease keyword to temporarily lend out access to a variable without giving up ownership.

But what if you wanted to give many people access to the same object, but only for a limited time? You might want this, for example, so that you could mutate the object again. The answer is that you can combine sharing and leasing to create a shared lease:

class Point(x, y)

async fn main() {
    p = Point(x: 22, y: 44)
    q = p.lease.share
    r = q
    print("p is ({p.x}, {p.y})").await
    print("q is ({q.x}, {q.y})").await
    print("r is ({r.x}, {r.y})").await
    p.x += 1
}

Let's take it step by step. First, position your cursor after p.lease (but before .share) and you will see:

┌───┐
│   │                  ┌───────┐
│ p ├╌my╌╌╌╌╌╌╌╌╌╌╌╌╌╌►│ Point │
│   │                  │ ───── │
│ q ├─leased(p)───────►│ x: 22 │
│   │                  │ y: 44 │
└───┘                  └───────┘

Just after the lease, we have that q is leased from p, the owner. Move the cursor after the .share and we see that the exclusive lease is now a shared lease, indicated by our leased(p):

┌───┐
│   │                  ┌───────┐
│ p ├╌my╌╌╌╌╌╌╌╌╌╌╌╌╌╌►│ Point │
│   │                  │ ───── │
│ q ├─our leased(p)───►│ x: 22 │
│   │                  │ y: 44 │
└───┘                  └───────┘

Although the lease is now shared, p remains the owner of the point (and the lessor of the lease).

Next go past the r = q.share line. As always, sharing a shared thing simply reproduces it:

┌───┐
│   │                  
│ p ├╌my╌╌╌╌╌╌╌╌╌╌╌╌╌╌►┌───────┐
│   │                  │ Point │
│ q ├─our leased(p)───►│ ───── │
│   │                  │ x: 22 │
│ r ├─our leased(p)───►│ y: 44 │
│   │                  └───────┘
└───┘

Finally, if you move your cursor to after p.x += 1 you will see that the lease has expired, so q and r have no value:

┌───┐
│   │                  ┌───────┐
│ p ├─my──────────────►│ Point │
│   │                  │ ───── │
│ q │                  │ x: 23 │
│   │                  │ y: 44 │
│ r │                  └───────┘
│   │                  
└───┘

Leasing a shared value

If x.lease.share produces a shared lease, what do you think happens with x.share.lease? In other words, what happens if we try to lease a shared value?

class Point(x, y)

async fn main() {
    p = Point(x: 22, y: 44).share
    q = q.lease
}

The answer is that p remains the joint owner of the point, but q has a shared lease:

┌───┐
│   │                  ┌───────┐
│ p ├╌our╌╌╌╌╌╌╌╌╌╌╌╌╌►│ Point │
│   │                  │ ───── │
│ q ├─our leased(p)───►│ x: 22 │
│   │                  │ y: 44 │
└───┘                  └───────┘

There is one interesting wrinkle here. Ordinarily, if you lease an object, then the lease is cancelled when the original object is used again. But if you have a shared lease, it's ok to continue using the original object, since the only thing that both of you can do is to read from it:

class Point(x, y)

async fn main() {
    p = Point(x: 22, y: 44).share
    q = q.lease

    # Reading from `p` does not cancel the lease `q`
    print(p).await

    # Reading from `q` still works:
    print(q).await
}

# Prints:
#
# our Point(22, 44)
# our leased Point(22, 44)

Atomic storage and blocks

In the sharing xor mutability section, we discussed how var fields, when shared, become immutable. We also talked about the dangers of mixing sharing and mutation. The challenge is that sometimes you really do want to mix sharing and mutation. As a simple example, we might want to have a shared cache that multiple parts of our code can access. How do we do that?

For this reason, Dada supports a more dynamic variant of sharing xor mutability called "atomic data". The idea is that we can declare some storage as being atomic instead of var. Unlike var storage, atomic storage can be mutated when shared, but only within a transaction. The transaction ensures that all of our changes to that shared data occur as a single unit, without interference from either other variables or other threads.

Let's see an example. To start, we'll write a shared counter type using atomic. It might seem at first that atomic behaves just like var. This code, for example, will print counter is 1:

class Counter(atomic value)

async fn main() {
    var c1 = Counter(0)
    c1.value += 1
    print("counter is {c1.value}").await
}

But what happens if we make the variable c1 a shared variable, instead?

class Counter(atomic value)

async fn main() {
    c1 = Counter(0)
    c1.value += 1
    print("counter is {c1.value}").await
}

When you run this, you'll find that you still get an exception:

error: access to shared, atomic field outside of atomic block
|    c1.value += 1
        ^^^^^ when shared, atomic fields can only be accessed in an atomic block

In fact, even if we comment out the write, we still get an exception:

class Counter(atomic value)

async fn main() {
    c1 = Counter(0)
    // c1.value += 1
    print("counter is {c1.value}").await
}

Running that snippet yields:

error: access to shared, atomic field outside of atomic block
|    print("counter is {c1.value}").await
                           ^^^^^ when shared, atomic fields can only be accessed in an atomic block

Atomic blocks

The solution to our problem, as the message says, is to add an atomic block:

class Counter(atomic value)

async fn main() {
    c1 = Counter(0)
    atomic {
        c1.value += 1

        // we'll come back to this:
        //
        // print("counter is {c1.value}").await
    }
}

Inside of an atomic block, we are allowed to access and modify atomic fields "as if" we had unique access. The runtime tracks what data we are using and looks for conflicts. It also ensures that, if there are multiple threads, the threads execute in some sequential order. In other words, if we had 10 threads each running atomic { c1.value += 1; } we could be sure that the counter had the value 10 at the end, as expected.

Transactions and await

You probably noticed that we commented out the call to print in the previous example. What happens if we uncomment it?

class Counter(atomic value)

async fn main() {
    c1 = Counter(0)
    atomic {
        c1.value += 1

        print("counter is {c1.value}").await
    }
}

When you run this, you see the following error:

error: await cannot be used inside of an atomic block
|    atomic {
     ------ atomic block started here
...
|        print("counter is {c1.value}").await
                                        ^^^^^ await appears here

As the message says, it is not permitted to have an await inside of an atomic block. The reason for this is that atomic blocks are implemented using software transactional memory. The idea is that we monitor the behavior of different threads and detect potential conflicts. If one thread interferes with another, we have to rerun one or both of them to get the final result. Rerunning code that has no side-effects is not a problem. But re-running code that does I/O (such as printing on the screen) would be bad, that would mean you see the same message twice. Since all I/O in Dada is asynchronous, we can guarantee that there are no side-effects by forbidding await inside of an atomic.

You can make the shared counter work by moving the await outside of the atomic block. The value of an atomic block is equal to the value of its last expression, so you can (for example) pass the final value of the counter out from the atomic block and store it into a variable v, like so:

class Counter(atomic value)

async fn main() {
    c1 = Counter(0)
    v = atomic {
        c1.value += 1
        c1.value
    }
    print("counter is {v}").await
}

Printing the variable v doesn't require accessing atomic storage, so there are no problems here.

Another cute way to make this work is to make the value of the atomic block be the thunk itself:

class Counter(atomic value)

async fn main() {
    c1 = Counter(0)
    atomic {
        c1.value += 1

        print("counter is {c1.value}")
    }.await
}

The reason this works is that the string s to be printed is computed inside the atomic block. We then create a thunk for print(s) that will hold on to that string s and return it out from the atomic block. The await then operates on the thunk after the atomic has completed.

Interference between threads

The fact that we can't read shared, atomic fields outside of an atomic block is telling us something interesting. For a moment, imagine that we had shared c1 with other threads: since it is a shared value, that is something we would be allowed to do.

class Counter(atomic value)

async fn main() {
    c1 = Counter(0)
    // ... imagine we shared c1 with other threads here
    v = atomic {
        c1.value += 1
        c1.value
    }
    print("counter is {v}").await
}

If we had done that, then the value that we are going to print is not necessarily the current value of the counter. Consider: if there were multiple threads executing with accessing to c1, they too could be incrementing the counter. Those transactions could occur in between the end of our atomic section and the start of print. This is why we have to both increment and read the value together. If we modify the program to have two atomic blocks, it is actually doing something quite different:

class Counter(atomic value)

async fn main() {
    c1 = Counter(0)
    // ... imagine we shared c1 with other threads here
    atomic { c1.value += 1}
    v = atomic { c1.value }
    print("counter is {v}").await
}

In this version, we are separating the increment from the read. This explicitly makes space for other threads to come in and modify c1.value during that time. Therefore, the value we read for v might be quite different than the value at the end of the first transaction.

Interference within a thread

As described in the sharing xor mutability discussion, it is possible to have interference within a single thread as well. Consider this example, where we have a Point stored in an atomic field (part of a class Cell). There are two references to this cell, cell1 and cell2:

class Point(x, y)
class Cell(atomic value)

async fn main() {
    cell1 = Cell(Point(x: 22, y: 44))
    cell2 = cell1

    x = atomic {
        point1 = cell1.value.lease
        v = point1.x
        cell2.value.x += 1
        point1.x := v + 1
    }

    print("{x}").await
}

What do you think this program prints? Try it and see. OK, I admit it, it's a trick question. The final print never executes:

error: use of invalidated lease
|    point1 = cell1.value.lease
                          ----- lease issued here
...
|    cell2.value.x += 1
                 - lease invalidated here
|    point1.x := v + 1
     ^^^^^^^^ invalidated lease used here

If you step through this program, you can see what's going on. Initially, we see that point1 is leased from cell1:

class Point(x, y)
class Cell(atomic value)

async fn main() {
    cell1 = Cell(Point(x: 22, y: 44))
    cell2 = cell1

    x = atomic {
        point1 = cell1.value.lease
        //                        ▲
        // ───────────────────────┘
        v = point1.x
        cell2.value.x += 1
        point1.x := v + 1
    }

    print("{x}").await
}

// ┌───────────┐             ┌───────┐           ┌───────┐
// │ cell1     ├─our────────►│ Cell  │           │ Point │
// │           │             │ ────  │           │ ───── │
// │ cell2     ├─our────────►│ value ├─atomic───►│ x: 22 │
// │           │             │       │           │ y: 44 │
// ├───────────┤             └───────┘           └───────┘
// │           │                ▲
// │ point1    ├─leased(cell1)──┘
// │           │
// └───────────┘

Moving the cursor to right after the write through cell2.value, we see that this lease has been invalidated:

class Point(x, y)
class Cell(atomic value)

async fn main() {
    cell1 = Cell(Point(x: 22, y: 44))
    cell2 = cell1

    x = atomic {
        point1 = cell1.value.lease
        v = point1.x
        cell2.value.x += 1
        //                ▲
        // ───────────────┘
        point1.x := v + 1
    }

    print("{x}").await
}

// ┌───────────┐             ┌───────┐           ┌───────┐
// │ cell1     ├─our────────►│ Cell  │           │ Point │
// │           │             │ ────  │           │ ───── │
// │ cell2     ├─our────────►│ value ├─atomic───►│ x: 22 │
// │           │             │       │           │ y: 44 │
// ├───────────┤             └───────┘           └───────┘
// │           │
// │ point1    │
// │           │
// └───────────┘

If you think back to the rules on leasing, this makes sense: a lease lasts until the lessor ends it by using the value. In this case, though, the value that was leased had not one lessor (cell1) but two, because it is jointly owned. Either of those lessors can end the lease by using the value again.

To see why this is useful, imagine for a moment that you were writing a function that takes two cells as arguments. Just like the [transfer] function that we described in the sharing xor mutability chapter, you don't realize that cell1 and cell2 refer to the same object. In that case, this code that you wrote above is probably wrong! It is going to read the value of x, mutate it, and then mutate it again, ignoring that write in between. This is precisely the bug we showed as a "data race", but occurring within a single thread. Dada's rules detect this problem and eliminate it.

Leasing versus multiple writes

In the previous example, it was crucial that we created a lease. If we didn't create a lease, the code could execute just fine, for better or worse:

class Point(x, y)
class Cell(atomic value)

async fn main() {
    cell1 = Cell(Point(x: 22, y: 44))
    cell2 = cell1

    x = atomic {
        v = cell1.value.x
        cell2.value.x += 1
        cell1.value.x := v + 1
    }

    print("{x}").await
}

Running this, we see the output 23 -- even though there were two increments, only one took effect. Is this right? Wrong? Well, that's for you, as the author of the code, to say.

The idea here is this: when you lease an object, you are saying "so long as I use this lease, I am not expecting interference from other variables". You are, in effect, creating a kind of "mini-transaction". If however you write the code without a lease, as we did above, then interference is possible. Just as we saw with multiple atomic sections, that may sometimes be what you want!

Tutorial: Typed Dada

This tutorial picks up¹ where the Dynamic Dada tutorial leaves off. It introduces the static type system used by the Dada compiler to help your code avoid errors related to ownership permissions. Using Typed Dada not only makes your code more secure, it also allows us to compile down to tight and efficient machine code that doesn't require any kind of permission checks.

Or it will, once it is written, lol.

Dada for Rustaceans

If you know Rust, many of the concepts in Dada will be familiar, but there are also some key differences. Let's start by exploring dynamic Dada and then we will discuss the type system!

Dynamic Dada: Ownership

When you create a value in Dada, as in Rust, you get ownership of it:

async fn main() {
    var v /* : my Vec */ = [];
    
}

FAQ

Isn't Dada competing with Rust?

I don't think of it that way. To me, the goal of Dada is to explore some ideas without worrying about backwards compatibility with Rust for a time. I figure that this leads us to one of two places:

Dada informs new Rust features and designs, and remains an experiment. There are tons of ideas in Dada that could apply to Rust, although in some cases we'd have to think about how to adapt them.
Dada becomes a successful language in its own right, one that interoperates smoothly and well with Rust.

Why work on Dada?

Working on Dada is really fun and, frankly, kind of relaxing for me. It's also a way to explore different language ideas unfettered by constraints of backwards compatibility. It is my hope that some of the ideas in Dada can make their way back to Rust. --nikomatsakis

Acknowledgments

Dada is designed by nikomatsakis and wycats.

Dada started as a "fork" of the ideas in Lark, which was a joint project by nikomatsakis, wycats, and JT.

Ralf Jung's work on stacked borrows is a key ingredient for Dada's operational semantics and overall approach.

I found Felienne Herman's book The Programmer's Brain quite intriguing, and I've been leaning on the framework it suggests as I iterate and thinking about the experience of learning Dada. I feel confident it is showing up in here.

I also want to highlight Lionel Parreaux's work on Seagl. It has a lot of similarities to Dada's leases and Polonius's origins. Parreaux described it to me many years ago and I didn't fully appreciate the power of this direction at the time. Cool stuff.

--nikomatsakis

Dada: the calculus

Repository

You will find the Dada model in the [dada-lang/dada-model] repository. The model is implemented in PLT Redex, which is a fantastic tool for exploring type systems and operational semantics. This section is meant to explain how it works, but I've not written it yet!

Current status

Working on the operational semantics, which I believe to be "getting close".
The static type system is on hold while those are finalized.
- There is a complete (but no doubt unsound) working type system model, but it targets an older version of Dada.

Permissions

Every reference to a Dada object has an associated permission. Each permission has its own unique identity. In the interpreter, permissions are actual values that are allocated and referenced; this allows us to check for permission violations. In compiled Dada, the type system ensures there are no permission violations, so they can be erased and carry no runtime cost.

Kinds of permissions

Dada has four kinds of permissions, and they can be categorized along two dimensions:

	Exclusive	Shared
Owned	my	our
Leased	leased	our leased

Exclusive permissions give exclusive access to the object, meaning that while that permission is active, no other permission gives access to the same data. They give full ability to mutate. Exclusive permissions cannot be duplicated, but they can be leased, as will be discussed shortly. Shared permissions do not guarantee exclusive access. They can be freely duplicated.

Owned permissions are permissions that independently guarantee that data is live and will not be collected. Leased permissions are tied to some owned permission (called the lessor, see the section on the permission forest).

Owning and leasing: the permission forest

Permissions are structured into a forest to represent leasing relationships. When one permission p is leased to create another permission q, that makes p a parent of q in the forest. We refer to parent-child relationships in this forest as lessor-tenant: i.e., p is the lessor of q and q is the tenant of p.

Cancelling a tenancy

Leased permissions are not permanent. They last until the lessor permission is used in some incompatible way. Using the lessor permission causes it to reassert its access to the object, cancelling the tenant permission. Once a tenant permission is cancelled, any further attempt to use it will create an error (in the interpreter, this is a runtime error; in the compiler, this is a detected by the type system and rejected).

The following sorts of actions cause cancellation:

Reads: Reading with a permission p cancels any exclusive tenants of p (if p is a shared permission, though, it cannot have any exclusive tenants).
Writes: Writing with a permission p cancels all tenants of p (only possible if p is an exclusive permission).
Drops or giving: Dropping an object with permission p cancels all tenants of p, as does giving p (only possible if p is exclusively owned).

The final point is interesting: we can have an our object (shared ownership) that is leased, and that lease can be cancelled:

class Point()

fn test() -> {
    p = Point().share        # our Point
    q = p.lease              # our leased Point
    q                        # returning to the caller drops `p`, cancelling `q`
}

fn main() {
    t = test()               # error, this `our leased Point` has been cancelled
}

Mutation of fields

The ability to mutate a field is dependent on the kind of permission that you have and whether or not the field is declared atomic:

	ordinary field	atomic field
shared permission	immutable	mutable in an atomic section
exclusive permission	mutable	mutable

Actions on a permission

There are three actions one can take on a permission:

give: Giving a permission p creates another permission q with equal capabilities. It does this in the "least disturbing" way possible:
- If p is a shared permission (our, our leased), it is duplicated and so q = p.
- If p is a leased permission, then a sublease q is created with p as the lessor.
- For a my permission p, the older permission is revoked.
lease: Leasing a permission p creates another permission q with equal access, but which can be revoked if p is used again:
- If p is an exclusive permission (my, my leased), then q becomes a my leased permission. q is revoked if p is used again in any way (or if p is revoked).
- If p is a shared permission (our, our leased), then q becomes an our leased permission. q is revoked if p is revoked (p cannot be written to).
share: Sharing a permission p converts it into shared mode and then duplicates it:
- If p is already a joint permission, it simply duplicates p, so p = q.
- If p is a leased permission, it creates a shared tenant q of p.
  - If you write to p again, then q is revoked; reads from p have no effect.
- If p is a my permission, it converts p into a shared permission (our) and then duplicates it.
  - You can continue reading from p, but attempting to write to it will yield an error.

Effectively:

give creates a permission that occupies the same cell in the table.
lease moves one row down.
share moves one column to the right.

Giving a `my` permission away

When you have a my permission p, that permission is relatively "fragile". The only way to create a second permission with access to the same object is to lease from p. The other actions, giving and sharing, both modify p to create the new permission q that now has access to the same object: give will cancel p, sharing converts p into shared ownership. In both cases, p is surrendering some of its permissions to create the new permission. This is only possible if you are the owner of the p permission. This is in contrast to leased permissions, discussed in the next section, which can be cancelled by their lessor permissions.

Building Dada and running tests

If you're interested in contributing to Dada development, the first thing you will want to do is build and run tests. Here's a quick guide to how it works. Note that Dada is implemented in Rust, so you have to install Rust first.

Build and run Dada

Building Dada is easy. Simply clone the repository and type:

> cargo build

Once it is built, you can run it by doing

> cargo dada --help

dada is a cargo alias for cargo run; it turns off some of cargo's output about building things and so forth. If you prefer, you can do

> cargo run -- --help

Running tests

Like any cargo package, Dada's test suite can be run with cargo test. You may also find it convenient to run the Dada test runner alone via...

> cargo dada test

...as this allows you to pass more options. Read the test runner documentation for more details.

Checking a particular file for compilation errors

You can check a particular file for compilation errors by using

> cargo dada check path/to/file.dada

There are other options too, e.g. for dumping out the IR in various stages, check out

> cargo dada check --help

to see the list.

Logs and debugging

If you are debugging Dada, you will probably want to see the logs. You can configure them using the --log parameter. Dada uses tracing so it takes the usual configuration options.

For example, this will dump out all debug logs:

> cargo dada --log debug check dada_tests/hello_world.dada

Or you can dump the logs from a particular crate or module:

> cargo dada --log dada_brew check dada_tests/hello_world.dada

Tutorial

⚠️ DADA DOESN'T REALLY EXIST. ⚠️

This "tutorial" is a thought exercise to get a feeling for how it would be to teach Dada and to explore the ideas without going through the trouble of implementing them.

What is Dada?

Dada is a language for writing reliable, efficient programs. It has a lot in common with Rust, so if you know Rust, you'll likely feel right at home. At the same time, it is meant to feel a lot closer to Java or JavaScript, so if you know those languages, you'll hopefully find it familiar as well. Like Rust, Dada has an ownership-based type system with strong safety guarantees. It doesn't require a garbage collector and it generally compiles to very efficient code. Unlike Rust, Dada doesn't aim to support zero-cost abstractions to the same extent: it has a required runtime, for example, and it Dada values all follow some similar layout rules to improve ergonomics, which can make them larger than they otherwise would be. Dada also doesn't support inline assembly or features like that; if you want to do that sort of thing, you can call out to Rust code.¹

WebAssembly first, optional interpreter

Dada's native target is WebAssembly. It is meant to be embedded on the web and it uses interface types (spec) for its FFI.

In addition to the compiler, Dada has an interpreter. The interpreter is generally used for testing and debugging, since it can do more validation and internal testing. You'll find that all examples in this tutorial are editable and runnable. This is done via the Dada interpreter compiled to WebAssembly.

There is a notion of unsafe code in Dada, but it is much more limited in scope that Rust's unsafe.

Chapters

The tutorial is broken up into chapters:

Dada basics: Start here! Introduces the basics of Dada, including ownership and lending.
Sharing: Introducing sharing.
Joint ownership: Introducing joint ownership.
Classes: Creating classes.
Matching: Matching and subclassing.
Interfaces: Matching and subclassing.

Dada basics

⚠️ DADA DOESN'T REALLY EXIST. ⚠️ See the main tutorial page for more information. Also, you have to pretend that all the code examples are editable and runnable, with live IDE tooltips and so forth. =)

Hello, World

The classic “Hello, World” program in Dada should be quite familiar:

async fn main() {
    print(“Hello, world!”).await
}

The main twist that may be surprising is that, like JavaScript, Dada 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.

Introducing variables

Let's try creating some local variables. Local variables in Dada are introduced with the var keyword. For example, we could create a local variable that stores the print thunk like so:

async fn main() {
    var thunk = print(“Hello, world!”)
    thunk.await
}

Alternatively, we could put the "Hello, world!" string into a variable like so:

async fn main() {
    var greeting = “Hello, world!”
    print(greeting).await
}

Type inference and type annotations on variables

When you create local variables like greeting, you may have noticed that the IDE displays some grey text next to each variable:

async fn main() {
    var greeting: my String = “Hello, world!”
    //          ^^^^^^^^^^^ type hint displayed by the IDE
    print(greeting).await
}

This text indicates the type of the variable greeting; as you can see, the compiler typically infers the types of local variables, but you can also write the annotations yourself if you prefer.

Ownership permission

Let's discuss the type my String itself! The String part is probably fairly familiar to you, but you might be wondering what the word my is about. The keyword my is called an ownership permission; ownership permissions are the way that Dada tracks who has access to a given value, and what kind of access they have. These permissions are the "secret sauce" that allows Dada programs to avoid all kinds of bugs (and the use of a garbage collector).

The my permission indicates that main is the only function that has access to this particular string. That makes sense, since the string was just created. Dada ultimately has four kinds of permissions (my, our, lent, and shared); we'll cover them as we go through the tutorial.

Format strings

In addition to plain string constants, Dada strings can embed program fragments that will get executed and placed inline. These are called "format strings". For example, we could introduce a variable name (set to "world") and then compose greeting like so:

async fn main() {
    var name = “world”
    var greeting = “Hello, {name}”
    print(greeting).await
}

Building up a string imperatively

Format strings are ultimately compiled into some code that builds up the string bit by bit. Let's do that ourselves. Instead of writing "Hello, {name}", let's construct the string by starting with "Hello, " and then appending the word "world":

async fn main() {
    var name = “world”
    var greeting = “Hello, “
    greeting.push_str(name)
    print(greeting).await
}

You'll notice that when you type this in the IDE, the IDE inserts some greyed out text into the call to push_str:

    greeting.lend.push_str(name)
    //      ^^^^^

What is going on here? What is this lend keyword?

Lending

As you probably guessed, lending is related to the ownership permissions. When you have unique access to a value, you can lend it to others, which gives them temporary access. In this case, main owns the string greeting and so when it calls push_str, it is lending access to greeting.

Ownership and lending works just the way it does in real life. Imagine that you are the owner of a book. It is on your shelf. If you think your friend would like it, you can lend it to them. Importantly, though, while your friend is borrowing the book, you no longer have access to it. It's still your book, you still own it, but it's not on your shelf anymore. Lending values in Dada works the same way! While greeting is lent out, it is no longer accessible.

You can't really see the way that lent values become inaccessible in our example because the lent copy of greeting is immediately given to push_str. If we make a simpler example though where everything occurs in one function, you should be able to see it. See the error in the code below? Try editing it and reordering things. You'll see that so long as the lent copy is live (i.e., going to be used later), you can't access greeting:

var greeting = "One"
var greeting_lent = greeting.lend
print(greeting).await // <-- error
greeting_lent.push_str("Two")

Creating a helper function

To better understanding lending, let's create a helper function of our own. We're going to make a function append_name that appends a name to a greeting. The syntax for a function in Dada looks like this:

fn append_name(greeting: String) {
    var name = “world”
    greeting.push_str(name)
}

The first thing to note is that append_name is not an async fn, just a fn. This is because it doesn't do any I/O. The second thing to note is that we are getting an error! Highlight the "squiggly line" on the call to push_str to see the details:

error: cannot lend `greeting`
| fn append_name(greeting: String) {
                 ---------------- greeting is not declared with any permissions
|     greeting.push_str(name)
               ^^^^^^^^
               push_str requires a lent string
help: try declaring `greeting` as a `Lent` string
| fn append_name(greeting: lent String) {
                           +++++

The problem is that function parameters only have the permissions that we give them. We didn't declare greeting with any particular permissions, and so we are not able to lend it out (the only thing we can do is read from it, in fact). We can fix this by applying the compiler's suggestion (try dada fix from the command line if you prefer):

fn append_name(greeting: lent String) {
    var name = “world”
    greeting.push_str(name)
}

Ta da! It works. Now we can modify main to use it:

async fn main() {
    var greeting = “Hello, “
    append_name(greeting) // IDE shows: append_name(greeting.lend)
    print(greeting).await
}

fn append_name(greeting: lent String) {
    var name = “world”
    greeting.push_str(name)
}

As you can see, the call to append_name has a greyed out annotation, indicating that greeting is being lent to append_name.

Covers:

The shared ownership mode and its implications.

Starting point

As our starting point, we'll use the format string example from the basics chapter:

async fn main() {
    var name = “world”
    var greeting = “Hello, {name}”
    print(greeting).await
}

Helper function: `greet`

Let's introduce a helper function called greet. The role of greet is to compose the greeting and print it to the screen:

async fn main() {
    var name = “world”
    greet(name).await
}

async fn greet(name: String) {
    var greeting = “Hello, {name}”
    print(greeting).await
}

Two important things to note:

greet is an async function. This is because it is calling print, which is an async function. Try removing the async keyword and see what happens. (Answer: compilation error.)
Because greet is an async function, calling it yields a thunk which we must await. Try removing the await and running the example and see what happens! (Answer: nothing.)

Why no ownership mode?

You may have noticed that name doesn't have any ownership mode! That's because the only thing we are doing is reading from name. When you write no ownership mode on a function parameter, that means the function can be called with any ownership mode that the caller wants¹.

What's actually happening is that greet is generic over the permissions of name. We'll cover generics in more detail in a later tutorial.

Key capabilities

This section contains a series of draft blog posts that help explain some of the key differences in Dada's approach. These are really comparing and contrasting Dada's core calculus with Rust, and as such the surface syntax we use for Dada changes between them..

Motivating example: returning synthesized values

For this post, I'm going to work through the very basics of ownership in Dada. By the end, I'll show you how Dada solves the "returning synthesized values" problem in Rust.

The "returning synthesized values" problem occurs when you are 'locked in' to a function signature that returns an &T, but you wish to return synthesized data. For example, imagine I have a trait GetName that returns an &str:


#![allow(unused)]
fn main() {
trait GetName {
    fn get_name(&self) -> &str;
}
}

Now imagine that I wish to implement GetName for a struct like Code:


#![allow(unused)]
fn main() {
struct Code { code: usize }

impl GetName for Code {
    fn get_name(&self) -> &str {
        format!("Code({})", self.code) // ERROR
    }
}
}

This code will not compile, and it can be quite frustrating. The type signature of the trait effectively locks me in to returning a reference to some String that is owned by self, but that's not what I want here.

By the end of this post, we'll see how Dada addresses this problem.

Show me the code

Everything I describe here is prototyped in the form of a PLT Redex model. You can find it in the dada-model repository. The model doesn't have a real syntax: Dada programs are represented using S-expressions. For each example, I will link to a test case in the repo.

For the purposes of this post, I'm going to use a "Rust-like surface syntax" for Dada. I have had a lot of fun imagining some ways the syntax could be different, too, and I'll probably blog about those in the future, but I think it would distract from this post.

I me me mine: the basics of ownership in Dada

In Rust, there are three basic types:

String -- an owned string (mutable, movable)
&String -- a shared reference to a string (immutable, copyable)
&mut String -- a mutable reference to a string (mutable, movable)

In Dada, those same three concepts are expressed via permissions that are applied to a type. The names are slightly different, but the concepts are the same:

my String -- an owned string (mutable, movable)
shared String -- a shared string (immutable, copyable)
lent String -- a lent (borrowed) string (mutable, movable)

Local variables in Dada are declared using the var keyword:

var x: my String = "Hello, World!"

As in Rust, owned values can be moved from place to place. As in the MIR representation used internally in the compiler, Dada's formal model makes moves versus copies explicit. A value can be moved from one place to another by using the give keyword:

var x: my String = "Hello, World!"
var y: my String = give x
// Using `x` again here would be an error

Copyable values can be copied using the copy keyword. Attempting to copy an owned class like a my String would be an error, however:

var x: my String = "Hello, World!"
var y: my String = copy x // ERROR: `x` must be moved

In Rust, one uses the &T operator to create a shared reference to a value. In Dada, one uses the share keyword, which creates a shared copy of the value:

var x: my String = "Hello, World!"
var p: shared(x) String = share x

You'll notice an interesting thing: the type of p here is shared(x) String. That x is called a lease, and its Dada's equivalent of a lifetime. It indicates that p is shared from x -- in other words, p is a shared copy of a value that is owned by x.¹

This is a similar model to the one we use in Polonius (explained here); in fact, work on Dada suggested some simplifications that were possible in Polonius, which I'll hopefully describe in a future blog post.

It's possible to have shared values with multiple leases:

var greeting: my String = "Hello, World!"
var farewell: my String = "Goodbye, World!"
p = if say_hello { 
    share greeting
} else {
    share farewell
}

Here, the type of p is shared(greeting | farewell), indicating that p is a shared String owned by either greeting or farewell.

There is a subtyping relationship between shared values: you can always add more leases. So shared(greeting) String <: shared(greeting | farewell) String.

In Rust, if you have a function that returns an &T, you indicate which of the inputs this value was borrowed from by using an explicit lifetime parameter, like so:


#![allow(unused)]
fn main() {
fn get_random<'a>(
    &self, 
    v: &'a Vec<String>,
) -> &'a String
}

In Dada, there are lease parameters, but you would typically use the name of parameters instead:

fn get_random(
    shared self, 
    v: shared Vec<String>,
) -> shared(v) String
//         ^^^

Technically, this is shorthand for a function with two explicit "lease parameters". Lease parameters are a kind of generic parameter that refer to some set of owner variables in the caller(s):

fn get_random<lease l1, lease l2>(
    shared(l1) self, 
    v: shared(l2) Vec<String>,
) -> shared(v) String

The compiler knows that borrowing something from v, when v has type shared(l2), means that you will be borrowing something owned by l2.

If you wanted to write a function that returned one of two things, you could do that as well:

fn pick<type T>(
    a: shared T,
    b: shared T,
) -> shared(a|b) T

Shared copies, not shared references

The representation of shared values is a major point of departure between Dada and Rust: in Rust, an &T is a pointer to the original value. In Dada, a shared T is a copy of the original value. To make it clear:

Type	Language	Representation
String	Rust	(owned data_pointer, length, capacity)
&String	Rust	pointer to `String`
my String	Dada	(owned data_pointer, length, capacity)
shared String	Dada	(shared data_pointer, length, capacity)

In effect, the only difference between a my and a shared value in Dada is whether or not we will run the destructor when it is dropped. For a my value, we will, but for a shared value, we will not.

Making shared values have the same representation as owned values seems surprising at first, but it has a number of important advantages. For example, in Rust, the types &Vec<String> and &Vec<&String> are exactly equivalent in terms of what you can do with them. In both cases, you can only get &String out from that vector. It might be nice if you could interconvert them. But you can't, because they are very different in terms of their runtime representation.

In Dada, shared Vec<String> and shared Vec<shared String> have the same representation and are literally the same type. (It's not always possible to propagate shared modifiers inwards, but I won't go into the details in this post.)

Subtyping between `my` and `shared`

Because my and shared have the same representation, we can actually create a subtyping relationship between my and shared. That is, any place a shared value is expected, a my value can be used instead. For example, imagine we have a function read_file that reads the contents of a file from the disk:

fn read_file(file_name: shared String) -> my String {
    ...
}

Now I can call read_file like so:

var text = read_file("README.md")

Note that "README.md", in Dada, has type my String, not shared String. So this compiles because my String is a subtyping of shared String. This achieves a more limited version of the AsRef pattern we use in Rust.

Returning synthesized values

We are finally ready to return to the "returning synthesized values" problem that I used to kick off the post. If you recall, the problem is that sometimes you get 'locked in' to a function signature that returns an &T, but you wish to return synthesized data, as is the case with the trait GetName and the struct Code in this Rust example:


#![allow(unused)]
fn main() {
trait GetName {
    fn get_name(&self) -> &str;
}

struct Code { code: usize }

impl GetName for Code {
    fn get_name(&self) -> &str {
        format!("Code({})", self.code) // ERROR
    }
}
}

This code will not compile because Code::get_name() is trying to return a String but a &str is expected. This can be very frustrating! The type signature of the trait effectively locks me in to returning a reference to some String that is owned by self, but that's not what I want here.

In Dada, thanks to the subtyping relationship I described, this problem doesn't arise. Here is the equivalent, using a Rust-like syntax for traits and structs:

trait GetName {
    fn get_name(shared self) -> shared String;
}

struct Code { code: usize }

impl GetName for Code {
    fn get_name(shared self) -> shared String {
        "Code({self.code})" // equivalent to `format!`
    }
}

This code compiles just fine because "Code({self.code})" has type my String, and my String is a subtype of shared String.

Downside of subtyping

There are some downsides to Dada's approach: when the compiler sees a variable of type shared String in Dada, it doesn't know a priori whether the value needs to be freed or not. It could be a my String at runtime that does need to be freed. Consider some Dada code like the following:

let c = Code { code: 22 }
let s: shared(c) String = c.get_name()

Here, the type of s (as annotated) is shared(c) String. In other words, this is a shared value that may be owned by c. But in fact, we know that s is really a my String that was created and returned by get_name().

In practice this means that the compiler would have to generate code to check a flag when a shared value is dropped, unless it can see via optimizations that the value is definitely not owned.

Conclusion

To recap, there were two primary ideas that I introduced in this post:

Sharing that is specified in terms of variables, not lifetimes.
Subtyping between owned and shared values, which:
- means that semantically equivalent types like shared Vec<String> and shared Vec<shared String> also have the same representation;
- permits one to return synthesized data when shared data is expected;
- but comes at some cost in space and checking whether destructors are needed.

The Dada Programming Language