3 ms·
Would withFADR' :: (FragileAndDangerousResource #-> IO ()) -> IO () be a better type? My reasoning is if I use the linear identity function lid :: foral
by 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 agoYeah, 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 agoGood 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