GHC 9.0, supporting linear types

Re:GHC 9.0, supporting linear types by javbit on Thursday December 31, 2020 @12:51AM (#25589988)

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`.

[ Parent | on HN ]

Re:GHC 9.0, supporting linear types by tome on Thursday December 31, 2020 @06:30AM (#25591725)

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

[ Parent | on HN ]

Re:GHC 9.0, supporting linear types by nimih on Thursday December 31, 2020 @01:42AM (#25590194)

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.

[ Parent | on HN ]