4 ms·

Any pointers to a comparison between Clean's uniqueness typing and GHC's linear types? And is Rust the motivating factor behind linear types cropping up lately

Any pointers to a comparison between Clean's uniqueness typing and GHC's linear types? And is Rust the motivating factor behind linear types cropping up lately? I see Idris is now getting them as well.

necubi 6y ago
Rust has affine types (can be used no more than once), but not linear types (must be used exactly once). Linear types would be a nice feature for rust, and there's been some discussion about how to add them, but as far as I know there hasn't been any real progress there. Affine types in Rust are anything with move semantics; for example you can create a method that consumes itself like this: impl A { fn use(&mut self) { // takes a mutable reference to self, so it // can be used again later } fn consume(self) { // moves self into this function, which means // it cannot be used again } }
- throwaway17_17 6y ago
  I don’t understand how a usage pattern where some variable (representing a semantic object) is said to have an affine type but it can be used more than once. Can you explain how such a type is not just a regular non-substructural type?
  - necubi 6y ago
    Sorry, that wasn't very clear. `&mut self` in the first method ("use") is an example of a non-affine type, `self` in the "consume" method is an affine type which cannot be re-used.
- atombender 6y ago
  What's the importance of having to use a value? I.e. isn't this the same as discarding it? Or is related to things like resource finalizers — i.e. once you open a file, you have to "consume" it in order for it to be closed?
  - necubi 6y ago
    There are lots of bugs that linear types can prevent. For example, if you have an operation that returns a Result that must be handled, you can use linear types to ensure that it is. You can also use linear types to implement safe memory management (Rust's lifetime system is basically a special case of this), by returning a value from `malloc` which must be used in a call to `free`.
    - unnah 6y ago
      Usually what happens in Rust is that if you don't use an owned allocation, it is automatically freed. However, it is possible to leak memory by making a cycle of heap-allocated structures. Can such cycles be prevented by linear types?
- james-mcelwain 6y ago
  > Rust has affine types (can be used no more than once), but not linear types (must be used exactly once) Obviously it's not part of the type system itself, but doesn't the must_use attr get pretty close?
dgellow 6y ago
Idris2 has linear types. I don’t think it will come to Idris.
throwaway17_17 6y ago
One of the best write-ups on the differences (at a level that is comprehensible to most programmers) is Linearity, Uniqueness, and Haskell by Edsko de Vries. 1 - http://edsko.net/2017/01/08/linearity-in-haskell/ http://edsko.net/2017/01/08/linearity-in-haskell/
T-R 6y ago
> is Rust the motivating factor behind linear types cropping up lately? Philip Wadler wrote "Linear Types Can Change the World!" while he was working on Haskell back in 1990. I vaguely remember there were some mentions of possibly adding it a year or two before Rust was publicly announced, but it seemed like it was going to be far off at the time. I wouldn't be surprised if Rust contributed to a lot of the interest in it - Simon Peyton Jones did specifically say that he had "Rust Envy" for shipping something similar to linear types in one of his talks. Linear Types can Change the World!: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.5002 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.5...

necubi 6y ago

Rust has affine types (can be used no more than once), but not linear types (must be used exactly once). Linear types would be a nice feature for rust, and there's been some discussion about how to add them, but as far as I know there hasn't been any real progress there. Affine types in Rust are anything with move semantics; for example you can create a method that consumes itself like this: impl A { fn use(&mut self) { // takes a mutable reference to self, so it // can be used again later } fn consume(self) { // moves self into this function, which means // it cannot be used again } }

throwaway17_17 6y ago
I don’t understand how a usage pattern where some variable (representing a semantic object) is said to have an affine type but it can be used more than once. Can you explain how such a type is not just a regular non-substructural type?
- necubi 6y ago
  Sorry, that wasn't very clear. `&mut self` in the first method ("use") is an example of a non-affine type, `self` in the "consume" method is an affine type which cannot be re-used.
atombender 6y ago
What's the importance of having to use a value? I.e. isn't this the same as discarding it? Or is related to things like resource finalizers — i.e. once you open a file, you have to "consume" it in order for it to be closed?
- necubi 6y ago
  There are lots of bugs that linear types can prevent. For example, if you have an operation that returns a Result that must be handled, you can use linear types to ensure that it is. You can also use linear types to implement safe memory management (Rust's lifetime system is basically a special case of this), by returning a value from `malloc` which must be used in a call to `free`.
  - unnah 6y ago
    Usually what happens in Rust is that if you don't use an owned allocation, it is automatically freed. However, it is possible to leak memory by making a cycle of heap-allocated structures. Can such cycles be prevented by linear types?
james-mcelwain 6y ago
> Rust has affine types (can be used no more than once), but not linear types (must be used exactly once) Obviously it's not part of the type system itself, but doesn't the must_use attr get pretty close?

dgellow 6y ago

Idris2 has linear types. I don’t think it will come to Idris.

throwaway17_17 6y ago

One of the best write-ups on the differences (at a level that is comprehensible to most programmers) is Linearity, Uniqueness, and Haskell by Edsko de Vries. 1 - http://edsko.net/2017/01/08/linearity-in-haskell/ http://edsko.net/2017/01/08/linearity-in-haskell/

T-R 6y ago

> is Rust the motivating factor behind linear types cropping up lately? Philip Wadler wrote "Linear Types Can Change the World!" while he was working on Haskell back in 1990. I vaguely remember there were some mentions of possibly adding it a year or two before Rust was publicly announced, but it seemed like it was going to be far off at the time. I wouldn't be surprised if Rust contributed to a lot of the interest in it - Simon Peyton Jones did specifically say that he had "Rust Envy" for shipping something similar to linear types in one of his talks. Linear Types can Change the World!: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.5002 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.5...