Comment by pash | Hacker News Reader

Comment by pash | Hacker News Reader

Parent Full thread

Linear logic and affine logic (the latter of which SrPeixinho refers to in that Reddit post) let you use an assumption only once in a proof. Their counterparts in functional programming are called linear and affine types [0]; the arguments of functions with such types are restricted to being used only once in the function’s body. This constraint lets you do some interesting things in compiling and optimizing languages built around these types, and in particular it makes garbage collection trivial.

Linear and affine types are pretty hot right now in the small world of type theory and functional programming. SrPeixinho’s work with his collaborators is aimed at building a language for the Ethereum VM that might actually make it possible to write smart contracts that don’t blow up in your face. It’s good stuff. Search his posts on Reddit to see what he’s up to [1].

0. https://en.wikipedia.org/wiki/Curry–Howard_correspondence

1. https://www.reddit.com/user/SrPeixinho

I think affine types force usage at least once, while linear types force it exactly once. IIRC, this is because linear logic rejects both contraction and weakening while affine logic rejects only contraction.

I'm not sure exactly how this ties into avoiding a GC, but my guess is that rejecting type contraction allows a kind of "reference counting" at the type level.

I was trying to avoid being too detailed, but the distinction is actually that linear types require function arguments to be used exactly once and affine types require that they be used at most once. So affine types allow constant functions, but linear types don’t. A good place to start for anyone interested in learning more is the Wikipedia article on substructural types [0].

And, yes, you’re right that these type systems effectively implement reference counting at the type level. In practice, linear and affine types are used alongside more general types to permit controlled copying and destruction, which tends to look like manual (but type-enforced) memory allocation and deallocation around the edges.

0. https://en.wikipedia.org/wiki/Substructural_type_system

Reply on news.ycombinator.com