4 ms·

Linear types are an interesting idea. I really liked the way that each transformation of the file was a separate File object, reminded me of functional style i

Linear types are an interesting idea. I really liked the way that each transformation of the file was a separate File object, reminded me of functional style immutable data structures where each transformation returns a new structure.

yellowapple 2y ago
Same. Feels like a precocious lovechild between Erlang and Pascal.
toastal 2y ago
ATS2 would give you all the FP + linear types + a proof system. No “capabilities” tho.
nerdponx 2y ago
Idris 2 has some really interesting stuff with linear types. IO is implemented using a linear "world" token. Every I/O operation consumes the current state of the world and returns a new state of the world. Each state of the world must be used exactly once. And the IO monad ends up just being syntactic sugar around this. See https://github.com/stefan-hoeck/idris2-tutorial/blob/main/src/Tutorial/IO.md#how-io-is-implemented https://github.com/stefan-hoeck/idris2-tutorial/blob/main/sr...
sparkie 2y ago
The same technique is also done with uniqueness types, which Clean[1] implements. They look very similar on the surface and are sometimes confused. The paper Linearity and Uniqueness: An Entente Cordiale[2] goes into depth on the differences - but it basically boils down to - Uniqueness is about the history of some value - a contract that asserts it has not been aliased in the past. Linearity is about the future of the value - a contract that it must be consumed exactly once, from this point onward. The benefit of uniqueness types is that it enables us to perform in-place mutation, because we know that nowhere else is this value aliased. The benefit of linear types is to guarantee proper cleanup. The two systems complement each other, and we can have types which are both unique and linear - steadfast types. Austral doesn't have uniqueness types as such, but Capabilities are used to fulfil the same purpose. Because capabilities must be created from other capabilities, they're unforgeable - so we can design types that encapsulate a capability which in effect, ensures their uniqueness, but it's a bit more cumbersome than having uniqueness as a property of the language. Granule has both systems built in - uniqueness and linearity - but it doesn't support types which are both - they have to begin unique and be made into linear values. [1]:https://wiki.clean.cs.ru.nl/download/html_report/CleanRep.2.2_11.htm#_Toc311798092 https://wiki.clean.cs.ru.nl/download/html_report/CleanRep.2.... [2]:https://granule-project.github.io/papers/esop22-paper.pdf https://granule-project.github.io/papers/esop22-paper.pdf

yellowapple 2y ago

Same. Feels like a precocious lovechild between Erlang and Pascal.

toastal 2y ago

ATS2 would give you all the FP + linear types + a proof system. No “capabilities” tho.

nerdponx 2y ago

Idris 2 has some really interesting stuff with linear types. IO is implemented using a linear "world" token. Every I/O operation consumes the current state of the world and returns a new state of the world. Each state of the world must be used exactly once. And the IO monad ends up just being syntactic sugar around this. See https://github.com/stefan-hoeck/idris2-tutorial/blob/main/src/Tutorial/IO.md#how-io-is-implemented https://github.com/stefan-hoeck/idris2-tutorial/blob/main/sr...

sparkie 2y ago

The same technique is also done with uniqueness types, which Clean[1] implements. They look very similar on the surface and are sometimes confused. The paper Linearity and Uniqueness: An Entente Cordiale[2] goes into depth on the differences - but it basically boils down to - Uniqueness is about the history of some value - a contract that asserts it has not been aliased in the past. Linearity is about the future of the value - a contract that it must be consumed exactly once, from this point onward. The benefit of uniqueness types is that it enables us to perform in-place mutation, because we know that nowhere else is this value aliased. The benefit of linear types is to guarantee proper cleanup. The two systems complement each other, and we can have types which are both unique and linear - steadfast types. Austral doesn't have uniqueness types as such, but Capabilities are used to fulfil the same purpose. Because capabilities must be created from other capabilities, they're unforgeable - so we can design types that encapsulate a capability which in effect, ensures their uniqueness, but it's a bit more cumbersome than having uniqueness as a property of the language. Granule has both systems built in - uniqueness and linearity - but it doesn't support types which are both - they have to begin unique and be made into linear values. [1]:https://wiki.clean.cs.ru.nl/download/html_report/CleanRep.2.2_11.htm#_Toc311798092 https://wiki.clean.cs.ru.nl/download/html_report/CleanRep.2.... [2]:https://granule-project.github.io/papers/esop22-paper.pdf https://granule-project.github.io/papers/esop22-paper.pdf