This seems very versatile and flexible. I like the idea of I/O tracking being opt-in and very specific. I often find that only one type of effect is of interest, and tracking the rest can get in the way.
I recently used a similar technique to track drawing to the screen (using an absview, "DRAWING"). This helped annotate function signatures, as well as provide meaningful restrictions for effects. I do wonder how this change might affect proofs. If it's no longer possible to mark a function as "pure", can any function be used in a proof-function so long as it typechecks? On Thursday, August 8, 2019 at 9:24:02 AM UTC-4, gmhwxi wrote: > > > Because tracking effects is no longer planned in ATS3, we need to > think about how to handle effects incurred by calling external functions. > > We can introduce an abstrace linear VIEW IO: > > absview IO > > Say a function foo needs to do IO. Then it has to have a proof of the view > IO: > > fun foo(!IO | ...): ... > > This is just a monadic style of handing effects in Haskell. > > IO is so-called because there is I and O in IO. So we may also introduce > > absview I and O > > and proof functions > > prfun IO_split : IO -> (I, O) > prfun IO_unsplit: (I, O) -> IO > > If a function only does I but no O, then it only needs a proof of the I > view: > > fun foo2 (!I | ...): ... > > Again, this is just a note put here as a reminder. > > > > -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/58633b60-e4fe-466e-8f84-329bc6499f30%40googlegroups.com.
