4 ms·

> Safe zero-copy data (de)serialization, a notoriously difficult endeavour that is in fact so error prone without linear types that most production systems toda

> Safe zero-copy data (de)serialization, a notoriously difficult endeavour that is in fact so error prone without linear types that most production systems today typically avoid it. I wonder how this compares to Rust's borrowing approach which can be used for the same goal. I don't know enough about Haskell to understand Linear types. Perhaps someone more knowledgeable can comment.

Raphael_Amiard 6y ago
Affine types, which Rust more or less implements with its ownership system are very close to linear types, see https://en.m.wikipedia.org/wiki/Substructural_type_system#Affine_type_systems https://en.m.wikipedia.org/wiki/Substructural_type_system#Af...
sa1 6y ago
Rust has affine types (values can be used upto 1 time), which are similar to linear types(values can be used exactly once). Affine types are slightly more general, but offer less guarantees about your program. To add back some guarantees, Rust also has lifetime analysis. So for most common use-cases, you will be able to use Rust and Haskell for similar guarantees. But I’m also eager to see what unique use-cases will be enabled by each of them.
platz 6y ago
GHC models linearity differently. Rust puts linearity on the types, GHC puts linearity on the arrows. https://i.imgur.com/s0Mxhcr_d.webp?maxwidth=640&shape=thumb&fidelity=medium https://i.imgur.com/s0Mxhcr_d.webp?maxwidth=640&shape=thumb&...
- the_duke 6y ago
  Do you know the reasoning why? Not tying the linearity to the type seems quite a bit more confusing and error prone to me. If a type can be used in different ways, I'd rather have two different types.
  - platz 6y ago
    The core logic theory behind linearity on the arrows is provably sound and more well understood theoretically, and it fits better with Haskell's existing semantics. The rust way is probably more practically useful from a programmer's perspective, but it isn't as easily understood to be sound from a type theory perspective.
    - the_duke 6y ago
      So to be clear: Let's say a function returns a linear value. If I then feed this value into a function that does not specify linearity, all linearity is lost and the function can treat it as a regular non-linear type? If yes that would seem to require extreme discipline by the programmer to remain useful.
      - whateveracct 6y ago
        No that's not the case. I am fairly sure that situation you describe results in a type error. The extension does in fact enforce linearity, and does not have such a trivial & universal escape hatch afaiu. Feel free to give GHC 9.0 a try with a minimal example of your scenario!
      - ghostwriter 6y ago
        There is a recent article about these scenarios, you may find it helpful - https://tek.brick.do/64693fb8-39b4-40a5-8762-768009eeed91 https://tek.brick.do/64693fb8-39b4-40a5-8762-768009eeed91
      - mauricioc 6y ago
        There is no such thing as a "linear value" per se, since linearity is on the arrow. But speaking of linear values makes sense when there's an ambient monad, and all of the restrictions you expect are enforced; see Section 2.7 (and the last paragraph of Section 6.1) of https://arxiv.org/pdf/1710.09756.pdf https://arxiv.org/pdf/1710.09756.pdf for details.
      - nimih 6y ago
        The general idea is that the discipline is automatically enforced via the type system, e.g. you have a library which provides a type FragileAndDangerousResource, but the only way to interact with such a thing is via (linear) functions along the lines of withFADR :: (FragileAndDangerousResource #-> a) -> a addToFADR :: Int -> FragileAndDangerousResource #-> FragileAndDangerousResource In other words, linear types are purportedly useful precisely because they make it reasonable to ask for that extreme discipline on the programmer's part, because the compiler is right there to tell them when they screw it up--ideally with a helpful error message.
- ric2b 6y ago
  What is "the arrow" in this context?
  - tremon 6y ago
    "the arrow" is an expression of a function operation, or rather, how a function transforms its arguments. In Haskell, the following signature: func :: A -> B declares a function func that takes one argument of type A and returns a value of type B. I'm guessing a bit, I feel this goes over my head, but here's my layman's interpretation: In Rust, in order to declare a linear type, you must do so when initializing the variable: let x = vec![1, 2, 3]; Now x is declared as move-only, so that the vector cannot be duplicated by assigning it to a second variable; after assignment, accessing x will result in a compiler error. In Haskell, you declare a function func :: A %1 -> B to indicate that after this function call, accessing A should result in a compiler error.
    - paavohtl 6y ago
      I don't find this answer satisfactory, because you also need to specify in Rust whether or not a function moves its argument(s). // This moves the argument fn func(a: A) -> B { .. } func(x); // x is not accessible after this line // This borrows the argument, and therefore won't move it fn func(a: &A) -> B { .. } func(&x); // x remains accessible after this line
      - Ericson2314 6y ago
        From the perspective of Rust, Linear Haskell is going to seem quite weird, and I say that as Haskeller wishing that language extension was more like Rust. I'm not really sure how to explain it, but basically only functions that are themselves linear can have linear parameters, It's vaguely like "`Fn(A) -> B` only if `A: Copy`", and `FnOnce(A) -> B` only if `A: !Copy`, except there is no `Copy` or `!Copy` and the only say to determine it is `Fn` vs `FnOnce`.
KirillPanov 6y ago
For the most part they accomplish the same goals, but in very different ways. Linear types have a simpler mathematical underpinning and are much easier to prove things about. However they are notoriously difficult to use for actual programming, especially in larger projects. Rust's borrow checker is approximately affine types plus regions. Its proof theory gets very complicated if you spell out all the details. However mere mortals can actually write large, complex, and correct programs with it, as has now been empirically demonstrated many times.

Raphael_Amiard 6y ago

Affine types, which Rust more or less implements with its ownership system are very close to linear types, see https://en.m.wikipedia.org/wiki/Substructural_type_system#Affine_type_systems https://en.m.wikipedia.org/wiki/Substructural_type_system#Af...

sa1 6y ago

Rust has affine types (values can be used upto 1 time), which are similar to linear types(values can be used exactly once). Affine types are slightly more general, but offer less guarantees about your program. To add back some guarantees, Rust also has lifetime analysis. So for most common use-cases, you will be able to use Rust and Haskell for similar guarantees. But I’m also eager to see what unique use-cases will be enabled by each of them.

platz 6y ago

GHC models linearity differently. Rust puts linearity on the types, GHC puts linearity on the arrows. https://i.imgur.com/s0Mxhcr_d.webp?maxwidth=640&shape=thumb&fidelity=medium https://i.imgur.com/s0Mxhcr_d.webp?maxwidth=640&shape=thumb&...

the_duke 6y ago
Do you know the reasoning why? Not tying the linearity to the type seems quite a bit more confusing and error prone to me. If a type can be used in different ways, I'd rather have two different types.
- platz 6y ago
  The core logic theory behind linearity on the arrows is provably sound and more well understood theoretically, and it fits better with Haskell's existing semantics. The rust way is probably more practically useful from a programmer's perspective, but it isn't as easily understood to be sound from a type theory perspective.
  - the_duke 6y ago
    So to be clear: Let's say a function returns a linear value. If I then feed this value into a function that does not specify linearity, all linearity is lost and the function can treat it as a regular non-linear type? If yes that would seem to require extreme discipline by the programmer to remain useful.
    - whateveracct 6y ago
      No that's not the case. I am fairly sure that situation you describe results in a type error. The extension does in fact enforce linearity, and does not have such a trivial & universal escape hatch afaiu. Feel free to give GHC 9.0 a try with a minimal example of your scenario!
    - ghostwriter 6y ago
      There is a recent article about these scenarios, you may find it helpful - https://tek.brick.do/64693fb8-39b4-40a5-8762-768009eeed91 https://tek.brick.do/64693fb8-39b4-40a5-8762-768009eeed91
    - mauricioc 6y ago
      There is no such thing as a "linear value" per se, since linearity is on the arrow. But speaking of linear values makes sense when there's an ambient monad, and all of the restrictions you expect are enforced; see Section 2.7 (and the last paragraph of Section 6.1) of https://arxiv.org/pdf/1710.09756.pdf https://arxiv.org/pdf/1710.09756.pdf for details.
    - nimih 6y ago
      The general idea is that the discipline is automatically enforced via the type system, e.g. you have a library which provides a type FragileAndDangerousResource, but the only way to interact with such a thing is via (linear) functions along the lines of withFADR :: (FragileAndDangerousResource #-> a) -> a addToFADR :: Int -> FragileAndDangerousResource #-> FragileAndDangerousResource In other words, linear types are purportedly useful precisely because they make it reasonable to ask for that extreme discipline on the programmer's part, because the compiler is right there to tell them when they screw it up--ideally with a helpful error message.
ric2b 6y ago
What is "the arrow" in this context?
- tremon 6y ago
  "the arrow" is an expression of a function operation, or rather, how a function transforms its arguments. In Haskell, the following signature: func :: A -> B declares a function func that takes one argument of type A and returns a value of type B. I'm guessing a bit, I feel this goes over my head, but here's my layman's interpretation: In Rust, in order to declare a linear type, you must do so when initializing the variable: let x = vec![1, 2, 3]; Now x is declared as move-only, so that the vector cannot be duplicated by assigning it to a second variable; after assignment, accessing x will result in a compiler error. In Haskell, you declare a function func :: A %1 -> B to indicate that after this function call, accessing A should result in a compiler error.
  - paavohtl 6y ago
    I don't find this answer satisfactory, because you also need to specify in Rust whether or not a function moves its argument(s). // This moves the argument fn func(a: A) -> B { .. } func(x); // x is not accessible after this line // This borrows the argument, and therefore won't move it fn func(a: &A) -> B { .. } func(&x); // x remains accessible after this line
    - Ericson2314 6y ago
      From the perspective of Rust, Linear Haskell is going to seem quite weird, and I say that as Haskeller wishing that language extension was more like Rust. I'm not really sure how to explain it, but basically only functions that are themselves linear can have linear parameters, It's vaguely like "`Fn(A) -> B` only if `A: Copy`", and `FnOnce(A) -> B` only if `A: !Copy`, except there is no `Copy` or `!Copy` and the only say to determine it is `Fn` vs `FnOnce`.

KirillPanov 6y ago

For the most part they accomplish the same goals, but in very different ways. Linear types have a simpler mathematical underpinning and are much easier to prove things about. However they are notoriously difficult to use for actual programming, especially in larger projects. Rust's borrow checker is approximately affine types plus regions. Its proof theory gets very complicated if you spell out all the details. However mere mortals can actually write large, complex, and correct programs with it, as has now been empirically demonstrated many times.