Unison programming language and hashed semantics

Unison (not to be confused with Unisom, which I sometimes take if sleep eludes me) is a rather interesting, currently-alpha, Haskell-like language. One of the more interesting bits for ATS3 seems to be their approach for how code is stored and transmitted:

Re: Read IO and Write IO

>>So practically speaking, not much trouble, though it does leave room for >>erroneous modeling of effects. Well, this is really unavoidable. If you think about it, there is a even bigger issue. Say you call function 'foo' in your code. How do you even know that 'foo' should be called in the

Re: Read IO and Write IO

I like this. Also, this later discussion reminds me of ZIO in Scala. The trouble only really starts when you import the non-pure code and want to use it from pure code. In that case, you can either go with the default assumption it has all effects ("regular IO"), or annotate it as having specific

Re: Read IO and Write IO

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

Re: Read IO and Write IO

On Sat, Aug 10, 2019 at 10:17 AM Hongwei Xi wrote: > Yes, you should be able to program in the same way as you do now. Thanks. It's good news to port my idiomaticca project to ATS3. -- Kiwamu Okabe at METASEPI DESIGN -- You received this message because you are subscribed to the Google Groups

Re: Read IO and Write IO

>>I can write my code without any IO? Yes, you should be able to program in the same way as you do now. --Hongwei On Fri, Aug 9, 2019 at 8:43 PM Kiwamu Okabe wrote: > Dear all, > > On Fri, Aug 9, 2019 at 8:53 PM gmhwxi wrote: > > If you don't want to track IO effects, then you don't really >

Re: Read IO and Write IO

Dear all, On Fri, Aug 9, 2019 at 8:53 PM gmhwxi wrote: > If you don't want to track IO effects, then you don't really > feel the difference. Umm... There will be an option to write ATS3 code without any IO effects. Example: If I create my own prelude library without IO effect, I can write my

Re: Read IO and Write IO

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,

Re: Read IO and Write IO

Sometimes, a programmer may want to track IO effects. If you don't want to track IO effects, then you don't really feel the difference. On Friday, August 9, 2019 at 2:25:25 AM UTC-4, Kiwamu Okabe wrote: > > Dear Hongwei, > > On Thu, Aug 8, 2019 at 10:24 PM gmhwxi <...> wrote: > > We can

Re: Read IO and Write IO

Dear Hongwei, On Thu, Aug 8, 2019 at 10:24 PM gmhwxi wrote: > We can introduce an abstrace linear VIEW IO: I have a just question. "Why do we separate the IO functions from the pure function?" Unfortunately, I have not felt that such separation is useful... Best regards, -- Kiwamu Okabe at