2 ms·

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

by 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

by nimih 6y ago

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