Typed Dada

[nikomatsakis]

This issue is tracking ongoing work to introduce Typed Dada.

The plan

The plan roughly proceeds in 3 parts

• Support type declarations in all the usual places (function arguments, return types, local variables)
• Enforce these dynamically
• Add a static checker that reports errors too

The intent is that you can run your program even when you have static type errors and it makes sense, but it will fail if your type annotations are wrong. This lets you explore why you are getting a static type error.

Status

Here is a vague list of things that are done vs not done.

• Type declarations are parsed and validated in function arguments, return types
• Class types work, but strings, integers, and other built-ins don't
• Generic parameter declarations are not parsed (expected syntax: fn foo[T] for types, fn foo[perm P] for permissions)
• Where clauses are not parsed (excepted syntax: fn foo[perm P]() where shared(P), like Rust)
• Generic arguments are not parsed in types (expected syntax: `
• Argument and return types are dynamically checked
• Local variable types are not checked nor validated
• No static checking
• Write tutorials and explanations of type system -- vaguely started

Type system

Here are some examples:

class Character(name: my Name)

fn name(c: shared Character) -> shared{c} Name {
    c.name
}

This signature indicates we take in c which is some shared Character and return a Name that was shared from c (which the code does).

class Character(name: my Name)

fn name(c: shared Character, d: shared Character) -> shared{c} Name {
    d.name
}

The return type is the same, but the function will get an error when it runs, because the name we return was shared from d, not c.

Other types at present:

• my Foo -- indicates a fully owned Foo
• our Foo -- indicates a jointly owned Foo. This counts as shared.
• leased Foo -- indicates a Foo that is uniquely leased from someone.
• leased{x, y} Foo -- indicates a Foo that is leased from either x or y. Currently only makes sense in return types.
• shared Foo -- indicates a Foo that is shared -- either temporarily or permanently (i.e., our).
• shared{x, y} Foo -- indicates a Foo that is shared from either x or y. Currently only makes sense in return types.
• given{x, y} Foo -- indicates a Foo that is given from either x or y. Currently only makes sense in return types.