>>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?
Good point! There will still be "pure" functions; such functions can be used in proof construction. Given that the word "pure" is already taken, maybe we could call them "proof-like" functions. On Fri, Aug 9, 2019 at 5:02 PM M88 <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/ats-lang-users/58633b60-e4fe-466e-8f84-329bc6499f30%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAPPSPLohN%3D3uVwpihK0R2p6NUERy59NKvNzKnF%2BW8JR8cUmZRg%40mail.gmail.com.
