5 ms·

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 semant

by 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.
  - javbit 6y ago
    Would withFADR' :: (FragileAndDangerousResource #-> IO ()) -> IO () be a better type? My reasoning is if I use the linear identity function lid :: forall a. a #-> a in the following withFADR lid I should be able to “break out of” the managed context [1] by the types. Using withFADR'' :: (FragileAndDangerousResource #-> ()) -> () is obviously not right since nothing could be done with the `FragileAndDangerousResource`, so I think side effects are necessary. --- [1]: I'm assuming that's what you're going for with `withFADR`.
    - nimih 6y ago
      Yeah, that seems right. I'd also believe you if you told me that the second arrow also needs to be linear, since I can't really give a good reason why it should be one way or the other off the top of my head. I admittedly don't really have a great intuition for how to work with this machinery, since I haven't had a chance/excuse to actually play around with it, to be honest; I'm just going off of a SPJ talk on this stuff I watched many months ago, which I mostly understood at the time, and the paper associated with the GHC implementation, which I understood substantially less of.
    - tome 6y ago
      Good observation. I believe you would use withFADR :: (FragileAndDangerousResource #-> Unrestricted a) -> Unrestricted a One can't tag "linear" values in the type system but one can tag non-linear "unrestricted" values. See "borrow" in Section 7.2, page 5:26 of https://arxiv.org/pdf/1710.09756.pdf https://arxiv.org/pdf/1710.09756.pdf
Ericson2314 6y ago
This has been expressed, but I do not think it is true. Yes, the original linear logic doesn't have anything like a "linear kind", but that's mainly because it's a logic not a type theory. The classic A → B = !A ⊸ B could be interpreted as something like A → B = GC A ⊸ B, i.e. making the ! an in-language type constructor not some sort erased modality. I'm not expert at this stuff, but when I was interrogating this before, I found the thesis behind https://ncatlab.org/nlab/show/linear-non-linear+logic https://ncatlab.org/nlab/show/linear-non-linear+logic as a quite old example (1994, only a few years after the first LL paper from Girard in 1987) of separating the linear and non-linear worlds as two categories with an adjudication between them. This is very compatible with linearity in the types. That all said, I will admit that the "quantitative type theory" line of research gives the current LinearHaskell a big leg up on integrating with dependent types. See https://ncatlab.org/nlab/show/linear-non-linear+logic https://ncatlab.org/nlab/show/linear-non-linear+logic for the latest plans on that. I certainly have no retort. My big complaint about the status quo is we can't even have things like Rust's `Box`, but I have no idea what the operational semantics of `f : pi (b : Box<T>) ...` might be, let alone the static semantics!

by platz 6y ago

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.
- javbit 6y ago
  Would withFADR' :: (FragileAndDangerousResource #-> IO ()) -> IO () be a better type? My reasoning is if I use the linear identity function lid :: forall a. a #-> a in the following withFADR lid I should be able to “break out of” the managed context [1] by the types. Using withFADR'' :: (FragileAndDangerousResource #-> ()) -> () is obviously not right since nothing could be done with the `FragileAndDangerousResource`, so I think side effects are necessary. --- [1]: I'm assuming that's what you're going for with `withFADR`.
  - nimih 6y ago
    Yeah, that seems right. I'd also believe you if you told me that the second arrow also needs to be linear, since I can't really give a good reason why it should be one way or the other off the top of my head. I admittedly don't really have a great intuition for how to work with this machinery, since I haven't had a chance/excuse to actually play around with it, to be honest; I'm just going off of a SPJ talk on this stuff I watched many months ago, which I mostly understood at the time, and the paper associated with the GHC implementation, which I understood substantially less of.
  - tome 6y ago
    Good observation. I believe you would use withFADR :: (FragileAndDangerousResource #-> Unrestricted a) -> Unrestricted a One can't tag "linear" values in the type system but one can tag non-linear "unrestricted" values. See "borrow" in Section 7.2, page 5:26 of https://arxiv.org/pdf/1710.09756.pdf https://arxiv.org/pdf/1710.09756.pdf

Ericson2314 6y ago

This has been expressed, but I do not think it is true. Yes, the original linear logic doesn't have anything like a "linear kind", but that's mainly because it's a logic not a type theory. The classic A → B = !A ⊸ B could be interpreted as something like A → B = GC A ⊸ B, i.e. making the ! an in-language type constructor not some sort erased modality. I'm not expert at this stuff, but when I was interrogating this before, I found the thesis behind https://ncatlab.org/nlab/show/linear-non-linear+logic https://ncatlab.org/nlab/show/linear-non-linear+logic as a quite old example (1994, only a few years after the first LL paper from Girard in 1987) of separating the linear and non-linear worlds as two categories with an adjudication between them. This is very compatible with linearity in the types. That all said, I will admit that the "quantitative type theory" line of research gives the current LinearHaskell a big leg up on integrating with dependent types. See https://ncatlab.org/nlab/show/linear-non-linear+logic https://ncatlab.org/nlab/show/linear-non-linear+logic for the latest plans on that. I certainly have no retort. My big complaint about the status quo is we can't even have things like Rust's `Box`, but I have no idea what the operational semantics of `f : pi (b : Box<T>) ...` might be, let alone the static semantics!