Unison programming language and hashed semantics

[Brandon Barker]

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:



> This dynamic transfer / deployment of arbitrary computations is possible 
> because definitions in Unison are identified by a cryptographic hash of 
> their content, *including the hashes of all dependencies* (the hash is 
> also "nameless" as it isn't affected by naming of variables). To transfer a 
> computation, we send it to the recipient, and the recipient checks to see 
> if the computation references any unknown hashes. Any unknown hashes are 
> synced to the recipient before the transfer completes and the computation 
> proceeds.


So textual references (names) are just aliased to, I suppose, the actual 
semantic meaning of the underlying code, and are stored separately:

To make this happen, Unison just changed the name associated with the hash 
> of foldl *in one place*. The view command just looks up the names for the 
> hashes on the fly, right when it’s printing out the code.
> This is important: Unison isn’t doing a bunch of text mutation on your 
> behalf, updating possibly thousands of files, generating a huge textual 
> diff, and also breaking a bunch of downstream library users who are still 
> expecting that definition to be called by the old name. That would be 
> crazy, right?
> So rename and move things around as much as you want. Don’t worry about 
> picking a perfect name the first time. Give the same definition multiple 
> names if you want. It’s all good!
> ☝️ Using alias.term instead of move.term introduces a new name for a 
> definition without removing the old name(s).
>  


I think there was some discussion on the list previously about doing ATS3 
in a non-textual fashion, but I couldn't quickly find the reference. 

-- 
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 ats-lang-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/5aebc1e2-a178-4790-ab1e-868a79b11a8b%40googlegroups.com.

Re: Read IO and Write IO

[Hongwei Xi]

>>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 first
place?
Usually, it is all based on your understanding of 'foo'? How do you even
know that
your understanding of 'foo' is correct? I think I should stop here :)



On Fri, Aug 9, 2019 at 9:23 PM Brandon Barker 
wrote:

> 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 effects, if you really know what is going on. So
> practically speaking, not much trouble, though it does leave room for
> erroneous modeling of effects.
>
> On Fri, Aug 9, 2019 at 9:17 PM Hongwei Xi  wrote:
> >
> > >>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
> >> > 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 code without any IO?
> >>
> >> Best regards,
> >> --
> >> Kiwamu Okabe at METASEPI DESIGN
> >>
> >> --
> >> 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 ats-lang-users+unsubscr...@googlegroups.com.
> >> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/CAEvX6d%3DJnwDYDzC4%3Dj--dcYqLh4AJYr2pqdtmBA2AioDqngH%3Dg%40mail.gmail.com
> .
> >
> > --
> > 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 ats-lang-users+unsubscr...@googlegroups.com.
> > To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrC5K7Zcya6tw-RV8DMFGjH0oaQW7PiSJrkE0QQfS5foA%40mail.gmail.com
> .
>
>
>
> --
> Brandon Barker
> brandon.bar...@gmail.com
>
> --
> 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 ats-lang-users+unsubscr...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/CAORbNRr5PN7ye6u1FgfWGKRfynmEhQq3hn3_TY2h%2BLb%2BffXjgA%40mail.gmail.com
> .
>

-- 
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 ats-lang-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLpjSJtHtwTYdKGXA7O-0%3DRxn3rAROjk__Rj%3DA1C7Sk6Zg%40mail.gmail.com.

Re: Read IO and Write IO

[Brandon Barker]

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 effects, if you really know what is going on. So
practically speaking, not much trouble, though it does leave room for
erroneous modeling of effects.

On Fri, Aug 9, 2019 at 9:17 PM Hongwei Xi  wrote:
>
> >>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
>> > 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 code without any IO?
>>
>> Best regards,
>> --
>> Kiwamu Okabe at METASEPI DESIGN
>>
>> --
>> 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 ats-lang-users+unsubscr...@googlegroups.com.
>> To view this discussion on the web visit 
>> https://groups.google.com/d/msgid/ats-lang-users/CAEvX6d%3DJnwDYDzC4%3Dj--dcYqLh4AJYr2pqdtmBA2AioDqngH%3Dg%40mail.gmail.com.
>
> --
> 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 ats-lang-users+unsubscr...@googlegroups.com.
> To view this discussion on the web visit 
> https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrC5K7Zcya6tw-RV8DMFGjH0oaQW7PiSJrkE0QQfS5foA%40mail.gmail.com.



-- 
Brandon Barker
brandon.bar...@gmail.com

-- 
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 ats-lang-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/CAORbNRr5PN7ye6u1FgfWGKRfynmEhQq3hn3_TY2h%2BLb%2BffXjgA%40mail.gmail.com.

Re: Read IO and Write IO

[Hongwei Xi]

 >>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  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 ats-lang-users+unsubscr...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/58633b60-e4fe-466e-8f84-329bc6499f30%40googlegroups.com
> 
> .
>

-- 
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 ats-lang-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLohN%3D3uVwpihK0R2p6NUERy59NKvNzKnF%2BW8JR8cUmZRg%40mail.gmail.com.

Re: Read IO and Write IO

[Kiwamu Okabe]

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 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dk18KbWx8QDePLdAr7t8YOTkytv7xWrv95K%2BK6udLcnHA%40mail.gmail.com.

Re: Read IO and Write IO

[Hongwei Xi]

>>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
> > 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 code without any IO?
>
> Best regards,
> --
> Kiwamu Okabe at METASEPI DESIGN
>
> --
> 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 ats-lang-users+unsubscr...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/CAEvX6d%3DJnwDYDzC4%3Dj--dcYqLh4AJYr2pqdtmBA2AioDqngH%3Dg%40mail.gmail.com
> .
>

-- 
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 ats-lang-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrC5K7Zcya6tw-RV8DMFGjH0oaQW7PiSJrkE0QQfS5foA%40mail.gmail.com.

Re: Read IO and Write IO

[Kiwamu Okabe]

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 code without any IO?

Best regards,
-- 
Kiwamu Okabe at METASEPI DESIGN

-- 
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 ats-lang-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/CAEvX6d%3DJnwDYDzC4%3Dj--dcYqLh4AJYr2pqdtmBA2AioDqngH%3Dg%40mail.gmail.com.

Re: Read IO and Write IO

[M88]

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 ats-lang-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/58633b60-e4fe-466e-8f84-329bc6499f30%40googlegroups.com.

Re: Read IO and Write IO

[gmhwxi]

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

-- 
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 ats-lang-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/e3598427-877d-47be-979f-bf758a3a049b%40googlegroups.com.

Re: Read IO and Write IO

[Kiwamu Okabe]

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

-- 
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 ats-lang-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dmiWLDO6_NcXBnxbDefgu%2BibyC_moq%3DcWS4kmkm-BvgBQ%40mail.gmail.com.