4 ms·

Linear Types for Programmers (2023)

60 points by marvinborner 1y ago

scythmic_waves 1y ago
Sorry off topic but I love the styling of this site.
- Twey 1y 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 :)
jnpnj 1y ago
Newb question, aren't phantom types and typestates a subset (or cousin) of linear types ?
- burakemir 1y 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".
  - jnpnj 1y ago
    Thanks a lot
- Twey 1y 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.
renox 1y ago
There's Austral https://austral-lang.org/ 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.
- Twey 1y 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.
  - marvinborner 1y ago
    Do you know about the Par language? They try to integrate Par into a usable syntax https://github.com/faiface/par-lang https://github.com/faiface/par-lang
    - Twey 1y ago
      I didn't know about this! That's brilliant, thank you for the pointer! Since the death of LtU I don't really know where to learn about interesting new PL work. I try to occasionally read the POPL submissions but there's nothing like HN for PL.
      - marvinborner 1y ago
        Reddit's r/programminglanguages is still quite active. Otherwise most of the community switched to Discord, it seems. (I found Par by hopping the Discord servers of "Programming Language Development"->HOC->Vine->Par)
        Twey 1y ago
        I've been recommended /r/pl a lot but it's not quite the same vibe as LtU. I think LtU was very carefully curated professional research with commentary, while /r/pl has a lot more amateurs asking questions about their hobby languages — which is great, I'm happy that people are experimenting with programming languages, but it does make it hard to use as a way to keep up with the latest big results for someone who doesn't necessarily have the time to follow everything that's going on on the subreddit. Maybe the Discord is the way to go. The user interface confuses the heck out of me, though. Appreciate the recommendation!
melodyogonna 1y ago
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/9dfc97a3fbed72280019812884b5455d https://gist.github.com/VerdagonModular/9dfc97a3fbed72280019...
instig007 1y ago
ATS2 has full support for linear and dependent types, capable of operating at pointer-level arithmetics. While the docs may seem impenetrable, in essence it's just a framework of four composable components 1) constrained data types T's, 2) description of resource management and ownership V's, 3) a statically checked "package-deal" (T * V) for lawful programmer-decided ownership semantics (as opposed to "the only true way" in Rust), and 4) formal proofs of the programmed logic. And you are free to mix & match them canteen-style. Whenever there's a need for complex C API with generics, it's much more pleasant to implement it as a wrapper atop verified ATS C-output rather than C itself. https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x3993.html https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML...

60 points by marvinborner 1y ago

scythmic_waves 1y ago

Sorry off topic but I love the styling of this site.

Twey 1y 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 :)

jnpnj 1y ago

Newb question, aren't phantom types and typestates a subset (or cousin) of linear types ?

burakemir 1y 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".
- jnpnj 1y ago
  Thanks a lot
Twey 1y 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.

renox 1y ago

There's Austral https://austral-lang.org/ 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.

Twey 1y 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.
- marvinborner 1y ago
  Do you know about the Par language? They try to integrate Par into a usable syntax https://github.com/faiface/par-lang https://github.com/faiface/par-lang
  - Twey 1y ago
    I didn't know about this! That's brilliant, thank you for the pointer! Since the death of LtU I don't really know where to learn about interesting new PL work. I try to occasionally read the POPL submissions but there's nothing like HN for PL.
    - marvinborner 1y ago
      Reddit's r/programminglanguages is still quite active. Otherwise most of the community switched to Discord, it seems. (I found Par by hopping the Discord servers of "Programming Language Development"->HOC->Vine->Par)
      - Twey 1y ago
        I've been recommended /r/pl a lot but it's not quite the same vibe as LtU. I think LtU was very carefully curated professional research with commentary, while /r/pl has a lot more amateurs asking questions about their hobby languages — which is great, I'm happy that people are experimenting with programming languages, but it does make it hard to use as a way to keep up with the latest big results for someone who doesn't necessarily have the time to follow everything that's going on on the subreddit. Maybe the Discord is the way to go. The user interface confuses the heck out of me, though. Appreciate the recommendation!

melodyogonna 1y ago

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/9dfc97a3fbed72280019812884b5455d https://gist.github.com/VerdagonModular/9dfc97a3fbed72280019...

instig007 1y ago

ATS2 has full support for linear and dependent types, capable of operating at pointer-level arithmetics. While the docs may seem impenetrable, in essence it's just a framework of four composable components 1) constrained data types T's, 2) description of resource management and ownership V's, 3) a statically checked "package-deal" (T * V) for lawful programmer-decided ownership semantics (as opposed to "the only true way" in Rust), and 4) formal proofs of the programmed logic. And you are free to mix & match them canteen-style. Whenever there's a need for complex C API with generics, it's much more pleasant to implement it as a wrapper atop verified ATS C-output rather than C itself. https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x3993.html https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML...