Mojo has some support for Linear Types, it is not fully-fleshed out yet because of missing type system machinery, but the plan is to have full support for Linear Types.
There's Austral https://austral-lang.org/ for linear types, I'm not sure what is the state of the language but it has a nice tutorial about linear types.
explodes4 hours ago
Wow, this really hits the nail on the head for me. I've been pondering about how to make systems that can only be in well-defined states, modified by well-defined state transitions.
This looks like one giant step forward in that direction. I'll be enthusiastically playing around with Austral, all while hoping these concepts can become standardised, and maybe retrofitted to popular tech by way of design patterns or language features, in the future.
Twey11 hours ago
This is great, really accessible! I feel like for me the par operation ⅋ is the thing I struggled with getting intuition for the most, and I think that I am (and everyone else is!) still kind of figuring out the consequences of it, and a lot of language designers neglect it.
jnpnj15 hours ago
Newb question, aren't phantom types and typestates a subset (or cousin) of linear types ?
burakemir15 hours ago
No. A phantom type is a type whose only use is to communicate a constraint on a type variable, without having a runtime value that corresponds to it.
Typestate is a bit closer: it communicates some property where an operation (typically a method invocation) changes the property and hence the typestate. But there isn't necessarily a mechanism that renders the value in the old typestate inaccessible. When there is, then this indeed requires some linearity/affinity ("consuming the object"), but typestate is something built "on top".
jnpnj2 hours ago
Thanks a lot
Twey1 hour ago
Kind of! Specifically typestates allow you to encode the special case of linear functions `f a ⊸ f b` for some type constructor `f` where `a` and `b` are (usually?) phantom types. Phantom types themselves don't involve any linearity per se though.
scythmic_waves16 hours ago
Sorry off topic but I love the styling of this site.
Twey11 hours ago
Hi! I put a lot of effort into getting it to look just how I like it and I'm very happy you like it too :)
Mojo has some support for Linear Types, it is not fully-fleshed out yet because of missing type system machinery, but the plan is to have full support for Linear Types.
Here is the full proposal: https://gist.github.com/VerdagonModular/9dfc97a3fbed72280019...
There's Austral https://austral-lang.org/ for linear types, I'm not sure what is the state of the language but it has a nice tutorial about linear types.
Wow, this really hits the nail on the head for me. I've been pondering about how to make systems that can only be in well-defined states, modified by well-defined state transitions.
This looks like one giant step forward in that direction. I'll be enthusiastically playing around with Austral, all while hoping these concepts can become standardised, and maybe retrofitted to popular tech by way of design patterns or language features, in the future.
This is great, really accessible! I feel like for me the par operation ⅋ is the thing I struggled with getting intuition for the most, and I think that I am (and everyone else is!) still kind of figuring out the consequences of it, and a lot of language designers neglect it.
Newb question, aren't phantom types and typestates a subset (or cousin) of linear types ?
No. A phantom type is a type whose only use is to communicate a constraint on a type variable, without having a runtime value that corresponds to it.
Typestate is a bit closer: it communicates some property where an operation (typically a method invocation) changes the property and hence the typestate. But there isn't necessarily a mechanism that renders the value in the old typestate inaccessible. When there is, then this indeed requires some linearity/affinity ("consuming the object"), but typestate is something built "on top".
Thanks a lot
Kind of! Specifically typestates allow you to encode the special case of linear functions `f a ⊸ f b` for some type constructor `f` where `a` and `b` are (usually?) phantom types. Phantom types themselves don't involve any linearity per se though.
Sorry off topic but I love the styling of this site.
Hi! I put a lot of effort into getting it to look just how I like it and I'm very happy you like it too :)