I speak only of myself since I do not wish to convince, I have no right to drag others into my river, I oblige no one to follow me and everybody practices his art in his own way.
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.
[x] 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: `
[x] 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.
This issue is tracking ongoing work to introduce Typed Dada.
The plan
The plan roughly proceeds in 3 parts
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.
fn foo[T]for types,fn foo[perm P]for permissions)fn foo[perm P]() where shared(P), like Rust)Type system
Here are some examples:
This signature indicates we take in
cwhich is some sharedCharacterand return aNamethat was shared fromc(which the code does).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, notc.Other types at present:
my Foo-- indicates a fully ownedFooour Foo-- indicates a jointly ownedFoo. This counts asshared.leased Foo-- indicates aFoothat is uniquely leased from someone.leased{x, y} Foo-- indicates aFoothat is leased from eitherxory. Currently only makes sense in return types.shared Foo-- indicates aFoothat is shared -- either temporarily or permanently (i.e.,our).shared{x, y} Foo-- indicates aFoothat is shared from eitherxory. Currently only makes sense in return types.given{x, y} Foo-- indicates aFoothat is given from eitherxory. Currently only makes sense in return types.