Re: Referential transparency in ATS

[Artyom Shalkhakov]

On Sunday, August 18, 2019 at 7:10:26 AM UTC+3, Brandon Barker wrote:
>
> Hi Artyom - would you mind sharing the repo URL, assuming it is open?
>
>
Well, here it is:

https://github.com/ashalkhakov/libatsc
 

> On Thursday, August 8, 2019 at 2:49:43 AM UTC-4, Artyom Shalkhakov wrote:
>>
>> Hi Brandon, Alexander,
>>
>> On Wednesday, August 7, 2019 at 5:31:04 AM UTC+3, Brandon Barker wrote:
>>
>>> I just want to say this is quite intriguing, I think it would be very 
>>> appealing to have a standard library built on this idea (a modification of 
>>> Temptory?), perhaps with some more fleshed out examples of IO splits before 
>>> really digging in.
>>>
>>
>> I'm writing such a library in my spare time, but I find that HX did most 
>> of the work back in ATS0/ATS1 days.
>>
>> Getting back to the problem Alexander mentioned, we could try using 
>> fractional permissions. I'll take an array as an example.
>>
>> We could still try to use fractional permissions (similarly to what is 
>> described here 
>> , PDF)
>>
>>- a collection gets one more type index, k:int (k >= 0)
>>- k stands for fraction 2^(-k) (e.g. k=0 is 1, k=1 is 1/2, etc.)
>>
>> Let's make a fractional dynamically-resizeable array:
>>
>> absview farray_v(a:vtflt, l:addr, n:int, k:int)
>>
>> Examples:
>>
>> farray_v(a,l,n,0) <- whole permission to array, allows writing!
>> farray_v(a,l,n,k) <- k > 0, this is a read-only permission, can't reassign
>>
>> Basically, it's OK to *split* the view in half.
>>
>> praxi split : {a:vtflt}{l:addr}{n:int}{k:nat} farray_v(a,l,n,k) -> 
>> (farray_v(a,l,n,k+1), farray_v(a,l,n,k+1))
>> praxi unsplit : {a:vtflt}{l:addr}{n:int}{k:pos} (farray_v(a,l,n,k), 
>> farray_v(a,l,n,k)) -> farray_v(a,l,n,k-1)
>>
>> Allocation and deallocation only deal with the whole permission:
>>
>> fun{a:tflt}
>> farray_free {l:addr;n:int} (farray_v(a,l,n,0) | ptr l): void
>> fun{a:vtflt}
>> farray_alloc (capacity: int): [l:addr] (farray_v(a,l,0,0) | ptr l)
>>
>> Now we can imagine that some array operations are destructive, so we 
>> require k=0 for the view, but the read-only operations can be used with any 
>> k.
>>
>> fun{a:tflt}
>> farray_get_at {l:addr;n:int;k:int;i:nat | i < n} (!farray_v(a,l,n,k) | 
>> ptr l, int i): a
>> fun{a:vtflt}
>> farray_insert_before {l:addr;n:int;k:int;i:nat | i <= n} 
>> (!farray_v(a,l,n,0) >> farray_v(a,l,n+1,0) | ptr l, int i, a): void
>>
>> Basically:
>>
>>- destructive operations can only be called if you have the whole 
>>permission (i.e. k=0)
>>- destructive operations are: insert, append, prepend, delete
>>
>> However, if we are to give safe types to C++-style iterators, we'd still 
>> need lots more precision... It isn't enough to have an farray(a,n), you 
>> have to ensure that the iterator is from *this* array not *that* array. 
>> This will be very painful to work with. I'll sketch out an iterator API 
>> below.
>>
>> // basically a pointer to array element (but may point past the end of 
>> array: this is the "end" iterator)
>> absvtbox
>> fiter (a:vtflt,l:addr,k:int,b:bool) // b=true: this is the end iterator, 
>> i.e. it can't be read from/written to
>>
>> // simple pointer equality
>> fun
>> eq_fiter {a:vtflt}{l:addr}{k1,k2:int} (!fiter(a,l,k1,b1), 
>> !fiter(a,l,k2,b2)): bool (b1 == b2)
>>
>> // taking pointers out
>> fun{a:vtflt}
>> farray_begin {l:addr}{n:int}{k:int} (!farray_v(a,l,n,k) >> 
>> farray_v(a,l,n,k+1) | ptr l): [b:bool] fiter(a,l,k+1,b)
>> fun{a:vtflt}
>> farray_end {l:addr}{n:int}{k:int} (!farray_v(a,l,n,k) >> 
>> farray_v(a,l,n,k+1) | ptr l): fiter(a,l,k+1,true)
>>
>> // putting pointers back
>> prfun
>> fiter_putback {a:vtflt}{l:addr}{n:int}{k:pos}{b:bool} (!farray_v(a,l,n,k) 
>> >> farray_v(a,l,n,k-1), fiter(a,l,k,b)): void
>>
>> fun{a:vtflt}
>> fiter_succ {l:addr}{k:int} (fiter(a,l,k,b)): fiter(a,l,k,b)
>> fun{a:vtflt}
>> fiter_pred {l:addr}{k:int} (fiter(a,l,k,b)): fiter(a,l,k,b)
>> fun{a:tflt}
>> fiter_get {l:addr}{k:int} (!fiter(a,l,k,false)): a
>> fun{a:tflt}
>> fiter_set {l:addr}{k:int} (!fiter(a,l,k,false), a): void
>>
>> For trees, it's going to be pretty similar, I think: if you have parent 
>> links in this tree, then an iterator is again simply a pointer, and the 
>> "end" iterator is the NULL pointer (so again pretty simple to check).
>>
>> Oh my, this above doesn't directly address the question, sorry! If there 
>> was some way for g_signal_emit( "CHDIR") to invalidate all iterators to 
>> the tree (and moreover, to track this statically), but it doesn't even 
>> mention the tree to begin with.
>>
>>
>>> On Thu, Mar 21, 2019, 8:18 PM gmhwxi  wrote:
>>>

 One can definitely build a monad-based library to support IO:

 absvtype IO(a:vt@ype) = ptr

 The problem with IO monad is that it is so broad. With linear types,
 a programmer can specify a lot more precisely.

 >>is that ATS doesn't (by default?) model an IO effect.

 No, it doesn't 

Re: Referential transparency in ATS

[Brandon Barker]

Hi Artyom - would you mind sharing the repo URL, assuming it is open?

On Thursday, August 8, 2019 at 2:49:43 AM UTC-4, Artyom Shalkhakov wrote:
>
> Hi Brandon, Alexander,
>
> On Wednesday, August 7, 2019 at 5:31:04 AM UTC+3, Brandon Barker wrote:
>
>> I just want to say this is quite intriguing, I think it would be very 
>> appealing to have a standard library built on this idea (a modification of 
>> Temptory?), perhaps with some more fleshed out examples of IO splits before 
>> really digging in.
>>
>
> I'm writing such a library in my spare time, but I find that HX did most 
> of the work back in ATS0/ATS1 days.
>
> Getting back to the problem Alexander mentioned, we could try using 
> fractional permissions. I'll take an array as an example.
>
> We could still try to use fractional permissions (similarly to what is 
> described here 
> , PDF)
>
>- a collection gets one more type index, k:int (k >= 0)
>- k stands for fraction 2^(-k) (e.g. k=0 is 1, k=1 is 1/2, etc.)
>
> Let's make a fractional dynamically-resizeable array:
>
> absview farray_v(a:vtflt, l:addr, n:int, k:int)
>
> Examples:
>
> farray_v(a,l,n,0) <- whole permission to array, allows writing!
> farray_v(a,l,n,k) <- k > 0, this is a read-only permission, can't reassign
>
> Basically, it's OK to *split* the view in half.
>
> praxi split : {a:vtflt}{l:addr}{n:int}{k:nat} farray_v(a,l,n,k) -> 
> (farray_v(a,l,n,k+1), farray_v(a,l,n,k+1))
> praxi unsplit : {a:vtflt}{l:addr}{n:int}{k:pos} (farray_v(a,l,n,k), 
> farray_v(a,l,n,k)) -> farray_v(a,l,n,k-1)
>
> Allocation and deallocation only deal with the whole permission:
>
> fun{a:tflt}
> farray_free {l:addr;n:int} (farray_v(a,l,n,0) | ptr l): void
> fun{a:vtflt}
> farray_alloc (capacity: int): [l:addr] (farray_v(a,l,0,0) | ptr l)
>
> Now we can imagine that some array operations are destructive, so we 
> require k=0 for the view, but the read-only operations can be used with any 
> k.
>
> fun{a:tflt}
> farray_get_at {l:addr;n:int;k:int;i:nat | i < n} (!farray_v(a,l,n,k) | ptr 
> l, int i): a
> fun{a:vtflt}
> farray_insert_before {l:addr;n:int;k:int;i:nat | i <= n} 
> (!farray_v(a,l,n,0) >> farray_v(a,l,n+1,0) | ptr l, int i, a): void
>
> Basically:
>
>- destructive operations can only be called if you have the whole 
>permission (i.e. k=0)
>- destructive operations are: insert, append, prepend, delete
>
> However, if we are to give safe types to C++-style iterators, we'd still 
> need lots more precision... It isn't enough to have an farray(a,n), you 
> have to ensure that the iterator is from *this* array not *that* array. 
> This will be very painful to work with. I'll sketch out an iterator API 
> below.
>
> // basically a pointer to array element (but may point past the end of 
> array: this is the "end" iterator)
> absvtbox
> fiter (a:vtflt,l:addr,k:int,b:bool) // b=true: this is the end iterator, 
> i.e. it can't be read from/written to
>
> // simple pointer equality
> fun
> eq_fiter {a:vtflt}{l:addr}{k1,k2:int} (!fiter(a,l,k1,b1), 
> !fiter(a,l,k2,b2)): bool (b1 == b2)
>
> // taking pointers out
> fun{a:vtflt}
> farray_begin {l:addr}{n:int}{k:int} (!farray_v(a,l,n,k) >> 
> farray_v(a,l,n,k+1) | ptr l): [b:bool] fiter(a,l,k+1,b)
> fun{a:vtflt}
> farray_end {l:addr}{n:int}{k:int} (!farray_v(a,l,n,k) >> 
> farray_v(a,l,n,k+1) | ptr l): fiter(a,l,k+1,true)
>
> // putting pointers back
> prfun
> fiter_putback {a:vtflt}{l:addr}{n:int}{k:pos}{b:bool} (!farray_v(a,l,n,k) 
> >> farray_v(a,l,n,k-1), fiter(a,l,k,b)): void
>
> fun{a:vtflt}
> fiter_succ {l:addr}{k:int} (fiter(a,l,k,b)): fiter(a,l,k,b)
> fun{a:vtflt}
> fiter_pred {l:addr}{k:int} (fiter(a,l,k,b)): fiter(a,l,k,b)
> fun{a:tflt}
> fiter_get {l:addr}{k:int} (!fiter(a,l,k,false)): a
> fun{a:tflt}
> fiter_set {l:addr}{k:int} (!fiter(a,l,k,false), a): void
>
> For trees, it's going to be pretty similar, I think: if you have parent 
> links in this tree, then an iterator is again simply a pointer, and the 
> "end" iterator is the NULL pointer (so again pretty simple to check).
>
> Oh my, this above doesn't directly address the question, sorry! If there 
> was some way for g_signal_emit( "CHDIR") to invalidate all iterators to 
> the tree (and moreover, to track this statically), but it doesn't even 
> mention the tree to begin with.
>
>
>> On Thu, Mar 21, 2019, 8:18 PM gmhwxi  wrote:
>>
>>>
>>> One can definitely build a monad-based library to support IO:
>>>
>>> absvtype IO(a:vt@ype) = ptr
>>>
>>> The problem with IO monad is that it is so broad. With linear types,
>>> a programmer can specify a lot more precisely.
>>>
>>> >>is that ATS doesn't (by default?) model an IO effect.
>>>
>>> No, it doesn't if you use the default library. But nothing prevents you
>>> from tracking IO effects in ATS.
>>>
>>> In the book you mentioned in your message, I was really thinking of
>>> views for specifying memory layouts. With linear views, a programmer
>>> can be very 

Re: Referential transparency in ATS

[Artyom Shalkhakov]

Hi Brandon, Alexander,

On Wednesday, August 7, 2019 at 5:31:04 AM UTC+3, Brandon Barker wrote:

> I just want to say this is quite intriguing, I think it would be very 
> appealing to have a standard library built on this idea (a modification of 
> Temptory?), perhaps with some more fleshed out examples of IO splits before 
> really digging in.
>

I'm writing such a library in my spare time, but I find that HX did most of 
the work back in ATS0/ATS1 days.

Getting back to the problem Alexander mentioned, we could try using 
fractional permissions. I'll take an array as an example.

We could still try to use fractional permissions (similarly to what is 
described here , 
PDF)

   - a collection gets one more type index, k:int (k >= 0)
   - k stands for fraction 2^(-k) (e.g. k=0 is 1, k=1 is 1/2, etc.)
   
Let's make a fractional dynamically-resizeable array:

absview farray_v(a:vtflt, l:addr, n:int, k:int)

Examples:

farray_v(a,l,n,0) <- whole permission to array, allows writing!
farray_v(a,l,n,k) <- k > 0, this is a read-only permission, can't reassign

Basically, it's OK to *split* the view in half.

praxi split : {a:vtflt}{l:addr}{n:int}{k:nat} farray_v(a,l,n,k) -> 
(farray_v(a,l,n,k+1), farray_v(a,l,n,k+1))
praxi unsplit : {a:vtflt}{l:addr}{n:int}{k:pos} (farray_v(a,l,n,k), 
farray_v(a,l,n,k)) -> farray_v(a,l,n,k-1)

Allocation and deallocation only deal with the whole permission:

fun{a:tflt}
farray_free {l:addr;n:int} (farray_v(a,l,n,0) | ptr l): void
fun{a:vtflt}
farray_alloc (capacity: int): [l:addr] (farray_v(a,l,0,0) | ptr l)

Now we can imagine that some array operations are destructive, so we 
require k=0 for the view, but the read-only operations can be used with any 
k.

fun{a:tflt}
farray_get_at {l:addr;n:int;k:int;i:nat | i < n} (!farray_v(a,l,n,k) | ptr 
l, int i): a
fun{a:vtflt}
farray_insert_before {l:addr;n:int;k:int;i:nat | i <= n} 
(!farray_v(a,l,n,0) >> farray_v(a,l,n+1,0) | ptr l, int i, a): void

Basically:

   - destructive operations can only be called if you have the whole 
   permission (i.e. k=0)
   - destructive operations are: insert, append, prepend, delete

However, if we are to give safe types to C++-style iterators, we'd still 
need lots more precision... It isn't enough to have an farray(a,n), you 
have to ensure that the iterator is from *this* array not *that* array. 
This will be very painful to work with. I'll sketch out an iterator API 
below.

// basically a pointer to array element (but may point past the end of 
array: this is the "end" iterator)
absvtbox
fiter (a:vtflt,l:addr,k:int,b:bool) // b=true: this is the end iterator, 
i.e. it can't be read from/written to

// simple pointer equality
fun
eq_fiter {a:vtflt}{l:addr}{k1,k2:int} (!fiter(a,l,k1,b1), 
!fiter(a,l,k2,b2)): bool (b1 == b2)

// taking pointers out
fun{a:vtflt}
farray_begin {l:addr}{n:int}{k:int} (!farray_v(a,l,n,k) >> 
farray_v(a,l,n,k+1) | ptr l): [b:bool] fiter(a,l,k+1,b)
fun{a:vtflt}
farray_end {l:addr}{n:int}{k:int} (!farray_v(a,l,n,k) >> 
farray_v(a,l,n,k+1) | ptr l): fiter(a,l,k+1,true)

// putting pointers back
prfun
fiter_putback {a:vtflt}{l:addr}{n:int}{k:pos}{b:bool} (!farray_v(a,l,n,k) 
>> farray_v(a,l,n,k-1), fiter(a,l,k,b)): void

fun{a:vtflt}
fiter_succ {l:addr}{k:int} (fiter(a,l,k,b)): fiter(a,l,k,b)
fun{a:vtflt}
fiter_pred {l:addr}{k:int} (fiter(a,l,k,b)): fiter(a,l,k,b)
fun{a:tflt}
fiter_get {l:addr}{k:int} (!fiter(a,l,k,false)): a
fun{a:tflt}
fiter_set {l:addr}{k:int} (!fiter(a,l,k,false), a): void

For trees, it's going to be pretty similar, I think: if you have parent 
links in this tree, then an iterator is again simply a pointer, and the 
"end" iterator is the NULL pointer (so again pretty simple to check).

Oh my, this above doesn't directly address the question, sorry! If there 
was some way for g_signal_emit( "CHDIR") to invalidate all iterators to the 
tree (and moreover, to track this statically), but it doesn't even mention 
the tree to begin with.


> On Thu, Mar 21, 2019, 8:18 PM gmhwxi > 
> wrote:
>
>>
>> One can definitely build a monad-based library to support IO:
>>
>> absvtype IO(a:vt@ype) = ptr
>>
>> The problem with IO monad is that it is so broad. With linear types,
>> a programmer can specify a lot more precisely.
>>
>> >>is that ATS doesn't (by default?) model an IO effect.
>>
>> No, it doesn't if you use the default library. But nothing prevents you
>> from tracking IO effects in ATS.
>>
>> In the book you mentioned in your message, I was really thinking of
>> views for specifying memory layouts. With linear views, a programmer
>> can be very precise in describing what memory a function can 
>> access/update.
>> Compared to state monads, this kind of precision is unmatched.
>>
>> On Thursday, March 21, 2019 at 1:28:42 PM UTC-4, Brandon Barker wrote:
>>>
>>>
>>>
>>> On Thursday, March 21, 2019 at 9:30:40 AM UTC-4, Brandon Barker wrote:

 Hi Artyom,

 I'm also grappling with the 

Re: Referential transparency in ATS

[Brandon Barker]

I just want to say this is quite intriguing, I think it would be very
appealing to have a standard library built on this idea (a modification of
Temptory?), perhaps with some more fleshed out examples of IO splits before
really digging in.


On Thu, Mar 21, 2019, 8:18 PM gmhwxi  wrote:

>
> One can definitely build a monad-based library to support IO:
>
> absvtype IO(a:vt@ype) = ptr
>
> The problem with IO monad is that it is so broad. With linear types,
> a programmer can specify a lot more precisely.
>
> >>is that ATS doesn't (by default?) model an IO effect.
>
> No, it doesn't if you use the default library. But nothing prevents you
> from tracking IO effects in ATS.
>
> In the book you mentioned in your message, I was really thinking of
> views for specifying memory layouts. With linear views, a programmer
> can be very precise in describing what memory a function can access/update.
> Compared to state monads, this kind of precision is unmatched.
>
> On Thursday, March 21, 2019 at 1:28:42 PM UTC-4, Brandon Barker wrote:
>>
>>
>>
>> On Thursday, March 21, 2019 at 9:30:40 AM UTC-4, Brandon Barker wrote:
>>>
>>> Hi Artyom,
>>>
>>> I'm also grappling with the issue of RT in this case as I'd so far only
>>> thought about it in terms of function calls, but what you and Vanessa say
>>> helped me to understand the issue. Though I haven't managed to get ATS to
>>> have the same behavior as OCaml in the "let expression" above, I suspect it
>>> is possible. The key phrase here seems to be "side-effecting expression",
>>> and relates to the fact that functions in ATS can perform side effects
>>> without having any effect type or IO monad ascribed to the value (again,
>>> iirc).
>>>
>>
>> Well, maybe that isn't the real key - the real key, I now think, is that
>> ATS doesn't (by default?) model an IO effect. In section 6.9 of
>> http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/PDF/main.pdf it
>> is mentioned that using both linear and dependent types may be used to do
>> this, though I think the suggestion here is for more than printing to e.g.
>> STDOUT.
>>
>> If anyone has looked at modeling/enforcing an IO-like effect type in ATS,
>> I'd be interested to see it.
>>
>>>
>>> Perhaps tonight I should try out the same in Idris or PureScript, which
>>> are not lazily evaluated by default but do use IO, to get a better
>>> understanding.
>>>
>>> On Thursday, March 21, 2019 at 3:17:46 AM UTC-4, Artyom Shalkhakov wrote:

 Hi Brandon,

 Admittedly I don't really understand what RT is, but from what I
 understand, in Haskell the expression like [print "ha"] is basically a
 command to the top-level interpreter (which is the language runtime) to
 perform an effect on the console (moreover, it will be evaluated on
 as-needed basis). Moreover, the ";" is itself another comand, the explicit
 sequencing command, the meaning of which is "perform the left-hand side
 effects, then perform the right-hand side effects". Such a command is a
 value, so it can be passed as a value and reused as many times as is
 necessary. In ATS, the expression like [print "ha"] evaluates right there
 to a void/"no value", and the ";" is also NOT a value at all, but rather a
 "shortcut" syntax to a "let-in-end" form.

 I like to imagine an interpreter that sits in the Haskell's runtime.
 Values of IO type are commands to this interpreter. Typical Haskell
 IO-based programs are building up these commands as they are being
 evaluated by the runtime. The runtime starts evaluation at the "main"
 expression defined by the programmer.

 чт, 21 мар. 2019 г. в 03:45, Brandon Barker :

> I'm a little rusty, so can't come up with many good examples.
>
> Apparently it is possible to do something like this in OCaml:
>
> implement
> main0 () = {
>   val () = let
> val ha = print("ha")
>   in
> (ha; ha) // How to get two ha's here?
>   end
> }
>
>
> After running the program, you would only see one "ha", which violates
> RT.
>
> However, ATS doesn't seem to allow a sequence expression in the "in"
> position of a let expression, as this doesn't compile. Admittedly I'm just
> trying to see if ATS2 doesn't have RT in this particular case, but it 
> would
> also be good to know about the sequence expressions here.
>
> --
> 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-user...@googlegroups.com.
> To post to this group, send email to ats-lan...@googlegroups.com.
> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/5eba6b86-4146-4ba2-a87f-f8c511d902f0%40googlegroups.com
> 

Re: Referential transparency in ATS

[Dambaev Alexander]

This looks interesting, will follow up if/when I will got something from it 
:)

-- 
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/467bd9d0-52e4-4b1b-bb79-9b637f28440a%40googlegroups.com.

Re: Referential transparency in ATS

[gmhwxi]

The problem, as I understand it, is very common in practice.

The solution you outlined in Haskell is what I call a "closed-world" 
solution.

What do I mean by a "closed-world" solution? For instance, in LISP, there
are a lot of functions that are like: creating a resource, using it
and then closing it. This is really a LISP's way to make sure that a 
created resource
is not leaked. In your solution, the obtained iterator must be used in the 
funciton of
the type (Iterator -> IteratorM(next)).

With linear types, we can separate the 3 steps: creating, using, and 
closing:

signal: (!IO) -> void

Iterator_get:
IO -> (Iterator, minus(IO, Iterator), Iterator)

Iterator_use: (!Iterator) -> void

Iterator_return: (minus(IO, Iterator), Iterator) -> IO

Once an iterator is obtained, you no longer have a "full" IO (you only have 
minus(IO, Iterator));
so you cannot call 'signal' any more; you can call it again after the 
iterator is returned.
so 



On Monday, August 5, 2019 at 11:41:32 AM UTC-4, Dambaev Alexander wrote:
>
> Hi all, I want to popup this topic again.
> And I will start with some context: recently, I had debugged pcmanfm file 
> manager's segmentation faults, that happen during navigation through hidden 
> folders. I found out, that the cause of this error is in per-directory 
> settings of displaying hidden files, which means, that if you will enable 
> showing of hidden files in $HOME directory, it will be stored only for this 
> directory. So $HOME/another_dir will not display hidden files, until you 
> will enable this option for directory explicitly.
>
> Here is sequence diagram of calls, that leads to segfaults (you can 
> copy-paste it to stackedit.io, which will render it):
> ```mermaid
> sequenceDiagram
> participant user
> participant side_panel
> participant main_window
> user->>side_panel:1 click on hidden directory
> gtk->>side_panel:2 on_sel_change()
> side_panel->>main_window:3 cancel_pending_chdir()
> side_panel->>gtk:4 emit_chdir_if_needed()
> side_panel->>gtk:5 gtk_tree_selection_get_selected()
> gtk->>side_panel:6 item iterator
> side_panel->>gtk:7 g_signal_emit("CHDIR")
> gtk->>tab_page:8 "CHDIR" signal
> tab_page->>tab_page:9 fm_tab_page_chdir_without_history()
> tab_page->>app_config:10 fm_app_config_get_config_for_path()
> app_config->>tab_page:11 show_hidden=0
> tab_page->>tab_page:12 page->show_hidden=0
> tab_page->>fm_folder:13 fm_folder_view_set_show_hidden(0)
> fm_folder->>fm_folder:14 fm_folder_model_set_show_hidden(0)
> fm_folder->>fm_folder:15 fm_folder_apply_filters()
> fm_folder->>gtk:16 g_signal_emit("row-deleting")
> fm_folder->>gtk:17 g_signal_emit("filter-changed")
> gtk->>fm_folder:18 signal "filter-changed"
> fm_folder->>gtk:19 g_signal_emit("filter-changed")
> gtk->>main_window:20 signal "filter-changed"
> main_window->>main_window:21 on_folder_view_filter_changed()
> main_window->>app_config:22 
> fm_app_config_save_config_for_path(show_hidden=0)
> tab_page->>side_panel:23 fm_side_pane_set_show_hidden(0)
> side_panel->>side_panel:24 fm_dir_tree_view_set_property(0)
> side_panel->>side_panel:25 fm_dir_tree_model_set_show_hidden(0)
> side_panel->>side_panel:26 item_hide_hidden_children()
> side_panel->>tab_page:27 show_hidden=0
> side_panel->>gtk:28 g_signal_emit("CHDIR")
> gtk->>main_window:29 signal "CHDIR"
> main_window->>main_window:30 on_side_pane_chdir()
> main_window->>main_window:31 fm_tab_page_chdir()
> side_panel->>side_panel:32 gtk_tree_model_get_path(item iterator)
> side_panel->>side_panel:33 fm_dir_tree_model_load_row(item iterator)
> ```
>
> In this diagram, at step 6 folders gets **iterator**, which will be used 
> at steps 32 and 33, but this iterator is already invalid, because at step 
> 26 hidden directories will be removed from side panel. This may cause a 
> segfault.
> So, I have started to think about how should look gtk2 API(in non-C 
> language, for GtkTreeIter, as a small example) to prevent such issues, 
> given those requirements:
> 1. usage of ffi calls to gtk2 library(nobody wants to reimplement a wheel, 
> right?);
> 2. When GtkTreeIter is in the scope, it should be impossible to add/delete 
> content to/from GtkTreeView;
> 3. gtk is not thread-safe library, so don't bother with it in API for now.
>
> Initially, I thought that linear types may be helpful here, but then, I 
> had realized, that g_signal_emit() is ffi call, which calls another signal 
> handler, which and I doubt, that linear types will be able to track such 
> behavior.
> Here is, obviously incorrect snippet(due to my lack of knowledge of ATS2):
> extern fn g_signal_emit(string): void = "ext#"
> extern fn g_signal_connect(name: string, handler: ptr->void, ptr): void = 
> "ext#"
>
> fn handler(tree: ptr): void =
>   let
> val () = gtk_tree_view_delete_by_index(tree, 0) (* for simplicity, 
> let's consider, that this is how it is being deleted *)
>
> implement main0(argc,argv) =
>   let
> val (tvpf1 | tv) = gtk_tree_view_new_with_model ()
> (* insert 

Re: Referential transparency in ATS

[Dambaev Alexander]

Thanks for directions to investigate!

>

-- 
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/bed9e22a-e7de-490e-a042-a95be8d36432%40googlegroups.com.

Re: Referential transparency in ATS

[Hongwei Xi]

Thanks!

There are quite a few issues mentioned in your message. Let me address them
separately.

>>The point of `IO` data type in pure language is not about precision. It's
purpose is to control where the source and distribution of side-effects in
your program.
In haskell, it is done in an opposite way: you have one `IO`, that can do
anything and you can split some subset of actions into `IO1`, `IO2` and so
on and the rules how to evaluate (in parallel or in sequence). In fact, it
is very common approach in haskell to define typeclasses for each IO
effect, that is being used in program, like ...

Like Haskell, ATS can be used as a pure language, too.

What is really IO(T) for some type T?

In ATS, we can introduce a linear type IO (for the so-called 'world').
IO(T) in Haskell corresponds to the function type IO -> (IO, T) in ATS.

A type like 'a -> IO(b)' corresponds to a -> IO -> (IO, b), which
corresponds to (IO, a) -> (IO, b)
(uncurrying),  which can be written as (!IO, a) -> b. So we have

Haskell: a -> IO(b) corresponds to (!IO, a) -> b in ATS.

A function of the type (!IO, a) -> b is pure in the sense that it can
use/modify the resource it owns.

Here comes what I consider a big advantage of ATS: IO(T) is now separated
into IO and T; in
particular, IO is a linear type, or more precisely, a linear view (linear
type for proofs); we could introduce
so-called view-change functions (which are proof functions) to manipulate
IO. For illustration, we can
have the following proof functions:

prfun IO_split: IO -> (IO1, IO2)
prfun IO_unsplit: (IO1, IO2) -> IO

for some other linear types IO1 and IO2.

We can also have the following locking functions:

fun IO_lock(): IO
fun IO_unlock(IO): void
fun IO_try_lock(): Option_vt(IO)

which make essential use of IO being a linear type (instead of a monad).

When I said that the IO monad lacks precision, I should have probably said
that the IO monad
lacks the kind of directness and expressiveness offered by a linear IO type.

Of course, monads can also offer what linear types cannot. But a stateful
monad like the IO monad
can be readily handled like what is outlined above.

On Tue, Aug 6, 2019 at 12:44 AM Dambaev Alexander 
wrote:

> Thanks for response.
>
> понедельник, 5 августа 2019 г., 17:56:43 UTC пользователь gmhwxi написал:
>>
>> If I understand correctly, I think I have dealt with this issue before.
>>
>> When an iterator is taken out, you can stop the object from being used
>> until
>> the iterator is returned. For instance, the 'minus' view in
>> PATSHOME/prelude/SATS/extern.sats
>> is precisely introduced for this purpose.
>>
>
> Unfortunately, I am only starting to learn ATS2, so if you can provide a
> simple snippet (not compilable, just to get an idea), which will contain
> main points how `minus` will prevent such errors, that will be great
> starting point for me to investigate another working approaches, that can
> address described issue.
>
> From your description, I imagine, that we can define
> gtk_tree_selection_with_selected (like in Haskell example above), which we
> can use like this:
> fn handler(tree: ptr) = gtk_tree_view_delete_by_index(tree, 0)(* ffi call,
> which removes first row, any iterator is now point to invalid row*)
> implement main0(argc,argv) =
>  let
>val tree = gtk_tree_view_new_with_model (...)
>val () = g_signal_connect ("CHDIR", handler, tree)
>val () = gtk_tree_view_selection_with_selected( lam iterator =>
>   let
> val () = gtk_tree_view_set_color iterator Blue (* some
> valid action with iterator *)
> val () = g_signal_emit ("CHDIR") (* valid, because ATS is
> not pure, but ATS is somehow will know, that handler will make `iterator`
> to be invalid? *)
> val () = gtk_tree_view_set_color iterator Green (*
> compile time error: iterator is invalid ? *)
>   in
>   end)
>  in
>  end
> Given, that iterator is represented as a pointer to GtkTreeIter from gtk2
> and `gtk_tree_view_delete_by_index` is ffi call to some gtk2 function,
> that actually deletes row, which makes any iterator to be invalid. Am I got
> it right? It seems quite optimistic.
>
>
>>
>> To me, a fundamental issue with the IO monad is its lack of precision.
>> Why just one IO? Not IO1,
>> IO2, etc. Say we have two programs P1 and P2; if P1 only uses IO1 and P2
>> only uses IO2, then
>> they can execute in parallel (assuming that IO1 and IO2 are disjoint). If
>> we lump IO1 and IO2 into
>> IO, then parallel execution of P1 and P2 is no longer considered
>> type-safe.
>>
>> The point of `IO` data type in pure language is not about precision. It's
> purpose is to control where the source and distribution of side-effects in
> your program.
> In haskell, it is done in an opposite way: you have one `IO`, that can do
> anything and you can split some subset of actions into `IO1`, `IO2` and so
> on and the rules how to evaluate (in parallel or in sequence). In fact, it
> is 

Re: Referential transparency in ATS

[Dambaev Alexander]

Thanks for response.

понедельник, 5 августа 2019 г., 17:56:43 UTC пользователь gmhwxi написал:
>
> If I understand correctly, I think I have dealt with this issue before.
>
> When an iterator is taken out, you can stop the object from being used 
> until
> the iterator is returned. For instance, the 'minus' view in 
> PATSHOME/prelude/SATS/extern.sats
> is precisely introduced for this purpose.
>

Unfortunately, I am only starting to learn ATS2, so if you can provide a 
simple snippet (not compilable, just to get an idea), which will contain 
main points how `minus` will prevent such errors, that will be great 
starting point for me to investigate another working approaches, that can 
address described issue.

>From your description, I imagine, that we can define 
gtk_tree_selection_with_selected (like in Haskell example above), which we 
can use like this:
fn handler(tree: ptr) = gtk_tree_view_delete_by_index(tree, 0)(* ffi call, 
which removes first row, any iterator is now point to invalid row*)
implement main0(argc,argv) =
 let
   val tree = gtk_tree_view_new_with_model (...)
   val () = g_signal_connect ("CHDIR", handler, tree)
   val () = gtk_tree_view_selection_with_selected( lam iterator => 
  let
val () = gtk_tree_view_set_color iterator Blue (* some 
valid action with iterator *)
val () = g_signal_emit ("CHDIR") (* valid, because ATS is 
not pure, but ATS is somehow will know, that handler will make `iterator` 
to be invalid? *)
val () = gtk_tree_view_set_color iterator Green (* compile 
time error: iterator is invalid ? *)
  in
  end)
 in
 end
Given, that iterator is represented as a pointer to GtkTreeIter from gtk2 
and `gtk_tree_view_delete_by_index` is ffi call to some gtk2 function, that 
actually deletes row, which makes any iterator to be invalid. Am I got it 
right? It seems quite optimistic.
 

>
> To me, a fundamental issue with the IO monad is its lack of precision. Why 
> just one IO? Not IO1,
> IO2, etc. Say we have two programs P1 and P2; if P1 only uses IO1 and P2 
> only uses IO2, then
> they can execute in parallel (assuming that IO1 and IO2 are disjoint). If 
> we lump IO1 and IO2 into
> IO, then parallel execution of P1 and P2 is no longer considered type-safe.
>
> The point of `IO` data type in pure language is not about precision. It's 
purpose is to control where the source and distribution of side-effects in 
your program.
In haskell, it is done in an opposite way: you have one `IO`, that can do 
anything and you can split some subset of actions into `IO1`, `IO2` and so 
on and the rules how to evaluate (in parallel or in sequence). In fact, it 
is very common approach in haskell to define typeclasses for each IO 
effect, that is being used in program, like
class Monad m => UsesFileSystem m where
  openFile :: String-> IOMode-> m Handle

class Monad m => UsesNetwork m where
  socket :: SocketFamily-> SocketType-> m Socket


some_custom_action
 :: ( UsesFileSystem m
, UsesNetwork m
, Monad m
)
 => m ()
some_custom_action = do
 h <- openFile "test" ReadOnly
 s <- socket AF_UNIX Datagram
 return ()
which helps with mock tests by allowing usage of `some_custom_action` for 
any monad, that has appropriate instances

In the haskell example above, I had defined `IteratorM` datatype and monad, 
which can be treated as subset of IO (or IO1 from your example) with number 
of actions in it (like `gtk_tree_view_iter_set_color`). The whole purpose 
of it is to forbid composition such `IO1` with other `IO` actions 
(including any other `IO2` actions) and to consider such composition as not 
type-safe. I see no point to run `IteratorM` and `IO2` in parallel as such 
uncontrolled mixing is the source of described issue in a first place.

But, maybe, I just didn't get what you mean in your example with `IO1` and 
`IO2`?

-- 
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/4a5064b4-357e-4055-b1af-44373e076592%40googlegroups.com.

Re: Referential transparency in ATS

[Hongwei Xi]

If I understand correctly, I think I have dealt with this issue before.

When an iterator is taken out, you can stop the object from being used until
the iterator is returned. For instance, the 'minus' view in
PATSHOME/prelude/SATS/extern.sats
is precisely introduced for this purpose.

To me, a fundamental issue with the IO monad is its lack of precision. Why
just one IO? Not IO1,
IO2, etc. Say we have two programs P1 and P2; if P1 only uses IO1 and P2
only uses IO2, then
they can execute in parallel (assuming that IO1 and IO2 are disjoint). If
we lump IO1 and IO2 into
IO, then parallel execution of P1 and P2 is no longer considered type-safe.



On Mon, Aug 5, 2019 at 11:41 AM Dambaev Alexander 
wrote:

> Hi all, I want to popup this topic again.
> And I will start with some context: recently, I had debugged pcmanfm file
> manager's segmentation faults, that happen during navigation through hidden
> folders. I found out, that the cause of this error is in per-directory
> settings of displaying hidden files, which means, that if you will enable
> showing of hidden files in $HOME directory, it will be stored only for this
> directory. So $HOME/another_dir will not display hidden files, until you
> will enable this option for directory explicitly.
>
> Here is sequence diagram of calls, that leads to segfaults (you can
> copy-paste it to stackedit.io, which will render it):
> ```mermaid
> sequenceDiagram
> participant user
> participant side_panel
> participant main_window
> user->>side_panel:1 click on hidden directory
> gtk->>side_panel:2 on_sel_change()
> side_panel->>main_window:3 cancel_pending_chdir()
> side_panel->>gtk:4 emit_chdir_if_needed()
> side_panel->>gtk:5 gtk_tree_selection_get_selected()
> gtk->>side_panel:6 item iterator
> side_panel->>gtk:7 g_signal_emit("CHDIR")
> gtk->>tab_page:8 "CHDIR" signal
> tab_page->>tab_page:9 fm_tab_page_chdir_without_history()
> tab_page->>app_config:10 fm_app_config_get_config_for_path()
> app_config->>tab_page:11 show_hidden=0
> tab_page->>tab_page:12 page->show_hidden=0
> tab_page->>fm_folder:13 fm_folder_view_set_show_hidden(0)
> fm_folder->>fm_folder:14 fm_folder_model_set_show_hidden(0)
> fm_folder->>fm_folder:15 fm_folder_apply_filters()
> fm_folder->>gtk:16 g_signal_emit("row-deleting")
> fm_folder->>gtk:17 g_signal_emit("filter-changed")
> gtk->>fm_folder:18 signal "filter-changed"
> fm_folder->>gtk:19 g_signal_emit("filter-changed")
> gtk->>main_window:20 signal "filter-changed"
> main_window->>main_window:21 on_folder_view_filter_changed()
> main_window->>app_config:22
> fm_app_config_save_config_for_path(show_hidden=0)
> tab_page->>side_panel:23 fm_side_pane_set_show_hidden(0)
> side_panel->>side_panel:24 fm_dir_tree_view_set_property(0)
> side_panel->>side_panel:25 fm_dir_tree_model_set_show_hidden(0)
> side_panel->>side_panel:26 item_hide_hidden_children()
> side_panel->>tab_page:27 show_hidden=0
> side_panel->>gtk:28 g_signal_emit("CHDIR")
> gtk->>main_window:29 signal "CHDIR"
> main_window->>main_window:30 on_side_pane_chdir()
> main_window->>main_window:31 fm_tab_page_chdir()
> side_panel->>side_panel:32 gtk_tree_model_get_path(item iterator)
> side_panel->>side_panel:33 fm_dir_tree_model_load_row(item iterator)
> ```
>
> In this diagram, at step 6 folders gets **iterator**, which will be used
> at steps 32 and 33, but this iterator is already invalid, because at step
> 26 hidden directories will be removed from side panel. This may cause a
> segfault.
> So, I have started to think about how should look gtk2 API(in non-C
> language, for GtkTreeIter, as a small example) to prevent such issues,
> given those requirements:
> 1. usage of ffi calls to gtk2 library(nobody wants to reimplement a wheel,
> right?);
> 2. When GtkTreeIter is in the scope, it should be impossible to add/delete
> content to/from GtkTreeView;
> 3. gtk is not thread-safe library, so don't bother with it in API for now.
>
> Initially, I thought that linear types may be helpful here, but then, I
> had realized, that g_signal_emit() is ffi call, which calls another signal
> handler, which and I doubt, that linear types will be able to track such
> behavior.
> Here is, obviously incorrect snippet(due to my lack of knowledge of ATS2):
> extern fn g_signal_emit(string): void = "ext#"
> extern fn g_signal_connect(name: string, handler: ptr->void, ptr): void =
> "ext#"
>
> fn handler(tree: ptr): void =
>   let
> val () = gtk_tree_view_delete_by_index(tree, 0) (* for simplicity,
> let's consider, that this is how it is being deleted *)
>
> implement main0(argc,argv) =
>   let
> val (tvpf1 | tv) = gtk_tree_view_new_with_model ()
> (* insert 1 row into tree view *)
> val () = g_signal_connect( "CHDIR", handler, tv)
> val (p | iter) = gtk_tree_selection_get_selected( tvpf1 | tv) (* get
> iterator on a row 0 *)
> val () = g_signal_emit( "CHDIR") (* handler will delete row 0 *)
> val (p | iter) = gtk_tree_model_get_path( p | iter) (* iter is invalid
> here, can 

Re: Referential transparency in ATS

[Dambaev Alexander]

Hi all, I want to popup this topic again.
And I will start with some context: recently, I had debugged pcmanfm file 
manager's segmentation faults, that happen during navigation through hidden 
folders. I found out, that the cause of this error is in per-directory 
settings of displaying hidden files, which means, that if you will enable 
showing of hidden files in $HOME directory, it will be stored only for this 
directory. So $HOME/another_dir will not display hidden files, until you 
will enable this option for directory explicitly.

Here is sequence diagram of calls, that leads to segfaults (you can 
copy-paste it to stackedit.io, which will render it):
```mermaid
sequenceDiagram
participant user
participant side_panel
participant main_window
user->>side_panel:1 click on hidden directory
gtk->>side_panel:2 on_sel_change()
side_panel->>main_window:3 cancel_pending_chdir()
side_panel->>gtk:4 emit_chdir_if_needed()
side_panel->>gtk:5 gtk_tree_selection_get_selected()
gtk->>side_panel:6 item iterator
side_panel->>gtk:7 g_signal_emit("CHDIR")
gtk->>tab_page:8 "CHDIR" signal
tab_page->>tab_page:9 fm_tab_page_chdir_without_history()
tab_page->>app_config:10 fm_app_config_get_config_for_path()
app_config->>tab_page:11 show_hidden=0
tab_page->>tab_page:12 page->show_hidden=0
tab_page->>fm_folder:13 fm_folder_view_set_show_hidden(0)
fm_folder->>fm_folder:14 fm_folder_model_set_show_hidden(0)
fm_folder->>fm_folder:15 fm_folder_apply_filters()
fm_folder->>gtk:16 g_signal_emit("row-deleting")
fm_folder->>gtk:17 g_signal_emit("filter-changed")
gtk->>fm_folder:18 signal "filter-changed"
fm_folder->>gtk:19 g_signal_emit("filter-changed")
gtk->>main_window:20 signal "filter-changed"
main_window->>main_window:21 on_folder_view_filter_changed()
main_window->>app_config:22 
fm_app_config_save_config_for_path(show_hidden=0)
tab_page->>side_panel:23 fm_side_pane_set_show_hidden(0)
side_panel->>side_panel:24 fm_dir_tree_view_set_property(0)
side_panel->>side_panel:25 fm_dir_tree_model_set_show_hidden(0)
side_panel->>side_panel:26 item_hide_hidden_children()
side_panel->>tab_page:27 show_hidden=0
side_panel->>gtk:28 g_signal_emit("CHDIR")
gtk->>main_window:29 signal "CHDIR"
main_window->>main_window:30 on_side_pane_chdir()
main_window->>main_window:31 fm_tab_page_chdir()
side_panel->>side_panel:32 gtk_tree_model_get_path(item iterator)
side_panel->>side_panel:33 fm_dir_tree_model_load_row(item iterator)
```

In this diagram, at step 6 folders gets **iterator**, which will be used at 
steps 32 and 33, but this iterator is already invalid, because at step 26 
hidden directories will be removed from side panel. This may cause a 
segfault.
So, I have started to think about how should look gtk2 API(in non-C 
language, for GtkTreeIter, as a small example) to prevent such issues, 
given those requirements:
1. usage of ffi calls to gtk2 library(nobody wants to reimplement a wheel, 
right?);
2. When GtkTreeIter is in the scope, it should be impossible to add/delete 
content to/from GtkTreeView;
3. gtk is not thread-safe library, so don't bother with it in API for now.

Initially, I thought that linear types may be helpful here, but then, I had 
realized, that g_signal_emit() is ffi call, which calls another signal 
handler, which and I doubt, that linear types will be able to track such 
behavior.
Here is, obviously incorrect snippet(due to my lack of knowledge of ATS2):
extern fn g_signal_emit(string): void = "ext#"
extern fn g_signal_connect(name: string, handler: ptr->void, ptr): void = 
"ext#"

fn handler(tree: ptr): void =
  let
val () = gtk_tree_view_delete_by_index(tree, 0) (* for simplicity, 
let's consider, that this is how it is being deleted *)

implement main0(argc,argv) =
  let
val (tvpf1 | tv) = gtk_tree_view_new_with_model ()
(* insert 1 row into tree view *)
val () = g_signal_connect( "CHDIR", handler, tv)
val (p | iter) = gtk_tree_selection_get_selected( tvpf1 | tv) (* get 
iterator on a row 0 *)
val () = g_signal_emit( "CHDIR") (* handler will delete row 0 *)
val (p | iter) = gtk_tree_model_get_path( p | iter) (* iter is invalid 
here, can ats catch this? *)
  in
  end

So I came to conclusion, that (with my skills), only 
Haskell/Idris/Agda(/Coq?) way of referential transparency is the only way 
to prevent such errors by allowing side effects only inside `IO` "actions". 
Example solution in Haskell (not compilable, just to get the idea):
Iterator.hs:
module Iterator
  ( IteratorM -- constructor is not being exported - IteratorM values can 
only be created inside this module
  , Iterator
  , gtk_tree_selection_with_selected
  , gtk_tree_model_get_path
  ) where
import Foreign.Ptr
import GtkTreeView

newtype Iterator = Iterator (Ptr ())

newtype IteratorM a = IteratorM 
{
runIterator :: IO a
}

-- just 
instance Monad IteratorM where
(>>=) (IteratorM left) second = IteratorM $
left >>= \arg->
case second arg of
IteratorM next-> next 
 

Re: Referential transparency in ATS

[Brandon Barker]

Thanks, Dambaev, for the excellent explanation.



On Sunday, May 5, 2019 at 1:48:48 PM UTC-4, Dambaev Alexander wrote:
>
>
>
>> Admittedly I don't really understand what RT is, but from what I 
>> understand, in Haskell the expression like [print "ha"] is basically a 
>> command to the top-level interpreter (which is the language runtime) to 
>> perform an effect on the console (moreover, it will be evaluated on 
>> as-needed basis).
>>
>
>>
>> I like to imagine an interpreter that sits in the Haskell's runtime. 
>> Values of IO type are commands to this interpreter. Typical Haskell 
>> IO-based programs are building up these commands as they are being 
>> evaluated by the runtime. The runtime starts evaluation at the "main" 
>> expression defined by the programmer.
>>
>
> You are describing "Free-monad", which is an AST interpreter in runtime, 
> but the actual *IO-action* in haskell is
>
> newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #))
>
> which means, that Haskell models IO as "some function, that takes 
> RealWorld state, possibly modifies it and returns new RealWorld state and 
> some value",
> `newtype` is a compile-time abstraction, which will be optimized out and 
> will be represented as a field, which is a function.
> State# is a `primitive` datatype (provided by runtime)
> (# #) is a primitive tuple
>
> So when you write
> main :: IO ()
> main = putStrLn "hello"
>
> it is actually a function, that needs `State# RealWorld` value in order to 
> produce value of type () (unit):
> putStrLn :: String-> IO ()
> putStrLn str = IO $ \state0->
>   case ffi_call_to_putStrLn str of
> IO next-> -- here we bind function of `ffi_call_to_putStrLn` as `next`
>   case next state0 of -- evaluate `next` here as it now has `s` 
> argument
> (# state1, () #) -> (# state1, () #) -- force evaluation of 
> `next`, as this pattern match is strict
>
> main :: IO ()
> main = IO $ \state0->
>   case putStrLn "hello" of
> IO next-> -- here we bind function of `putStrLn` as `next`
>   case next state0 of -- evaluate `next` here as it now has `s` 
> argument
> (# state1, () #)-> (# state1, () #) -- force evaluation of 
> `next`, as this pattern match is strict
>
>
> Moreover, the ";" is itself another comand, the explicit sequencing 
>> command, the meaning of which is "perform the left-hand side effects, then 
>> perform the right-hand side effects". Such a command is a value, so it can 
>> be passed as a value and reused as many times as is necessary. In ATS, the 
>> expression like [print "ha"] evaluates right there to a void/"no value", 
>> and the ";" is also NOT a value at all, but rather a "shortcut" syntax to a 
>> "let-in-end" form.
>>
>
> In haskell, this is (>>=) (bind) function:
>
> class Monad base where
>   (>>=) :: base left_type-> (left_type-> base right_type)-> base right_type
>   (>>) :: base left_type-> (left_type-> base right_type)-> base right_type
>   (>>) first second = first >>= \_ -> second
>
> instance Monad IO where
>   (>>=) (IO first) second = IO $ \state0->
> case first state0 of
>   (# state1, first_value #)->
> case second first_value of
>   IO next->
> next state1
> 
> And thus, in haskell:
>
> main = do
>   let shortcut = putStrLn "hello"
>   shortcut
>   shortcut
> will print "hello" twice, as shortcut is a function, which needs 1 
> argument to be evaluated. Desugared version:
>
> main =
>   let shortcut = putStrLn "hello" in 
>   shortcut >> shortcut
>
> which is:
> main = IO $ \state0->
>   let shortcut = putStrLn "hello" in
>   case (shortcut >> shortcut) state0 of
> (# state1, () #)-> (# state1, () #)
> So, being pure, Haskell pretends that "program is started with some 
> unknown RealWorld state of value0 and each IO action modifies this state 
> and thus, this value is unique for all expressions and thus. complier 
> should evaluate them all instead of caching result of the first evaluation 
> of `hostcut`"
>
>
>  
>

-- 
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 post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/e7795895-6198-4c2a-a7d2-76ab9183905a%40googlegroups.com.

Re: Referential transparency in ATS

[Dambaev Alexander]

>
> So, being pure, Haskell pretends that "program is started with some 
> unknown RealWorld state of value0 and each IO action modifies this state 
> and thus, this value is unique for all expressions and thus. complier 
> should evaluate them all instead of caching result of the first evaluation 
> of `hostcut`"
>
`shortcut` 

-- 
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 post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/9d27ea26-332e-4f31-a28e-a78e4e66aa10%40googlegroups.com.

Re: Referential transparency in ATS

[Dambaev Alexander]

>
> Admittedly I don't really understand what RT is, but from what I 
> understand, in Haskell the expression like [print "ha"] is basically a 
> command to the top-level interpreter (which is the language runtime) to 
> perform an effect on the console (moreover, it will be evaluated on 
> as-needed basis).
>

>
> I like to imagine an interpreter that sits in the Haskell's runtime. 
> Values of IO type are commands to this interpreter. Typical Haskell 
> IO-based programs are building up these commands as they are being 
> evaluated by the runtime. The runtime starts evaluation at the "main" 
> expression defined by the programmer.
>

You are describing "Free-monad", which is an AST interpreter in runtime, 
but the actual *IO-action* in haskell is

newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #))

which means, that Haskell models IO as "some function, that takes RealWorld 
state, possibly modifies it and returns new RealWorld state and some value",
`newtype` is a compile-time abstraction, which will be optimized out and 
will be represented as a field, which is a function.
State# is a `primitive` datatype (provided by runtime)
(# #) is a primitive tuple

So when you write
main :: IO ()
main = putStrLn "hello"

it is actually a function, that needs `State# RealWorld` value in order to 
produce value of type () (unit):
putStrLn :: String-> IO ()
putStrLn str = IO $ \state0->
  case ffi_call_to_putStrLn str of
IO next-> -- here we bind function of `ffi_call_to_putStrLn` as `next`
  case next state0 of -- evaluate `next` here as it now has `s` argument
(# state1, () #) -> (# state1, () #) -- force evaluation of `next`, 
as this pattern match is strict

main :: IO ()
main = IO $ \state0->
  case putStrLn "hello" of
IO next-> -- here we bind function of `putStrLn` as `next`
  case next state0 of -- evaluate `next` here as it now has `s` argument
(# state1, () #)-> (# state1, () #) -- force evaluation of `next`, 
as this pattern match is strict


Moreover, the ";" is itself another comand, the explicit sequencing 
> command, the meaning of which is "perform the left-hand side effects, then 
> perform the right-hand side effects". Such a command is a value, so it can 
> be passed as a value and reused as many times as is necessary. In ATS, the 
> expression like [print "ha"] evaluates right there to a void/"no value", 
> and the ";" is also NOT a value at all, but rather a "shortcut" syntax to a 
> "let-in-end" form.
>

In haskell, this is (>>=) (bind) function:

class Monad base where
  (>>=) :: base left_type-> (left_type-> base right_type)-> base right_type
  (>>) :: base left_type-> (left_type-> base right_type)-> base right_type
  (>>) first second = first >>= \_ -> second

instance Monad IO where
  (>>=) (IO first) second = IO $ \state0->
case first state0 of
  (# state1, first_value #)->
case second first_value of
  IO next->
next state1

And thus, in haskell:

main = do
  let shortcut = putStrLn "hello"
  shortcut
  shortcut
will print "hello" twice, as shortcut is a function, which needs 1 argument 
to be evaluated. Desugared version:

main =
  let shortcut = putStrLn "hello" in 
  shortcut >> shortcut

which is:
main = IO $ \state0->
  let shortcut = putStrLn "hello" in
  case (shortcut >> shortcut) state0 of
(# state1, () #)-> (# state1, () #)
So, being pure, Haskell pretends that "program is started with some unknown 
RealWorld state of value0 and each IO action modifies this state and thus, 
this value is unique for all expressions and thus. complier should evaluate 
them all instead of caching result of the first evaluation of `hostcut`"


 

-- 
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 post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/a6a6c026-9659-413a-895e-485249ecc6a1%40googlegroups.com.

Re: Referential transparency in ATS

[Artyom Shalkhakov]

On Tuesday, March 26, 2019 at 5:14:34 PM UTC+2, gmhwxi wrote:
>
> Boxing is removed:
>
> https://pastebin.com/JacNgK2t
>
> Some hacks are used to make it work...
>
>
This is awesome. Now we don't need to allocate every time we call a 'read' 
function. :)

Thanks! I've updated my gist with this and a note.
 

>
>
> On Tue, Mar 26, 2019 at 10:14 AM Hongwei Xi  > wrote:
>
>> >>Did you mean to use vtype in {a,b:vtype} here? Or not?
>>
>> Typo: vtype should be vt@ype. 
>>
>> On Tue, Mar 26, 2019 at 10:12 AM Artyom Shalkhakov > > wrote:
>>
>>> On Tuesday, March 26, 2019 at 4:07:38 PM UTC+2, gmhwxi wrote:

 A "standard" solution is to use call-by-reference:

 extern
 fun
 runCommand
 {a:vt@ype}
 (c:Command(a:vt@ype), ? >> a): void


>>> I think we covered this a few months back when Chris asked about it. 
>>> This finally reminded me of that discussion.
>>>  
>>>
 datavtype
 Command(vt@ype) =
   | Nop(unit)
   | Read(string)
   | Print(unit) of string
   | Seq(unit) of (Command(unit), Command(unit))
   | {a,b:vtype} Bind(b) of (Command(a), a?, ( >> a?) - 
 Command(b))

>>>  
>>> Did you mean to use vtype in {a,b:vtype} here? Or not?
>>>  
>>>
 This is a bit more involved but only an implementer like you (not user) 
 needs to deal with it :)

>>>
>>> Hmmm. A sane approach to dependent types is when the user needs none of 
>>> dependent types to get things going. :)
>>>  
>>>
  

>>>
 On Tue, Mar 26, 2019 at 10:01 AM Artyom Shalkhakov <
 artyom.s...@gmail.com> wrote:

> On Tuesday, March 26, 2019 at 3:55:47 PM UTC+2, gmhwxi wrote:
>>
>> >> Now, what about boxing, can we do something with boxing?
>>
>> Do you mean that you want to have 'a:t@ype' instead of 'a:type'?
>>
>>
> Yes. I think any use of 'bind' is highly discouraged if we have 
> 'a:type' restriction (e.g. want to return an int from an effectful 
> function 
> -- sure, but use heap for that...).
>  
>
>> On Tue, Mar 26, 2019 at 9:36 AM Artyom Shalkhakov <
>> artyom.s...@gmail.com> wrote:
>>
>>> Hi Hongwei,
>>>
>>> On Tuesday, March 26, 2019 at 3:22:41 PM UTC+2, gmhwxi wrote:

 Here is a linear version:

 https://pastebin.com/sqXcRhnf

 Also, Command is a linear datatype (i.e., dataviewtype).


>>> Great! Now, what about boxing, can we do something with boxing? I 
>>> expect such code, if it's really used in practice, to involve LOTS of 
>>> these 
>>> little objects. So it will probably behave badly if every call to a 
>>> continuation involves a heap allocation... Let us be a bit more 
>>> resource-conscious, please. :)
>>>
>>> I did a similar example a while back where I used some CPS style to 
>>> get rid of boxing:
>>>
>>> https://github.com/ashalkhakov/tfc/blob/master/src/SATS/cont.sats
>>>
>>> Basically we can 'co-opt' the ATS compiler to do all the plumbing. 
>>> The closure call and its packing is non-uniform but the closure itself 
>>> is 
>>> uniform in size, since it's a pointer to the heap:
>>>
>>> https://github.com/ashalkhakov/tfc/blob/master/test/threads.dats
>>>
>>> To call a continuation, the return type must be statically known (at 
>>> both the callee side and the caller side).
>>>
>>> So maybe we can do something similar here?
>>>  


 On Tue, Mar 26, 2019 at 9:02 AM Hongwei Xi  
 wrote:

> Nice!
>
> But I am very surprised that this code actually works.
> My understanding is that It works because of a bug in patsopt :)
>
> Basically, runCommand should be implemented as a polymorphic 
> function (instead of a function
> template). And 'a:t0ype' should be 'a:type'.
>
> fun runCommand: {a:type} Command(a) -> a
>
> Actually, I think that Command should be a linear type, which 
> should you more fun!
>
> On Tue, Mar 26, 2019 at 5:49 AM Artyom Shalkhakov <
> artyom.s...@gmail.com> wrote:
>
>> I've made a gist:
>>
>>
>> https://gist.github.com/ashalkhakov/c3577e97b20020fde31f84447fd1e056
>>
>> It actually works. It illustrates the basics (sequencing, bind, 
>> input and output). Nice. It doesn't have Haskell's "return" though, 
>> but 
>> that is pretty simple to add (it's something that "creates" IO where 
>> there 
>> is no IO at all...).
>>
>> The interpreter is using a continuation in the end. I chose this 
>> style because the closure-function (i.e. our continuation) can be 
>> passed 
>> around freely, whereas with a flat unboxed type it is sometimes 
>> difficult 
>> for the C 

Re: Referential transparency in ATS

[Hongwei Xi]

Boxing is removed:

https://pastebin.com/JacNgK2t

Some hacks are used to make it work...



On Tue, Mar 26, 2019 at 10:14 AM Hongwei Xi  wrote:

> >>Did you mean to use vtype in {a,b:vtype} here? Or not?
>
> Typo: vtype should be vt@ype.
>
> On Tue, Mar 26, 2019 at 10:12 AM Artyom Shalkhakov <
> artyom.shalkha...@gmail.com> wrote:
>
>> On Tuesday, March 26, 2019 at 4:07:38 PM UTC+2, gmhwxi wrote:
>>>
>>> A "standard" solution is to use call-by-reference:
>>>
>>> extern
>>> fun
>>> runCommand
>>> {a:vt@ype}
>>> (c:Command(a:vt@ype), ? >> a): void
>>>
>>>
>> I think we covered this a few months back when Chris asked about it. This
>> finally reminded me of that discussion.
>>
>>
>>> datavtype
>>> Command(vt@ype) =
>>>   | Nop(unit)
>>>   | Read(string)
>>>   | Print(unit) of string
>>>   | Seq(unit) of (Command(unit), Command(unit))
>>>   | {a,b:vtype} Bind(b) of (Command(a), a?, ( >> a?) -
>>> Command(b))
>>>
>>
>> Did you mean to use vtype in {a,b:vtype} here? Or not?
>>
>>
>>> This is a bit more involved but only an implementer like you (not user)
>>> needs to deal with it :)
>>>
>>
>> Hmmm. A sane approach to dependent types is when the user needs none of
>> dependent types to get things going. :)
>>
>>
>>>
>>>
>>
>>> On Tue, Mar 26, 2019 at 10:01 AM Artyom Shalkhakov <
>>> artyom.s...@gmail.com> wrote:
>>>
 On Tuesday, March 26, 2019 at 3:55:47 PM UTC+2, gmhwxi wrote:
>
> >> Now, what about boxing, can we do something with boxing?
>
> Do you mean that you want to have 'a:t@ype' instead of 'a:type'?
>
>
 Yes. I think any use of 'bind' is highly discouraged if we have
 'a:type' restriction (e.g. want to return an int from an effectful function
 -- sure, but use heap for that...).


> On Tue, Mar 26, 2019 at 9:36 AM Artyom Shalkhakov <
> artyom.s...@gmail.com> wrote:
>
>> Hi Hongwei,
>>
>> On Tuesday, March 26, 2019 at 3:22:41 PM UTC+2, gmhwxi wrote:
>>>
>>> Here is a linear version:
>>>
>>> https://pastebin.com/sqXcRhnf
>>>
>>> Also, Command is a linear datatype (i.e., dataviewtype).
>>>
>>>
>> Great! Now, what about boxing, can we do something with boxing? I
>> expect such code, if it's really used in practice, to involve LOTS of 
>> these
>> little objects. So it will probably behave badly if every call to a
>> continuation involves a heap allocation... Let us be a bit more
>> resource-conscious, please. :)
>>
>> I did a similar example a while back where I used some CPS style to
>> get rid of boxing:
>>
>> https://github.com/ashalkhakov/tfc/blob/master/src/SATS/cont.sats
>>
>> Basically we can 'co-opt' the ATS compiler to do all the plumbing.
>> The closure call and its packing is non-uniform but the closure itself is
>> uniform in size, since it's a pointer to the heap:
>>
>> https://github.com/ashalkhakov/tfc/blob/master/test/threads.dats
>>
>> To call a continuation, the return type must be statically known (at
>> both the callee side and the caller side).
>>
>> So maybe we can do something similar here?
>>
>>>
>>>
>>> On Tue, Mar 26, 2019 at 9:02 AM Hongwei Xi  wrote:
>>>
 Nice!

 But I am very surprised that this code actually works.
 My understanding is that It works because of a bug in patsopt :)

 Basically, runCommand should be implemented as a polymorphic
 function (instead of a function
 template). And 'a:t0ype' should be 'a:type'.

 fun runCommand: {a:type} Command(a) -> a

 Actually, I think that Command should be a linear type, which
 should you more fun!

 On Tue, Mar 26, 2019 at 5:49 AM Artyom Shalkhakov <
 artyom.s...@gmail.com> wrote:

> I've made a gist:
>
>
> https://gist.github.com/ashalkhakov/c3577e97b20020fde31f84447fd1e056
>
> It actually works. It illustrates the basics (sequencing, bind,
> input and output). Nice. It doesn't have Haskell's "return" though, 
> but
> that is pretty simple to add (it's something that "creates" IO where 
> there
> is no IO at all...).
>
> The interpreter is using a continuation in the end. I chose this
> style because the closure-function (i.e. our continuation) can be 
> passed
> around freely, whereas with a flat unboxed type it is sometimes 
> difficult
> for the C compiler to figure out the size of the variable.
>
> On Tuesday, March 26, 2019 at 10:11:11 AM UTC+2, Artyom Shalkhakov
> wrote:
>
>> Hi Brandon,
>>
>> On Friday, March 22, 2019 at 8:49:29 PM UTC+2, Brandon Barker
>> wrote:
>>>
>>> Hey Artyom,
>>>
>>> Thanks for the very interesting analysis and response.

Re: Referential transparency in ATS

[Hongwei Xi]

>>Did you mean to use vtype in {a,b:vtype} here? Or not?

Typo: vtype should be vt@ype.

On Tue, Mar 26, 2019 at 10:12 AM Artyom Shalkhakov <
artyom.shalkha...@gmail.com> wrote:

> On Tuesday, March 26, 2019 at 4:07:38 PM UTC+2, gmhwxi wrote:
>>
>> A "standard" solution is to use call-by-reference:
>>
>> extern
>> fun
>> runCommand
>> {a:vt@ype}
>> (c:Command(a:vt@ype), ? >> a): void
>>
>>
> I think we covered this a few months back when Chris asked about it. This
> finally reminded me of that discussion.
>
>
>> datavtype
>> Command(vt@ype) =
>>   | Nop(unit)
>>   | Read(string)
>>   | Print(unit) of string
>>   | Seq(unit) of (Command(unit), Command(unit))
>>   | {a,b:vtype} Bind(b) of (Command(a), a?, ( >> a?) -
>> Command(b))
>>
>
> Did you mean to use vtype in {a,b:vtype} here? Or not?
>
>
>> This is a bit more involved but only an implementer like you (not user)
>> needs to deal with it :)
>>
>
> Hmmm. A sane approach to dependent types is when the user needs none of
> dependent types to get things going. :)
>
>
>>
>>
>
>> On Tue, Mar 26, 2019 at 10:01 AM Artyom Shalkhakov 
>> wrote:
>>
>>> On Tuesday, March 26, 2019 at 3:55:47 PM UTC+2, gmhwxi wrote:

 >> Now, what about boxing, can we do something with boxing?

 Do you mean that you want to have 'a:t@ype' instead of 'a:type'?


>>> Yes. I think any use of 'bind' is highly discouraged if we have 'a:type'
>>> restriction (e.g. want to return an int from an effectful function -- sure,
>>> but use heap for that...).
>>>
>>>
 On Tue, Mar 26, 2019 at 9:36 AM Artyom Shalkhakov <
 artyom.s...@gmail.com> wrote:

> Hi Hongwei,
>
> On Tuesday, March 26, 2019 at 3:22:41 PM UTC+2, gmhwxi wrote:
>>
>> Here is a linear version:
>>
>> https://pastebin.com/sqXcRhnf
>>
>> Also, Command is a linear datatype (i.e., dataviewtype).
>>
>>
> Great! Now, what about boxing, can we do something with boxing? I
> expect such code, if it's really used in practice, to involve LOTS of 
> these
> little objects. So it will probably behave badly if every call to a
> continuation involves a heap allocation... Let us be a bit more
> resource-conscious, please. :)
>
> I did a similar example a while back where I used some CPS style to
> get rid of boxing:
>
> https://github.com/ashalkhakov/tfc/blob/master/src/SATS/cont.sats
>
> Basically we can 'co-opt' the ATS compiler to do all the plumbing. The
> closure call and its packing is non-uniform but the closure itself is
> uniform in size, since it's a pointer to the heap:
>
> https://github.com/ashalkhakov/tfc/blob/master/test/threads.dats
>
> To call a continuation, the return type must be statically known (at
> both the callee side and the caller side).
>
> So maybe we can do something similar here?
>
>>
>>
>> On Tue, Mar 26, 2019 at 9:02 AM Hongwei Xi  wrote:
>>
>>> Nice!
>>>
>>> But I am very surprised that this code actually works.
>>> My understanding is that It works because of a bug in patsopt :)
>>>
>>> Basically, runCommand should be implemented as a polymorphic
>>> function (instead of a function
>>> template). And 'a:t0ype' should be 'a:type'.
>>>
>>> fun runCommand: {a:type} Command(a) -> a
>>>
>>> Actually, I think that Command should be a linear type, which should
>>> you more fun!
>>>
>>> On Tue, Mar 26, 2019 at 5:49 AM Artyom Shalkhakov <
>>> artyom.s...@gmail.com> wrote:
>>>
 I've made a gist:

 https://gist.github.com/ashalkhakov/c3577e97b20020fde31f84447fd1e056

 It actually works. It illustrates the basics (sequencing, bind,
 input and output). Nice. It doesn't have Haskell's "return" though, but
 that is pretty simple to add (it's something that "creates" IO where 
 there
 is no IO at all...).

 The interpreter is using a continuation in the end. I chose this
 style because the closure-function (i.e. our continuation) can be 
 passed
 around freely, whereas with a flat unboxed type it is sometimes 
 difficult
 for the C compiler to figure out the size of the variable.

 On Tuesday, March 26, 2019 at 10:11:11 AM UTC+2, Artyom Shalkhakov
 wrote:

> Hi Brandon,
>
> On Friday, March 22, 2019 at 8:49:29 PM UTC+2, Brandon Barker
> wrote:
>>
>> Hey Artyom,
>>
>> Thanks for the very interesting analysis and response.
>>
>>
> Glad you found it useful!
>
> On Fri, Mar 22, 2019 at 4:06 AM Artyom Shalkhakov <
>> artyom.s...@gmail.com> wrote:
>>
>>> Hi Brandon,
>>>
>>> This is a very lively discussion, thanks for bringing it up.
>>>
>>> On Friday, March 22, 2019 

Re: Referential transparency in ATS

[Artyom Shalkhakov]

On Tuesday, March 26, 2019 at 4:07:38 PM UTC+2, gmhwxi wrote:
>
> A "standard" solution is to use call-by-reference:
>
> extern
> fun
> runCommand
> {a:vt@ype}
> (c:Command(a:vt@ype), ? >> a): void
>
>
I think we covered this a few months back when Chris asked about it. This 
finally reminded me of that discussion.
 

> datavtype
> Command(vt@ype) =
>   | Nop(unit)
>   | Read(string)
>   | Print(unit) of string
>   | Seq(unit) of (Command(unit), Command(unit))
>   | {a,b:vtype} Bind(b) of (Command(a), a?, ( >> a?) - 
> Command(b))
>
 
Did you mean to use vtype in {a,b:vtype} here? Or not?
 

> This is a bit more involved but only an implementer like you (not user) 
> needs to deal with it :)
>

Hmmm. A sane approach to dependent types is when the user needs none of 
dependent types to get things going. :)
 

>  
>

> On Tue, Mar 26, 2019 at 10:01 AM Artyom Shalkhakov  > wrote:
>
>> On Tuesday, March 26, 2019 at 3:55:47 PM UTC+2, gmhwxi wrote:
>>>
>>> >> Now, what about boxing, can we do something with boxing?
>>>
>>> Do you mean that you want to have 'a:t@ype' instead of 'a:type'?
>>>
>>>
>> Yes. I think any use of 'bind' is highly discouraged if we have 'a:type' 
>> restriction (e.g. want to return an int from an effectful function -- sure, 
>> but use heap for that...).
>>  
>>
>>> On Tue, Mar 26, 2019 at 9:36 AM Artyom Shalkhakov  
>>> wrote:
>>>
 Hi Hongwei,

 On Tuesday, March 26, 2019 at 3:22:41 PM UTC+2, gmhwxi wrote:
>
> Here is a linear version:
>
> https://pastebin.com/sqXcRhnf
>
> Also, Command is a linear datatype (i.e., dataviewtype).
>
>
 Great! Now, what about boxing, can we do something with boxing? I 
 expect such code, if it's really used in practice, to involve LOTS of 
 these 
 little objects. So it will probably behave badly if every call to a 
 continuation involves a heap allocation... Let us be a bit more 
 resource-conscious, please. :)

 I did a similar example a while back where I used some CPS style to get 
 rid of boxing:

 https://github.com/ashalkhakov/tfc/blob/master/src/SATS/cont.sats

 Basically we can 'co-opt' the ATS compiler to do all the plumbing. The 
 closure call and its packing is non-uniform but the closure itself is 
 uniform in size, since it's a pointer to the heap:

 https://github.com/ashalkhakov/tfc/blob/master/test/threads.dats

 To call a continuation, the return type must be statically known (at 
 both the callee side and the caller side).

 So maybe we can do something similar here?
  
>
>
> On Tue, Mar 26, 2019 at 9:02 AM Hongwei Xi  wrote:
>
>> Nice!
>>
>> But I am very surprised that this code actually works.
>> My understanding is that It works because of a bug in patsopt :)
>>
>> Basically, runCommand should be implemented as a polymorphic function 
>> (instead of a function
>> template). And 'a:t0ype' should be 'a:type'.
>>
>> fun runCommand: {a:type} Command(a) -> a
>>
>> Actually, I think that Command should be a linear type, which should 
>> you more fun!
>>
>> On Tue, Mar 26, 2019 at 5:49 AM Artyom Shalkhakov <
>> artyom.s...@gmail.com> wrote:
>>
>>> I've made a gist:
>>>
>>> https://gist.github.com/ashalkhakov/c3577e97b20020fde31f84447fd1e056
>>>
>>> It actually works. It illustrates the basics (sequencing, bind, 
>>> input and output). Nice. It doesn't have Haskell's "return" though, but 
>>> that is pretty simple to add (it's something that "creates" IO where 
>>> there 
>>> is no IO at all...).
>>>
>>> The interpreter is using a continuation in the end. I chose this 
>>> style because the closure-function (i.e. our continuation) can be 
>>> passed 
>>> around freely, whereas with a flat unboxed type it is sometimes 
>>> difficult 
>>> for the C compiler to figure out the size of the variable.
>>>
>>> On Tuesday, March 26, 2019 at 10:11:11 AM UTC+2, Artyom Shalkhakov 
>>> wrote:
>>>
 Hi Brandon,

 On Friday, March 22, 2019 at 8:49:29 PM UTC+2, Brandon Barker wrote:
>
> Hey Artyom,
>
> Thanks for the very interesting analysis and response.
>
>
 Glad you found it useful!

 On Fri, Mar 22, 2019 at 4:06 AM Artyom Shalkhakov <
> artyom.s...@gmail.com> wrote:
>
>> Hi Brandon,
>>
>> This is a very lively discussion, thanks for bringing it up.
>>
>> On Friday, March 22, 2019 at 5:48:07 AM UTC+2, Brandon Barker 
>> wrote:
>>>
>>> And for what it's worth, here is an Idris program for haha using 
>>> Effects:
>>>
>>> module Main
>>>
>>>
>>> import Effects
>>> import Effect.StdIO
>>>
>>>
>>> hello : Eff () 

Re: Referential transparency in ATS

[Artyom Shalkhakov]

On Tuesday, March 26, 2019 at 3:55:47 PM UTC+2, gmhwxi wrote:
>
> >> Now, what about boxing, can we do something with boxing?
>
> Do you mean that you want to have 'a:t@ype' instead of 'a:type'?
>
>
Yes. I think any use of 'bind' is highly discouraged if we have 'a:type' 
restriction (e.g. want to return an int from an effectful function -- sure, 
but use heap for that...).
 

> On Tue, Mar 26, 2019 at 9:36 AM Artyom Shalkhakov  > wrote:
>
>> Hi Hongwei,
>>
>> On Tuesday, March 26, 2019 at 3:22:41 PM UTC+2, gmhwxi wrote:
>>>
>>> Here is a linear version:
>>>
>>> https://pastebin.com/sqXcRhnf
>>>
>>> Also, Command is a linear datatype (i.e., dataviewtype).
>>>
>>>
>> Great! Now, what about boxing, can we do something with boxing? I expect 
>> such code, if it's really used in practice, to involve LOTS of these little 
>> objects. So it will probably behave badly if every call to a continuation 
>> involves a heap allocation... Let us be a bit more resource-conscious, 
>> please. :)
>>
>> I did a similar example a while back where I used some CPS style to get 
>> rid of boxing:
>>
>> https://github.com/ashalkhakov/tfc/blob/master/src/SATS/cont.sats
>>
>> Basically we can 'co-opt' the ATS compiler to do all the plumbing. The 
>> closure call and its packing is non-uniform but the closure itself is 
>> uniform in size, since it's a pointer to the heap:
>>
>> https://github.com/ashalkhakov/tfc/blob/master/test/threads.dats
>>
>> To call a continuation, the return type must be statically known (at both 
>> the callee side and the caller side).
>>
>> So maybe we can do something similar here?
>>  
>>>
>>>
>>> On Tue, Mar 26, 2019 at 9:02 AM Hongwei Xi  wrote:
>>>
 Nice!

 But I am very surprised that this code actually works.
 My understanding is that It works because of a bug in patsopt :)

 Basically, runCommand should be implemented as a polymorphic function 
 (instead of a function
 template). And 'a:t0ype' should be 'a:type'.

 fun runCommand: {a:type} Command(a) -> a

 Actually, I think that Command should be a linear type, which should 
 you more fun!

 On Tue, Mar 26, 2019 at 5:49 AM Artyom Shalkhakov <
 artyom.s...@gmail.com> wrote:

> I've made a gist:
>
> https://gist.github.com/ashalkhakov/c3577e97b20020fde31f84447fd1e056
>
> It actually works. It illustrates the basics (sequencing, bind, input 
> and output). Nice. It doesn't have Haskell's "return" though, but that is 
> pretty simple to add (it's something that "creates" IO where there is no 
> IO 
> at all...).
>
> The interpreter is using a continuation in the end. I chose this style 
> because the closure-function (i.e. our continuation) can be passed around 
> freely, whereas with a flat unboxed type it is sometimes difficult for 
> the 
> C compiler to figure out the size of the variable.
>
> On Tuesday, March 26, 2019 at 10:11:11 AM UTC+2, Artyom Shalkhakov 
> wrote:
>
>> Hi Brandon,
>>
>> On Friday, March 22, 2019 at 8:49:29 PM UTC+2, Brandon Barker wrote:
>>>
>>> Hey Artyom,
>>>
>>> Thanks for the very interesting analysis and response.
>>>
>>>
>> Glad you found it useful!
>>
>> On Fri, Mar 22, 2019 at 4:06 AM Artyom Shalkhakov <
>>> artyom.s...@gmail.com> wrote:
>>>
 Hi Brandon,

 This is a very lively discussion, thanks for bringing it up.

 On Friday, March 22, 2019 at 5:48:07 AM UTC+2, Brandon Barker wrote:
>
> And for what it's worth, here is an Idris program for haha using 
> Effects:
>
> module Main
>
>
> import Effects
> import Effect.StdIO
>
>
> hello : Eff () [STDIO]
> hello = let ha = StdIO.putStr "ha" in ha *> ha
>
>
> main : IO ()
> main = run hello
>
>
>
> It prints "ha" twice, despite being a strict language. I presume, 
> but am not sure, this is because the effect time requires it to be 
> re-evaluated each time.
>
>
>
 Well, the type of "hello" says that the computation will use the 
 STDIO effect as many times as is necessary. The way the computation is 
 constructed, it is meant to issue commands in a given sequence.

 One peculiarity of PureScript is that of handling effects via the 
 algebraic effects approach. It's not easy to do in a high-performance 
 way, 
 because you need a call/cc construct present in the language, and 
 moreover 
 a 'multi-shot' one at that (i.e. the continuation *may* be invoked 
 zero, 
 once or more times by the effect interpreter). In ATS a simpler way is 
 to 
 use template functions to define effects differently (e.g. during 
 

Re: Referential transparency in ATS

[Hongwei Xi]

>> Now, what about boxing, can we do something with boxing?

Do you mean that you want to have 'a:t@ype' instead of 'a:type'?

On Tue, Mar 26, 2019 at 9:36 AM Artyom Shalkhakov <
artyom.shalkha...@gmail.com> wrote:

> Hi Hongwei,
>
> On Tuesday, March 26, 2019 at 3:22:41 PM UTC+2, gmhwxi wrote:
>>
>> Here is a linear version:
>>
>> https://pastebin.com/sqXcRhnf
>>
>> Also, Command is a linear datatype (i.e., dataviewtype).
>>
>>
> Great! Now, what about boxing, can we do something with boxing? I expect
> such code, if it's really used in practice, to involve LOTS of these little
> objects. So it will probably behave badly if every call to a continuation
> involves a heap allocation... Let us be a bit more resource-conscious,
> please. :)
>
> I did a similar example a while back where I used some CPS style to get
> rid of boxing:
>
> https://github.com/ashalkhakov/tfc/blob/master/src/SATS/cont.sats
>
> Basically we can 'co-opt' the ATS compiler to do all the plumbing. The
> closure call and its packing is non-uniform but the closure itself is
> uniform in size, since it's a pointer to the heap:
>
> https://github.com/ashalkhakov/tfc/blob/master/test/threads.dats
>
> To call a continuation, the return type must be statically known (at both
> the callee side and the caller side).
>
> So maybe we can do something similar here?
>
>>
>>
>> On Tue, Mar 26, 2019 at 9:02 AM Hongwei Xi  wrote:
>>
>>> Nice!
>>>
>>> But I am very surprised that this code actually works.
>>> My understanding is that It works because of a bug in patsopt :)
>>>
>>> Basically, runCommand should be implemented as a polymorphic function
>>> (instead of a function
>>> template). And 'a:t0ype' should be 'a:type'.
>>>
>>> fun runCommand: {a:type} Command(a) -> a
>>>
>>> Actually, I think that Command should be a linear type, which should you
>>> more fun!
>>>
>>> On Tue, Mar 26, 2019 at 5:49 AM Artyom Shalkhakov 
>>> wrote:
>>>
 I've made a gist:

 https://gist.github.com/ashalkhakov/c3577e97b20020fde31f84447fd1e056

 It actually works. It illustrates the basics (sequencing, bind, input
 and output). Nice. It doesn't have Haskell's "return" though, but that is
 pretty simple to add (it's something that "creates" IO where there is no IO
 at all...).

 The interpreter is using a continuation in the end. I chose this style
 because the closure-function (i.e. our continuation) can be passed around
 freely, whereas with a flat unboxed type it is sometimes difficult for the
 C compiler to figure out the size of the variable.

 On Tuesday, March 26, 2019 at 10:11:11 AM UTC+2, Artyom Shalkhakov
 wrote:

> Hi Brandon,
>
> On Friday, March 22, 2019 at 8:49:29 PM UTC+2, Brandon Barker wrote:
>>
>> Hey Artyom,
>>
>> Thanks for the very interesting analysis and response.
>>
>>
> Glad you found it useful!
>
> On Fri, Mar 22, 2019 at 4:06 AM Artyom Shalkhakov <
>> artyom.s...@gmail.com> wrote:
>>
>>> Hi Brandon,
>>>
>>> This is a very lively discussion, thanks for bringing it up.
>>>
>>> On Friday, March 22, 2019 at 5:48:07 AM UTC+2, Brandon Barker wrote:

 And for what it's worth, here is an Idris program for haha using
 Effects:

 module Main


 import Effects
 import Effect.StdIO


 hello : Eff () [STDIO]
 hello = let ha = StdIO.putStr "ha" in ha *> ha


 main : IO ()
 main = run hello



 It prints "ha" twice, despite being a strict language. I presume,
 but am not sure, this is because the effect time requires it to be
 re-evaluated each time.



>>> Well, the type of "hello" says that the computation will use the
>>> STDIO effect as many times as is necessary. The way the computation is
>>> constructed, it is meant to issue commands in a given sequence.
>>>
>>> One peculiarity of PureScript is that of handling effects via the
>>> algebraic effects approach. It's not easy to do in a high-performance 
>>> way,
>>> because you need a call/cc construct present in the language, and 
>>> moreover
>>> a 'multi-shot' one at that (i.e. the continuation *may* be invoked zero,
>>> once or more times by the effect interpreter). In ATS a simpler way is 
>>> to
>>> use template functions to define effects differently (e.g. during 
>>> testing
>>> and during the actual execution) -- it's constrained compared to the
>>> call/cc for sure, but then you don't have to pay the price of the 
>>> call/cc
>>> plumbing. Another thing about PureScript is that it uses row types to 
>>> track
>>> the set of effects that a given Eff computation may involve during its
>>> evaluation.
>>>
>>
>> Not that it will invalidate anything you just 

Re: Referential transparency in ATS

[Artyom Shalkhakov]

On Tuesday, March 26, 2019 at 3:02:42 PM UTC+2, gmhwxi wrote:
>
> Nice!
>
> But I am very surprised that this code actually works.
> My understanding is that It works because of a bug in patsopt :)
>
>
May I suggest this bug to be classified as a feature. :)

Basically, runCommand should be implemented as a polymorphic function 
> (instead of a function
> template). And 'a:t0ype' should be 'a:type'.
>
> fun runCommand: {a:type} Command(a) -> a
>
> Actually, I think that Command should be a linear type, which should you 
> more fun!
>
> On Tue, Mar 26, 2019 at 5:49 AM Artyom Shalkhakov  > wrote:
>
>> I've made a gist:
>>
>> https://gist.github.com/ashalkhakov/c3577e97b20020fde31f84447fd1e056
>>
>> It actually works. It illustrates the basics (sequencing, bind, input and 
>> output). Nice. It doesn't have Haskell's "return" though, but that is 
>> pretty simple to add (it's something that "creates" IO where there is no IO 
>> at all...).
>>
>> The interpreter is using a continuation in the end. I chose this style 
>> because the closure-function (i.e. our continuation) can be passed around 
>> freely, whereas with a flat unboxed type it is sometimes difficult for the 
>> C compiler to figure out the size of the variable.
>>
>> On Tuesday, March 26, 2019 at 10:11:11 AM UTC+2, Artyom Shalkhakov wrote:
>>
>>> Hi Brandon,
>>>
>>> On Friday, March 22, 2019 at 8:49:29 PM UTC+2, Brandon Barker wrote:

 Hey Artyom,

 Thanks for the very interesting analysis and response.


>>> Glad you found it useful!
>>>
>>> On Fri, Mar 22, 2019 at 4:06 AM Artyom Shalkhakov  
 wrote:

> Hi Brandon,
>
> This is a very lively discussion, thanks for bringing it up.
>
> On Friday, March 22, 2019 at 5:48:07 AM UTC+2, Brandon Barker wrote:
>>
>> And for what it's worth, here is an Idris program for haha using 
>> Effects:
>>
>> module Main
>>
>>
>> import Effects
>> import Effect.StdIO
>>
>>
>> hello : Eff () [STDIO]
>> hello = let ha = StdIO.putStr "ha" in ha *> ha
>>
>>
>> main : IO ()
>> main = run hello
>>
>>
>>
>> It prints "ha" twice, despite being a strict language. I presume, but 
>> am not sure, this is because the effect time requires it to be 
>> re-evaluated 
>> each time.
>>
>>
>>
> Well, the type of "hello" says that the computation will use the STDIO 
> effect as many times as is necessary. The way the computation is 
> constructed, it is meant to issue commands in a given sequence.
>
> One peculiarity of PureScript is that of handling effects via the 
> algebraic effects approach. It's not easy to do in a high-performance 
> way, 
> because you need a call/cc construct present in the language, and 
> moreover 
> a 'multi-shot' one at that (i.e. the continuation *may* be invoked zero, 
> once or more times by the effect interpreter). In ATS a simpler way is to 
> use template functions to define effects differently (e.g. during testing 
> and during the actual execution) -- it's constrained compared to the 
> call/cc for sure, but then you don't have to pay the price of the call/cc 
> plumbing. Another thing about PureScript is that it uses row types to 
> track 
> the set of effects that a given Eff computation may involve during its 
> evaluation.
>

 Not that it will invalidate anything you just said, but the above code 
 was Idris, but they may be similar in this regard (not sure). I need to 
 look into call/cc more at some point - not very familiar with this idea. 
 But I like where you are going with templates in ATS!

>>>
>>>
>>> Haha, right! I mixed them up. I do remember reading about effects in 
>>> both languages! And I think they are pretty similar, except in Idris, you 
>>> have a type-level list of effects, whereas in PureScript, it is instead a 
>>> row of effects. So, pretty similar from the POV of using it. I think. :)
>>>  
>>>

> So in short, if we view the programs as creating commands, and then 
> some kind of external interpreter that executes them, then it all matches 
> up. The programs might be quite pure and non-side-effecting (except for 
> non-termination aka infinite looping runtime exceptions), the interpreter 
> will perform the effects. Here's a pseudocode for the interpreter:
>
> // the command sub-language
> datatype Command = Print of string | Nop | Seq of (command, command)
> extern
> fun runCommand (c:Command): void
> extern
> fun seq (c:Command, Command): Command
> extern
> fun cprint (s:string): Command
> implement
> seq (c1, c2) = Seq (c1, c2)
> implement
> cprint (s) = Print s
> // the interpreter itself
> implement
> runCommand (c) = case+ c of Nop => (*done!*) | Print s => print (s) | 
> Seq (c1, c2) => (runCommand(c1); 

Re: Referential transparency in ATS

[Artyom Shalkhakov]

Hi Hongwei,

On Tuesday, March 26, 2019 at 3:22:41 PM UTC+2, gmhwxi wrote:
>
> Here is a linear version:
>
> https://pastebin.com/sqXcRhnf
>
> Also, Command is a linear datatype (i.e., dataviewtype).
>
>
Great! Now, what about boxing, can we do something with boxing? I expect 
such code, if it's really used in practice, to involve LOTS of these little 
objects. So it will probably behave badly if every call to a continuation 
involves a heap allocation... Let us be a bit more resource-conscious, 
please. :)

I did a similar example a while back where I used some CPS style to get rid 
of boxing:

https://github.com/ashalkhakov/tfc/blob/master/src/SATS/cont.sats

Basically we can 'co-opt' the ATS compiler to do all the plumbing. The 
closure call and its packing is non-uniform but the closure itself is 
uniform in size, since it's a pointer to the heap:

https://github.com/ashalkhakov/tfc/blob/master/test/threads.dats

To call a continuation, the return type must be statically known (at both 
the callee side and the caller side).

So maybe we can do something similar here?
 
>
>
> On Tue, Mar 26, 2019 at 9:02 AM Hongwei Xi > 
> wrote:
>
>> Nice!
>>
>> But I am very surprised that this code actually works.
>> My understanding is that It works because of a bug in patsopt :)
>>
>> Basically, runCommand should be implemented as a polymorphic function 
>> (instead of a function
>> template). And 'a:t0ype' should be 'a:type'.
>>
>> fun runCommand: {a:type} Command(a) -> a
>>
>> Actually, I think that Command should be a linear type, which should you 
>> more fun!
>>
>> On Tue, Mar 26, 2019 at 5:49 AM Artyom Shalkhakov > > wrote:
>>
>>> I've made a gist:
>>>
>>> https://gist.github.com/ashalkhakov/c3577e97b20020fde31f84447fd1e056
>>>
>>> It actually works. It illustrates the basics (sequencing, bind, input 
>>> and output). Nice. It doesn't have Haskell's "return" though, but that is 
>>> pretty simple to add (it's something that "creates" IO where there is no IO 
>>> at all...).
>>>
>>> The interpreter is using a continuation in the end. I chose this style 
>>> because the closure-function (i.e. our continuation) can be passed around 
>>> freely, whereas with a flat unboxed type it is sometimes difficult for the 
>>> C compiler to figure out the size of the variable.
>>>
>>> On Tuesday, March 26, 2019 at 10:11:11 AM UTC+2, Artyom Shalkhakov wrote:
>>>
 Hi Brandon,

 On Friday, March 22, 2019 at 8:49:29 PM UTC+2, Brandon Barker wrote:
>
> Hey Artyom,
>
> Thanks for the very interesting analysis and response.
>
>
 Glad you found it useful!

 On Fri, Mar 22, 2019 at 4:06 AM Artyom Shalkhakov <
> artyom.s...@gmail.com> wrote:
>
>> Hi Brandon,
>>
>> This is a very lively discussion, thanks for bringing it up.
>>
>> On Friday, March 22, 2019 at 5:48:07 AM UTC+2, Brandon Barker wrote:
>>>
>>> And for what it's worth, here is an Idris program for haha using 
>>> Effects:
>>>
>>> module Main
>>>
>>>
>>> import Effects
>>> import Effect.StdIO
>>>
>>>
>>> hello : Eff () [STDIO]
>>> hello = let ha = StdIO.putStr "ha" in ha *> ha
>>>
>>>
>>> main : IO ()
>>> main = run hello
>>>
>>>
>>>
>>> It prints "ha" twice, despite being a strict language. I presume, 
>>> but am not sure, this is because the effect time requires it to be 
>>> re-evaluated each time.
>>>
>>>
>>>
>> Well, the type of "hello" says that the computation will use the 
>> STDIO effect as many times as is necessary. The way the computation is 
>> constructed, it is meant to issue commands in a given sequence.
>>
>> One peculiarity of PureScript is that of handling effects via the 
>> algebraic effects approach. It's not easy to do in a high-performance 
>> way, 
>> because you need a call/cc construct present in the language, and 
>> moreover 
>> a 'multi-shot' one at that (i.e. the continuation *may* be invoked zero, 
>> once or more times by the effect interpreter). In ATS a simpler way is 
>> to 
>> use template functions to define effects differently (e.g. during 
>> testing 
>> and during the actual execution) -- it's constrained compared to the 
>> call/cc for sure, but then you don't have to pay the price of the 
>> call/cc 
>> plumbing. Another thing about PureScript is that it uses row types to 
>> track 
>> the set of effects that a given Eff computation may involve during its 
>> evaluation.
>>
>
> Not that it will invalidate anything you just said, but the above code 
> was Idris, but they may be similar in this regard (not sure). I need to 
> look into call/cc more at some point - not very familiar with this idea. 
> But I like where you are going with templates in ATS!
>


 Haha, right! I mixed them up. I do remember reading about effects in 
 

Re: Referential transparency in ATS

[Hongwei Xi]

Here is a linear version:

https://pastebin.com/sqXcRhnf

Also, Command is a linear datatype (i.e., dataviewtype).


On Tue, Mar 26, 2019 at 9:02 AM Hongwei Xi  wrote:

> Nice!
>
> But I am very surprised that this code actually works.
> My understanding is that It works because of a bug in patsopt :)
>
> Basically, runCommand should be implemented as a polymorphic function
> (instead of a function
> template). And 'a:t0ype' should be 'a:type'.
>
> fun runCommand: {a:type} Command(a) -> a
>
> Actually, I think that Command should be a linear type, which should you
> more fun!
>
> On Tue, Mar 26, 2019 at 5:49 AM Artyom Shalkhakov <
> artyom.shalkha...@gmail.com> wrote:
>
>> I've made a gist:
>>
>> https://gist.github.com/ashalkhakov/c3577e97b20020fde31f84447fd1e056
>>
>> It actually works. It illustrates the basics (sequencing, bind, input and
>> output). Nice. It doesn't have Haskell's "return" though, but that is
>> pretty simple to add (it's something that "creates" IO where there is no IO
>> at all...).
>>
>> The interpreter is using a continuation in the end. I chose this style
>> because the closure-function (i.e. our continuation) can be passed around
>> freely, whereas with a flat unboxed type it is sometimes difficult for the
>> C compiler to figure out the size of the variable.
>>
>> On Tuesday, March 26, 2019 at 10:11:11 AM UTC+2, Artyom Shalkhakov wrote:
>>
>>> Hi Brandon,
>>>
>>> On Friday, March 22, 2019 at 8:49:29 PM UTC+2, Brandon Barker wrote:

 Hey Artyom,

 Thanks for the very interesting analysis and response.


>>> Glad you found it useful!
>>>
>>> On Fri, Mar 22, 2019 at 4:06 AM Artyom Shalkhakov 
 wrote:

> Hi Brandon,
>
> This is a very lively discussion, thanks for bringing it up.
>
> On Friday, March 22, 2019 at 5:48:07 AM UTC+2, Brandon Barker wrote:
>>
>> And for what it's worth, here is an Idris program for haha using
>> Effects:
>>
>> module Main
>>
>>
>> import Effects
>> import Effect.StdIO
>>
>>
>> hello : Eff () [STDIO]
>> hello = let ha = StdIO.putStr "ha" in ha *> ha
>>
>>
>> main : IO ()
>> main = run hello
>>
>>
>>
>> It prints "ha" twice, despite being a strict language. I presume, but
>> am not sure, this is because the effect time requires it to be 
>> re-evaluated
>> each time.
>>
>>
>>
> Well, the type of "hello" says that the computation will use the STDIO
> effect as many times as is necessary. The way the computation is
> constructed, it is meant to issue commands in a given sequence.
>
> One peculiarity of PureScript is that of handling effects via the
> algebraic effects approach. It's not easy to do in a high-performance way,
> because you need a call/cc construct present in the language, and moreover
> a 'multi-shot' one at that (i.e. the continuation *may* be invoked zero,
> once or more times by the effect interpreter). In ATS a simpler way is to
> use template functions to define effects differently (e.g. during testing
> and during the actual execution) -- it's constrained compared to the
> call/cc for sure, but then you don't have to pay the price of the call/cc
> plumbing. Another thing about PureScript is that it uses row types to 
> track
> the set of effects that a given Eff computation may involve during its
> evaluation.
>

 Not that it will invalidate anything you just said, but the above code
 was Idris, but they may be similar in this regard (not sure). I need to
 look into call/cc more at some point - not very familiar with this idea.
 But I like where you are going with templates in ATS!

>>>
>>>
>>> Haha, right! I mixed them up. I do remember reading about effects in
>>> both languages! And I think they are pretty similar, except in Idris, you
>>> have a type-level list of effects, whereas in PureScript, it is instead a
>>> row of effects. So, pretty similar from the POV of using it. I think. :)
>>>
>>>

> So in short, if we view the programs as creating commands, and then
> some kind of external interpreter that executes them, then it all matches
> up. The programs might be quite pure and non-side-effecting (except for
> non-termination aka infinite looping runtime exceptions), the interpreter
> will perform the effects. Here's a pseudocode for the interpreter:
>
> // the command sub-language
> datatype Command = Print of string | Nop | Seq of (command, command)
> extern
> fun runCommand (c:Command): void
> extern
> fun seq (c:Command, Command): Command
> extern
> fun cprint (s:string): Command
> implement
> seq (c1, c2) = Seq (c1, c2)
> implement
> cprint (s) = Print s
> // the interpreter itself
> implement
> runCommand (c) = case+ c of Nop => (*done!*) | Print s => print (s) |
> Seq (c1, c2) => 

Re: Referential transparency in ATS

[Artyom Shalkhakov]

I've made a gist:

https://gist.github.com/ashalkhakov/c3577e97b20020fde31f84447fd1e056

It actually works. It illustrates the basics (sequencing, bind, input and 
output). Nice. It doesn't have Haskell's "return" though, but that is 
pretty simple to add (it's something that "creates" IO where there is no IO 
at all...).

The interpreter is using a continuation in the end. I chose this style 
because the closure-function (i.e. our continuation) can be passed around 
freely, whereas with a flat unboxed type it is sometimes difficult for the 
C compiler to figure out the size of the variable.

On Tuesday, March 26, 2019 at 10:11:11 AM UTC+2, Artyom Shalkhakov wrote:

> Hi Brandon,
>
> On Friday, March 22, 2019 at 8:49:29 PM UTC+2, Brandon Barker wrote:
>>
>> Hey Artyom,
>>
>> Thanks for the very interesting analysis and response.
>>
>>
> Glad you found it useful!
>
> On Fri, Mar 22, 2019 at 4:06 AM Artyom Shalkhakov  
>> wrote:
>>
>>> Hi Brandon,
>>>
>>> This is a very lively discussion, thanks for bringing it up.
>>>
>>> On Friday, March 22, 2019 at 5:48:07 AM UTC+2, Brandon Barker wrote:

 And for what it's worth, here is an Idris program for haha using 
 Effects:

 module Main


 import Effects
 import Effect.StdIO


 hello : Eff () [STDIO]
 hello = let ha = StdIO.putStr "ha" in ha *> ha


 main : IO ()
 main = run hello



 It prints "ha" twice, despite being a strict language. I presume, but 
 am not sure, this is because the effect time requires it to be 
 re-evaluated 
 each time.



>>> Well, the type of "hello" says that the computation will use the STDIO 
>>> effect as many times as is necessary. The way the computation is 
>>> constructed, it is meant to issue commands in a given sequence.
>>>
>>> One peculiarity of PureScript is that of handling effects via the 
>>> algebraic effects approach. It's not easy to do in a high-performance way, 
>>> because you need a call/cc construct present in the language, and moreover 
>>> a 'multi-shot' one at that (i.e. the continuation *may* be invoked zero, 
>>> once or more times by the effect interpreter). In ATS a simpler way is to 
>>> use template functions to define effects differently (e.g. during testing 
>>> and during the actual execution) -- it's constrained compared to the 
>>> call/cc for sure, but then you don't have to pay the price of the call/cc 
>>> plumbing. Another thing about PureScript is that it uses row types to track 
>>> the set of effects that a given Eff computation may involve during its 
>>> evaluation.
>>>
>>
>> Not that it will invalidate anything you just said, but the above code 
>> was Idris, but they may be similar in this regard (not sure). I need to 
>> look into call/cc more at some point - not very familiar with this idea. 
>> But I like where you are going with templates in ATS!
>>
>
>
> Haha, right! I mixed them up. I do remember reading about effects in both 
> languages! And I think they are pretty similar, except in Idris, you have a 
> type-level list of effects, whereas in PureScript, it is instead a row of 
> effects. So, pretty similar from the POV of using it. I think. :)
>  
>
>>
>>> So in short, if we view the programs as creating commands, and then some 
>>> kind of external interpreter that executes them, then it all matches up. 
>>> The programs might be quite pure and non-side-effecting (except for 
>>> non-termination aka infinite looping runtime exceptions), the interpreter 
>>> will perform the effects. Here's a pseudocode for the interpreter:
>>>
>>> // the command sub-language
>>> datatype Command = Print of string | Nop | Seq of (command, command)
>>> extern
>>> fun runCommand (c:Command): void
>>> extern
>>> fun seq (c:Command, Command): Command
>>> extern
>>> fun cprint (s:string): Command
>>> implement
>>> seq (c1, c2) = Seq (c1, c2)
>>> implement
>>> cprint (s) = Print s
>>> // the interpreter itself
>>> implement
>>> runCommand (c) = case+ c of Nop => (*done!*) | Print s => print (s) | 
>>> Seq (c1, c2) => (runCommand(c1); runCommand(c2))
>>>
>>> Now let's assume the Command is abstract for the rest of the program 
>>> (and only the runCommand, seq and print are exposed). We can now write:
>>>
>>> val hello = let val h = cprint "hi" in seq (h, h) end // here. twice the 
>>> effect!
>>> implement
>>> main0 () = runCommand hello
>>>
>>> The "hello" itself is free of side-effects (or so it seems to me!). We 
>>> might need to lazily evaluate stuff here (e.g. to enable looping, where you 
>>> need to give the interpreter the chance to run side-by-side with your 
>>> expression). Or we need a more poweful "seq" (i.e. the Haskell's "bind" 
>>> operator for stitching together the commands such that the left-hand side 
>>> has to be evaluated to a value that is then fed to the right-hand side -- 
>>> i.e. incrementally built-up as it's being evaluated by the interpeter).
>>>
>>> In Haskell, 

Re: Referential transparency in ATS

[Artyom Shalkhakov]

Hi Brandon,

On Friday, March 22, 2019 at 8:49:29 PM UTC+2, Brandon Barker wrote:
>
> Hey Artyom,
>
> Thanks for the very interesting analysis and response.
>
>
Glad you found it useful!

On Fri, Mar 22, 2019 at 4:06 AM Artyom Shalkhakov  > wrote:
>
>> Hi Brandon,
>>
>> This is a very lively discussion, thanks for bringing it up.
>>
>> On Friday, March 22, 2019 at 5:48:07 AM UTC+2, Brandon Barker wrote:
>>>
>>> And for what it's worth, here is an Idris program for haha using Effects:
>>>
>>> module Main
>>>
>>>
>>> import Effects
>>> import Effect.StdIO
>>>
>>>
>>> hello : Eff () [STDIO]
>>> hello = let ha = StdIO.putStr "ha" in ha *> ha
>>>
>>>
>>> main : IO ()
>>> main = run hello
>>>
>>>
>>>
>>> It prints "ha" twice, despite being a strict language. I presume, but am 
>>> not sure, this is because the effect time requires it to be re-evaluated 
>>> each time.
>>>
>>>
>>>
>> Well, the type of "hello" says that the computation will use the STDIO 
>> effect as many times as is necessary. The way the computation is 
>> constructed, it is meant to issue commands in a given sequence.
>>
>> One peculiarity of PureScript is that of handling effects via the 
>> algebraic effects approach. It's not easy to do in a high-performance way, 
>> because you need a call/cc construct present in the language, and moreover 
>> a 'multi-shot' one at that (i.e. the continuation *may* be invoked zero, 
>> once or more times by the effect interpreter). In ATS a simpler way is to 
>> use template functions to define effects differently (e.g. during testing 
>> and during the actual execution) -- it's constrained compared to the 
>> call/cc for sure, but then you don't have to pay the price of the call/cc 
>> plumbing. Another thing about PureScript is that it uses row types to track 
>> the set of effects that a given Eff computation may involve during its 
>> evaluation.
>>
>
> Not that it will invalidate anything you just said, but the above code was 
> Idris, but they may be similar in this regard (not sure). I need to look 
> into call/cc more at some point - not very familiar with this idea. But I 
> like where you are going with templates in ATS!
>


Haha, right! I mixed them up. I do remember reading about effects in both 
languages! And I think they are pretty similar, except in Idris, you have a 
type-level list of effects, whereas in PureScript, it is instead a row of 
effects. So, pretty similar from the POV of using it. I think. :)
 

>
>> So in short, if we view the programs as creating commands, and then some 
>> kind of external interpreter that executes them, then it all matches up. 
>> The programs might be quite pure and non-side-effecting (except for 
>> non-termination aka infinite looping runtime exceptions), the interpreter 
>> will perform the effects. Here's a pseudocode for the interpreter:
>>
>> // the command sub-language
>> datatype Command = Print of string | Nop | Seq of (command, command)
>> extern
>> fun runCommand (c:Command): void
>> extern
>> fun seq (c:Command, Command): Command
>> extern
>> fun cprint (s:string): Command
>> implement
>> seq (c1, c2) = Seq (c1, c2)
>> implement
>> cprint (s) = Print s
>> // the interpreter itself
>> implement
>> runCommand (c) = case+ c of Nop => (*done!*) | Print s => print (s) | Seq 
>> (c1, c2) => (runCommand(c1); runCommand(c2))
>>
>> Now let's assume the Command is abstract for the rest of the program (and 
>> only the runCommand, seq and print are exposed). We can now write:
>>
>> val hello = let val h = cprint "hi" in seq (h, h) end // here. twice the 
>> effect!
>> implement
>> main0 () = runCommand hello
>>
>> The "hello" itself is free of side-effects (or so it seems to me!). We 
>> might need to lazily evaluate stuff here (e.g. to enable looping, where you 
>> need to give the interpreter the chance to run side-by-side with your 
>> expression). Or we need a more poweful "seq" (i.e. the Haskell's "bind" 
>> operator for stitching together the commands such that the left-hand side 
>> has to be evaluated to a value that is then fed to the right-hand side -- 
>> i.e. incrementally built-up as it's being evaluated by the interpeter).
>>
>> In Haskell, the type Command is termed "IO" (with an additional type 
>> parameter to signify the result type of the command) and the interpreter is 
>> somewhere in the runtime system.
>>
>
> Nice to see that the basis of an interpreter can be created so easily! I 
> guess to make it feasible to program in, in addition to the issues you just 
> mentioned, some primitive standard library functions would need to be 
> wrapped up as 'Command' functions just as you did with cprint; another way 
> to do this might be to ascribe certain effect types to these primitives 
> using e.g praxi. Functions that build on these primitives could then 
> accumulate effects - perhaps some effects could even be consumed, but not 
> sure. Also not sure how the interpreter would deal with some values have 
> more than one effect type: 

Re: Referential transparency in ATS

[Vanessa McHale]

Sounds like I have to fix atspkg :p

If you want to use the monads package with npm + Makefiles, I suppose I
could upload to npm (it might even be a good idea given the permanence
of packages there).

As an aside: I suspect that what makes IO so nice in the context of
Haskell is that you get the same result for the same inputs, every time.
It turns out that many operations involving reads/writes to memory still
satisfy this - and one would like to be able to express that, though I
suspect it would be difficult.

Cheers,
Vanessa McHale

On 3/23/19 2:06 PM, Brandon Barker wrote:
>
>
> On Friday, March 22, 2019 at 2:49:29 PM UTC-4, Brandon Barker wrote:
>
> Hey Artyom,
>
> Thanks for the very interesting analysis and response.
>
> On Fri, Mar 22, 2019 at 4:06 AM Artyom Shalkhakov
> mailto:artyom.shalkha...@gmail.com>>
> wrote:
>
> Hi Brandon,
>
> This is a very lively discussion, thanks for bringing it up.
>
> On Friday, March 22, 2019 at 5:48:07 AM UTC+2, Brandon Barker
> wrote:
>
> And for what it's worth, here is an Idris program for haha
> using Effects:
>
> |
> moduleMain
>
>
> importEffects
> importEffect.StdIO
>
>
> hello :Eff()[STDIO]
> hello =let ha =StdIO.putStr "ha"inha *>ha
>
>
> main :IO ()
> main =run hello
>
> |
>
>
> It prints "ha" twice, despite being a strict language. I
> presume, but am not sure, this is because the effect time
> requires it to be re-evaluated each time.
>
>
>
> Well, the type of "hello" says that the computation will use
> the STDIO effect as many times as is necessary. The way the
> computation is constructed, it is meant to issue commands in a
> given sequence.
>
> One peculiarity of PureScript is that of handling effects via
> the algebraic effects approach. It's not easy to do in a
> high-performance way, because you need a call/cc construct
> present in the language, and moreover a 'multi-shot' one at
> that (i.e. the continuation *may* be invoked zero, once or
> more times by the effect interpreter). In ATS a simpler way is
> to use template functions to define effects differently (e.g.
> during testing and during the actual execution) -- it's
> constrained compared to the call/cc for sure, but then you
> don't have to pay the price of the call/cc plumbing. Another
> thing about PureScript is that it uses row types to track the
> set of effects that a given Eff computation may involve during
> its evaluation.
>
>
> Not that it will invalidate anything you just said, but the above
> code was Idris, but they may be similar in this regard (not sure).
> I need to look into call/cc more at some point - not very familiar
> with this idea. But I like where you are going with templates in ATS!
>
>
> So in short, if we view the programs as creating commands, and
> then some kind of external interpreter that executes them,
> then it all matches up. The programs might be quite pure and
> non-side-effecting (except for non-termination aka infinite
> looping runtime exceptions), the interpreter will perform the
> effects. Here's a pseudocode for the interpreter:
>
> // the command sub-language
> datatype Command = Print of string | Nop | Seq of (command,
> command)
> extern
> fun runCommand (c:Command): void
> extern
> fun seq (c:Command, Command): Command
> extern
> fun cprint (s:string): Command
> implement
> seq (c1, c2) = Seq (c1, c2)
> implement
> cprint (s) = Print s
> // the interpreter itself
> implement
> runCommand (c) = case+ c of Nop => (*done!*) | Print s =>
> print (s) | Seq (c1, c2) => (runCommand(c1); runCommand(c2))
>
> Now let's assume the Command is abstract for the rest of the
> program (and only the runCommand, seq and print are exposed).
> We can now write:
>
> val hello = let val h = cprint "hi" in seq (h, h) end // here.
> twice the effect!
> implement
> main0 () = runCommand hello
>
> The "hello" itself is free of side-effects (or so it seems to
> me!). We might need to lazily evaluate stuff here (e.g. to
> enable looping, where you need to give the interpreter the
> chance to run side-by-side with your expression). Or we need a
> more poweful "seq" (i.e. the Haskell's "bind" operator for
> stitching together the commands such that the left-hand side
> has to be evaluated to a value that is then fed to the
> right-hand side -- i.e. incrementally built-up as it's being
> evaluated by 

Re: Referential transparency in ATS

[Brandon Barker]

On Friday, March 22, 2019 at 2:49:29 PM UTC-4, Brandon Barker wrote:
>
> Hey Artyom,
>
> Thanks for the very interesting analysis and response.
>
> On Fri, Mar 22, 2019 at 4:06 AM Artyom Shalkhakov <
> artyom.shalkha...@gmail.com> wrote:
>
>> Hi Brandon,
>>
>> This is a very lively discussion, thanks for bringing it up.
>>
>> On Friday, March 22, 2019 at 5:48:07 AM UTC+2, Brandon Barker wrote:
>>>
>>> And for what it's worth, here is an Idris program for haha using Effects:
>>>
>>> module Main
>>>
>>>
>>> import Effects
>>> import Effect.StdIO
>>>
>>>
>>> hello : Eff () [STDIO]
>>> hello = let ha = StdIO.putStr "ha" in ha *> ha
>>>
>>>
>>> main : IO ()
>>> main = run hello
>>>
>>>
>>>
>>> It prints "ha" twice, despite being a strict language. I presume, but am 
>>> not sure, this is because the effect time requires it to be re-evaluated 
>>> each time.
>>>
>>>
>>>
>> Well, the type of "hello" says that the computation will use the STDIO 
>> effect as many times as is necessary. The way the computation is 
>> constructed, it is meant to issue commands in a given sequence.
>>
>> One peculiarity of PureScript is that of handling effects via the 
>> algebraic effects approach. It's not easy to do in a high-performance way, 
>> because you need a call/cc construct present in the language, and moreover 
>> a 'multi-shot' one at that (i.e. the continuation *may* be invoked zero, 
>> once or more times by the effect interpreter). In ATS a simpler way is to 
>> use template functions to define effects differently (e.g. during testing 
>> and during the actual execution) -- it's constrained compared to the 
>> call/cc for sure, but then you don't have to pay the price of the call/cc 
>> plumbing. Another thing about PureScript is that it uses row types to track 
>> the set of effects that a given Eff computation may involve during its 
>> evaluation.
>>
>
> Not that it will invalidate anything you just said, but the above code was 
> Idris, but they may be similar in this regard (not sure). I need to look 
> into call/cc more at some point - not very familiar with this idea. But I 
> like where you are going with templates in ATS!
>
>>
>> So in short, if we view the programs as creating commands, and then some 
>> kind of external interpreter that executes them, then it all matches up. 
>> The programs might be quite pure and non-side-effecting (except for 
>> non-termination aka infinite looping runtime exceptions), the interpreter 
>> will perform the effects. Here's a pseudocode for the interpreter:
>>
>> // the command sub-language
>> datatype Command = Print of string | Nop | Seq of (command, command)
>> extern
>> fun runCommand (c:Command): void
>> extern
>> fun seq (c:Command, Command): Command
>> extern
>> fun cprint (s:string): Command
>> implement
>> seq (c1, c2) = Seq (c1, c2)
>> implement
>> cprint (s) = Print s
>> // the interpreter itself
>> implement
>> runCommand (c) = case+ c of Nop => (*done!*) | Print s => print (s) | Seq 
>> (c1, c2) => (runCommand(c1); runCommand(c2))
>>
>> Now let's assume the Command is abstract for the rest of the program (and 
>> only the runCommand, seq and print are exposed). We can now write:
>>
>> val hello = let val h = cprint "hi" in seq (h, h) end // here. twice the 
>> effect!
>> implement
>> main0 () = runCommand hello
>>
>> The "hello" itself is free of side-effects (or so it seems to me!). We 
>> might need to lazily evaluate stuff here (e.g. to enable looping, where you 
>> need to give the interpreter the chance to run side-by-side with your 
>> expression). Or we need a more poweful "seq" (i.e. the Haskell's "bind" 
>> operator for stitching together the commands such that the left-hand side 
>> has to be evaluated to a value that is then fed to the right-hand side -- 
>> i.e. incrementally built-up as it's being evaluated by the interpeter).
>>
>> In Haskell, the type Command is termed "IO" (with an additional type 
>> parameter to signify the result type of the command) and the interpreter is 
>> somewhere in the runtime system.
>>
>
> Nice to see that the basis of an interpreter can be created so easily! I 
> guess to make it feasible to program in, in addition to the issues you just 
> mentioned, some primitive standard library functions would need to be 
> wrapped up as 'Command' functions just as you did with cprint; another way 
> to do this might be to ascribe certain effect types to these primitives 
> using e.g praxi. Functions that build on these primitives could then 
> accumulate effects - perhaps some effects could even be consumed, but not 
> sure. Also not sure how the interpreter would deal with some values have 
> more than one effect type: Haskell seems to use the idea of monad 
> transformers to get around this but I do not find it particularly 
> satisfying so far 
>
> Still need to look into effects and how to encode different effect types - 
> I seem to recall ATS actually had build in support for effects at the type 
> level at some 

Re: Referential transparency in ATS

[Brandon Barker]

On Thu, Mar 21, 2019 at 8:18 PM gmhwxi  wrote:

>
> One can definitely build a monad-based library to support IO:
>
> absvtype IO(a:vt@ype) = ptr
>


If really using monads, would it also be reasonable to do (or ideally start
at Functor and then build up to Monad):

absvtype Monad(a:vt@ype) = ptr

somewhat as discussed at
https://groups.google.com/forum/m/#!msg/ats-lang-users/gLiMU29C77c/sIjtqzmCBAAJ


> The problem with IO monad is that it is so broad. With linear types,
> a programmer can specify a lot more precisely.
>
> I agree. But my limited and slowly changing experience suggests that IO is
a good starting point to help ensure purity in the rest of the code that
doesn't have effects; IO can typically be refined later to different types
of Effects, I suppose.


> >>is that ATS doesn't (by default?) model an IO effect.
>
> No, it doesn't if you use the default library. But nothing prevents you
> from tracking IO effects in ATS.
>

So in this case, one would create an alternative 'main' that must be
composed of IO values. But what is to stop somewhat from calling print in a
function returning an IO, for instance? Thus violating the IO contract.


>
> In the book you mentioned in your message, I was really thinking of
> views for specifying memory layouts. With linear views, a programmer
> can be very precise in describing what memory a function can access/update.
> Compared to state monads, this kind of precision is unmatched.
>

Agreed. Maybe a separate effect type for STDIO, STDIN, etc would be a
better starting point. Even in Haskell, I've seen some authors frown on
State since it is, in their view, a bit dishonest and not much better htan
IO (or maybe not better at all; see "false purity" at
https://www.fpcomplete.com/blog/2017/06/readert-design-pattern).


>
> On Thursday, March 21, 2019 at 1:28:42 PM UTC-4, Brandon Barker wrote:
>>
>>
>>
>> On Thursday, March 21, 2019 at 9:30:40 AM UTC-4, Brandon Barker wrote:
>>>
>>> Hi Artyom,
>>>
>>> I'm also grappling with the issue of RT in this case as I'd so far only
>>> thought about it in terms of function calls, but what you and Vanessa say
>>> helped me to understand the issue. Though I haven't managed to get ATS to
>>> have the same behavior as OCaml in the "let expression" above, I suspect it
>>> is possible. The key phrase here seems to be "side-effecting expression",
>>> and relates to the fact that functions in ATS can perform side effects
>>> without having any effect type or IO monad ascribed to the value (again,
>>> iirc).
>>>
>>
>> Well, maybe that isn't the real key - the real key, I now think, is that
>> ATS doesn't (by default?) model an IO effect. In section 6.9 of
>> http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/PDF/main.pdf it
>> is mentioned that using both linear and dependent types may be used to do
>> this, though I think the suggestion here is for more than printing to e.g.
>> STDOUT.
>>
>> If anyone has looked at modeling/enforcing an IO-like effect type in ATS,
>> I'd be interested to see it.
>>
>>>
>>> Perhaps tonight I should try out the same in Idris or PureScript, which
>>> are not lazily evaluated by default but do use IO, to get a better
>>> understanding.
>>>
>>> On Thursday, March 21, 2019 at 3:17:46 AM UTC-4, Artyom Shalkhakov wrote:

 Hi Brandon,

 Admittedly I don't really understand what RT is, but from what I
 understand, in Haskell the expression like [print "ha"] is basically a
 command to the top-level interpreter (which is the language runtime) to
 perform an effect on the console (moreover, it will be evaluated on
 as-needed basis). Moreover, the ";" is itself another comand, the explicit
 sequencing command, the meaning of which is "perform the left-hand side
 effects, then perform the right-hand side effects". Such a command is a
 value, so it can be passed as a value and reused as many times as is
 necessary. In ATS, the expression like [print "ha"] evaluates right there
 to a void/"no value", and the ";" is also NOT a value at all, but rather a
 "shortcut" syntax to a "let-in-end" form.

 I like to imagine an interpreter that sits in the Haskell's runtime.
 Values of IO type are commands to this interpreter. Typical Haskell
 IO-based programs are building up these commands as they are being
 evaluated by the runtime. The runtime starts evaluation at the "main"
 expression defined by the programmer.

 чт, 21 мар. 2019 г. в 03:45, Brandon Barker :

> I'm a little rusty, so can't come up with many good examples.
>
> Apparently it is possible to do something like this in OCaml:
>
> implement
> main0 () = {
>   val () = let
> val ha = print("ha")
>   in
> (ha; ha) // How to get two ha's here?
>   end
> }
>
>
> After running the program, you would only see one "ha", which violates
> RT.
>
> However, ATS doesn't seem to allow a sequence 

Re: Referential transparency in ATS

[Hongwei Xi]

Monads can be used to track effects in call-by-value languages as well.
I was once told that SPJ wanted to implement a call-by-value Haskell if he
could
have started again :)

In Ur/Web, Adam Chlipala's functional call-by-value language for
web-programming,
monads are used extensively for signals, transactions, etc.




On Thu, Mar 21, 2019 at 9:24 PM Vanessa McHale 
wrote:

> I'm not sure what the point of an IO monad is in a strict language -
> Haskell has good reason to employ them, but I don't think it's really worth
> it in other cases (at least, I actually know much about PureScript, but I
> don't think ATS needs it).
>
> I think the way that ATS uses linear types for IO is slightly different -
> it uses them to e.g. ensure a handle is closed. Linearity does also have
> the curious benefit of making it possible to have lazy/strict evaluation be
> the same; you can rule out the example you provide and you can rule out the
> bottom type.
>
> Cheers,
> Vanessa McHale
> On 3/21/19 12:28 PM, Brandon Barker wrote:
>
>
>
> On Thursday, March 21, 2019 at 9:30:40 AM UTC-4, Brandon Barker wrote:
>>
>> Hi Artyom,
>>
>> I'm also grappling with the issue of RT in this case as I'd so far only
>> thought about it in terms of function calls, but what you and Vanessa say
>> helped me to understand the issue. Though I haven't managed to get ATS to
>> have the same behavior as OCaml in the "let expression" above, I suspect it
>> is possible. The key phrase here seems to be "side-effecting expression",
>> and relates to the fact that functions in ATS can perform side effects
>> without having any effect type or IO monad ascribed to the value (again,
>> iirc).
>>
>
> Well, maybe that isn't the real key - the real key, I now think, is that
> ATS doesn't (by default?) model an IO effect. In section 6.9 of
> http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/PDF/main.pdf it is
> mentioned that using both linear and dependent types may be used to do
> this, though I think the suggestion here is for more than printing to e.g.
> STDOUT.
>
> If anyone has looked at modeling/enforcing an IO-like effect type in ATS,
> I'd be interested to see it.
>
>>
>> Perhaps tonight I should try out the same in Idris or PureScript, which
>> are not lazily evaluated by default but do use IO, to get a better
>> understanding.
>>
>> On Thursday, March 21, 2019 at 3:17:46 AM UTC-4, Artyom Shalkhakov wrote:
>>>
>>> Hi Brandon,
>>>
>>> Admittedly I don't really understand what RT is, but from what I
>>> understand, in Haskell the expression like [print "ha"] is basically a
>>> command to the top-level interpreter (which is the language runtime) to
>>> perform an effect on the console (moreover, it will be evaluated on
>>> as-needed basis). Moreover, the ";" is itself another comand, the explicit
>>> sequencing command, the meaning of which is "perform the left-hand side
>>> effects, then perform the right-hand side effects". Such a command is a
>>> value, so it can be passed as a value and reused as many times as is
>>> necessary. In ATS, the expression like [print "ha"] evaluates right there
>>> to a void/"no value", and the ";" is also NOT a value at all, but rather a
>>> "shortcut" syntax to a "let-in-end" form.
>>>
>>> I like to imagine an interpreter that sits in the Haskell's runtime.
>>> Values of IO type are commands to this interpreter. Typical Haskell
>>> IO-based programs are building up these commands as they are being
>>> evaluated by the runtime. The runtime starts evaluation at the "main"
>>> expression defined by the programmer.
>>>
>>> чт, 21 мар. 2019 г. в 03:45, Brandon Barker :
>>>
 I'm a little rusty, so can't come up with many good examples.

 Apparently it is possible to do something like this in OCaml:

 implement
 main0 () = {
   val () = let
 val ha = print("ha")
   in
 (ha; ha) // How to get two ha's here?
   end
 }


 After running the program, you would only see one "ha", which violates
 RT.

 However, ATS doesn't seem to allow a sequence expression in the "in"
 position of a let expression, as this doesn't compile. Admittedly I'm just
 trying to see if ATS2 doesn't have RT in this particular case, but it would
 also be good to know about the sequence expressions here.
 --
 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-user...@googlegroups.com.
 To post to this group, send email to ats-lan...@googlegroups.com.
 Visit this group at https://groups.google.com/group/ats-lang-users.
 To view this discussion on the web visit
 https://groups.google.com/d/msgid/ats-lang-users/5eba6b86-4146-4ba2-a87f-f8c511d902f0%40googlegroups.com
 

Re: Referential transparency in ATS

[gmhwxi]

One can definitely build a monad-based library to support IO:

absvtype IO(a:vt@ype) = ptr

The problem with IO monad is that it is so broad. With linear types,
a programmer can specify a lot more precisely.

>>is that ATS doesn't (by default?) model an IO effect.

No, it doesn't if you use the default library. But nothing prevents you
from tracking IO effects in ATS.

In the book you mentioned in your message, I was really thinking of
views for specifying memory layouts. With linear views, a programmer
can be very precise in describing what memory a function can access/update.
Compared to state monads, this kind of precision is unmatched.

On Thursday, March 21, 2019 at 1:28:42 PM UTC-4, Brandon Barker wrote:
>
>
>
> On Thursday, March 21, 2019 at 9:30:40 AM UTC-4, Brandon Barker wrote:
>>
>> Hi Artyom,
>>
>> I'm also grappling with the issue of RT in this case as I'd so far only 
>> thought about it in terms of function calls, but what you and Vanessa say 
>> helped me to understand the issue. Though I haven't managed to get ATS to 
>> have the same behavior as OCaml in the "let expression" above, I suspect it 
>> is possible. The key phrase here seems to be "side-effecting expression", 
>> and relates to the fact that functions in ATS can perform side effects 
>> without having any effect type or IO monad ascribed to the value (again, 
>> iirc).
>>
>
> Well, maybe that isn't the real key - the real key, I now think, is that 
> ATS doesn't (by default?) model an IO effect. In section 6.9 of 
> http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/PDF/main.pdf it is 
> mentioned that using both linear and dependent types may be used to do 
> this, though I think the suggestion here is for more than printing to e.g. 
> STDOUT. 
>
> If anyone has looked at modeling/enforcing an IO-like effect type in ATS, 
> I'd be interested to see it.
>
>>
>> Perhaps tonight I should try out the same in Idris or PureScript, which 
>> are not lazily evaluated by default but do use IO, to get a better 
>> understanding.
>>
>> On Thursday, March 21, 2019 at 3:17:46 AM UTC-4, Artyom Shalkhakov wrote:
>>>
>>> Hi Brandon,
>>>
>>> Admittedly I don't really understand what RT is, but from what I 
>>> understand, in Haskell the expression like [print "ha"] is basically a 
>>> command to the top-level interpreter (which is the language runtime) to 
>>> perform an effect on the console (moreover, it will be evaluated on 
>>> as-needed basis). Moreover, the ";" is itself another comand, the explicit 
>>> sequencing command, the meaning of which is "perform the left-hand side 
>>> effects, then perform the right-hand side effects". Such a command is a 
>>> value, so it can be passed as a value and reused as many times as is 
>>> necessary. In ATS, the expression like [print "ha"] evaluates right there 
>>> to a void/"no value", and the ";" is also NOT a value at all, but rather a 
>>> "shortcut" syntax to a "let-in-end" form.
>>>
>>> I like to imagine an interpreter that sits in the Haskell's runtime. 
>>> Values of IO type are commands to this interpreter. Typical Haskell 
>>> IO-based programs are building up these commands as they are being 
>>> evaluated by the runtime. The runtime starts evaluation at the "main" 
>>> expression defined by the programmer.
>>>
>>> чт, 21 мар. 2019 г. в 03:45, Brandon Barker :
>>>
 I'm a little rusty, so can't come up with many good examples.

 Apparently it is possible to do something like this in OCaml:

 implement
 main0 () = {
   val () = let
 val ha = print("ha")
   in
 (ha; ha) // How to get two ha's here?
   end
 }


 After running the program, you would only see one "ha", which violates 
 RT.

 However, ATS doesn't seem to allow a sequence expression in the "in" 
 position of a let expression, as this doesn't compile. Admittedly I'm just 
 trying to see if ATS2 doesn't have RT in this particular case, but it 
 would 
 also be good to know about the sequence expressions here.

 -- 
 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-user...@googlegroups.com.
 To post to this group, send email to ats-lan...@googlegroups.com.
 Visit this group at https://groups.google.com/group/ats-lang-users.
 To view this discussion on the web visit 
 https://groups.google.com/d/msgid/ats-lang-users/5eba6b86-4146-4ba2-a87f-f8c511d902f0%40googlegroups.com
  
 
 .

>>>
>>>
>>> -- 
>>> Cheers,
>>> Artyom Shalkhakov
>>>
>>

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

Re: Referential transparency in ATS

[gmhwxi]

I see. Then you have to blame C :)

My observation is that engineers have a tendency to not
treat things uniformly. For instance, in C, you cannot declare
a variable (or a field in a struct) to be of the type 'void'. In other
words, 'void' is treated specially as a type. This special treatment
of 'void' is "categorically" improper. Pun intended:

It is my humble opinion that engineers should all learn a little bit
of category theory.

By the way, here is a quick "fix":

implement
main0 () = {
  val () = let
val ha = print("ha")
  in
ignoret(ha; ha)
  end
}


On Thursday, March 21, 2019 at 9:15:48 AM UTC-4, Brandon Barker wrote:
>
>
>
> On Thursday, March 21, 2019 at 8:39:10 AM UTC-4, gmhwxi wrote:
>>
>>
>> >>ATS doesn't seem to allow a sequence expression in the "in" position of 
>> a let expression,
>>
>> It does. You can write:
>>
>> implement
>> main0 () =
>> let
>>   val ha = print("ha")
>> in
>>   ha; ha
>> end
>>
>>
> I think I tried that - but I tried it again verbatim, and I get:
>
> $ patscc -o haha haha.dats 
> In file included from haha_dats.c:15:0:
> haha_dats.c: In function 'mainats_void_0':
> haha_dats.c:179:26: error: 'tmp1' undeclared (first use in this function)
>  ATSINSmove_void(tmpret0, tmp1) ;
>   ^
> /nix/store/q8ll64apv4nn6x4dxprkjx29n3kwsraw-ats2-0.3.11/lib/ats2-postiats-
> 0.3.11/ccomp/runtime/pats_ccomp_instrset.h:284:39: note: in definition of 
> macro 'ATSINSmove_void'
>  #define ATSINSmove_void(tmp, command) command
>^~~
> haha_dats.c:179:26: note: each undeclared identifier is reported only 
> once for each function it appears in
>  ATSINSmove_void(tmpret0, tmp1) ;
>   ^
> /nix/store/q8ll64apv4nn6x4dxprkjx29n3kwsraw-ats2-0.3.11/lib/ats2-postiats-
> 0.3.11/ccomp/runtime/pats_ccomp_instrset.h:284:39: note: in definition of 
> macro 'ATSINSmove_void'
>  #define ATSINSmove_void(tmp, command) command
>^~~
>
>
>
>
>  
>
>> To get two ha's, you can write:
>>
>> implement
>> main0 () =
>> let
>>   val ha = $delay(print("ha"))
>> in
>>   !ha; !ha
>> end
>>
>> If you want 1000 ha's, you can do:
>>
>> #include "share/atspre_staload.hats"
>> #include "share/atspre_staload_libats_ML.hats"
>>
>> implement
>> main0 () =
>> let
>>   val ha = $delay(print("ha"))
>> in
>>   1000 * ha
>> end
>>
>>
>> On Wed, Mar 20, 2019 at 9:45 PM Brandon Barker  
>> wrote:
>>
>>> I'm a little rusty, so can't come up with many good examples.
>>>
>>> Apparently it is possible to do something like this in OCaml:
>>>
>>> implement
>>> main0 () = {
>>>   val () = let
>>> val ha = print("ha")
>>>   in
>>> (ha; ha) // How to get two ha's here?
>>>   end
>>> }
>>>
>>>
>>> After running the program, you would only see one "ha", which violates 
>>> RT.
>>>
>>> However, ATS doesn't seem to allow a sequence expression in the "in" 
>>> position of a let expression, as this doesn't compile. Admittedly I'm just 
>>> trying to see if ATS2 doesn't have RT in this particular case, but it would 
>>> also be good to know about the sequence expressions here.
>>>
>>> -- 
>>> 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-user...@googlegroups.com.
>>> To post to this group, send email to ats-lan...@googlegroups.com.
>>> Visit this group at https://groups.google.com/group/ats-lang-users.
>>> To view this discussion on the web visit 
>>> https://groups.google.com/d/msgid/ats-lang-users/5eba6b86-4146-4ba2-a87f-f8c511d902f0%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 post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/e483f183-00ba-4ebb-a8cf-94857a88d4b0%40googlegroups.com.

Re: Referential transparency in ATS

[Brandon Barker]

Hi Artyom,

I'm also grappling with the issue of RT in this case as I'd so far only 
thought about it in terms of function calls, but what you and Vanessa say 
helped me to understand the issue. Though I haven't managed to get ATS to 
have the same behavior as OCaml in the "let expression" above, I suspect it 
is possible. The key phrase here seems to be "side-effecting expression", 
and relates to the fact that functions in ATS can perform side effects 
without having any effect type or IO monad ascribed to the value (again, 
iirc).

Perhaps tonight I should try out the same in Idris or PureScript, which are 
not lazily evaluated by default but do use IO, to get a better 
understanding.

On Thursday, March 21, 2019 at 3:17:46 AM UTC-4, Artyom Shalkhakov wrote:
>
> Hi Brandon,
>
> Admittedly I don't really understand what RT is, but from what I 
> understand, in Haskell the expression like [print "ha"] is basically a 
> command to the top-level interpreter (which is the language runtime) to 
> perform an effect on the console (moreover, it will be evaluated on 
> as-needed basis). Moreover, the ";" is itself another comand, the explicit 
> sequencing command, the meaning of which is "perform the left-hand side 
> effects, then perform the right-hand side effects". Such a command is a 
> value, so it can be passed as a value and reused as many times as is 
> necessary. In ATS, the expression like [print "ha"] evaluates right there 
> to a void/"no value", and the ";" is also NOT a value at all, but rather a 
> "shortcut" syntax to a "let-in-end" form.
>
> I like to imagine an interpreter that sits in the Haskell's runtime. 
> Values of IO type are commands to this interpreter. Typical Haskell 
> IO-based programs are building up these commands as they are being 
> evaluated by the runtime. The runtime starts evaluation at the "main" 
> expression defined by the programmer.
>
> чт, 21 мар. 2019 г. в 03:45, Brandon Barker  >:
>
>> I'm a little rusty, so can't come up with many good examples.
>>
>> Apparently it is possible to do something like this in OCaml:
>>
>> implement
>> main0 () = {
>>   val () = let
>> val ha = print("ha")
>>   in
>> (ha; ha) // How to get two ha's here?
>>   end
>> }
>>
>>
>> After running the program, you would only see one "ha", which violates RT.
>>
>> However, ATS doesn't seem to allow a sequence expression in the "in" 
>> position of a let expression, as this doesn't compile. Admittedly I'm just 
>> trying to see if ATS2 doesn't have RT in this particular case, but it would 
>> also be good to know about the sequence expressions here.
>>
>> -- 
>> 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-user...@googlegroups.com .
>> To post to this group, send email to ats-lan...@googlegroups.com 
>> .
>> Visit this group at https://groups.google.com/group/ats-lang-users.
>> To view this discussion on the web visit 
>> https://groups.google.com/d/msgid/ats-lang-users/5eba6b86-4146-4ba2-a87f-f8c511d902f0%40googlegroups.com
>>  
>> 
>> .
>>
>
>
> -- 
> Cheers,
> Artyom Shalkhakov
>

-- 
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 post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/b1765d06-7659-4a60-846f-25535e87a0b9%40googlegroups.com.

Re: Referential transparency in ATS

[Brandon Barker]

On Wednesday, March 20, 2019 at 10:40:34 PM UTC-4, Vanessa McHale wrote:
>
> I think that might have do with laziness? If you have a side-effecting 
> expression and you try to pretend it's call-by-need, then bad things happen 
> (beta reduction is no longer valid!)
>
> Yes, that seems to be the case with OCaml as far as I can tell.
 

> Do you have an example in OCaml? I admit I am curious as to why their 
> compiler would do such a thing.
>

The example I saw, which I hadn't tested as I've never used OCaml, was:

let val ha = (print "ha") in ha; ha end 

 

> On 3/20/19 8:45 PM, Brandon Barker wrote:
>
> I'm a little rusty, so can't come up with many good examples. 
>
> Apparently it is possible to do something like this in OCaml:
>
> implement
> main0 () = {
>   val () = let
> val ha = print("ha")
>   in
> (ha; ha) // How to get two ha's here?
>   end
> }
>
>
> After running the program, you would only see one "ha", which violates RT.
>
> However, ATS doesn't seem to allow a sequence expression in the "in" 
> position of a let expression, as this doesn't compile. Admittedly I'm just 
> trying to see if ATS2 doesn't have RT in this particular case, but it would 
> also be good to know about the sequence expressions here.
> -- 
> 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-user...@googlegroups.com .
> To post to this group, send email to ats-lan...@googlegroups.com 
> .
> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit 
> https://groups.google.com/d/msgid/ats-lang-users/5eba6b86-4146-4ba2-a87f-f8c511d902f0%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 post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/2445b542-f850-4761-92f1-9375f1f610eb%40googlegroups.com.

Re: Referential transparency in ATS

[Vanessa McHale]

I think that might have do with laziness? If you have a side-effecting
expression and you try to pretend it's call-by-need, then bad things
happen (beta reduction is no longer valid!)

Do you have an example in OCaml? I admit I am curious as to why their
compiler would do such a thing.

On 3/20/19 8:45 PM, Brandon Barker wrote:
> I'm a little rusty, so can't come up with many good examples.
>
> Apparently it is possible to do something like this in OCaml:
>
> |
> implement
> main0 ()={
>   val ()=let
>     val ha =print("ha")
>   in
>     (ha;ha)// How to get two ha's here?
>   end
> }
> |
>
>
> After running the program, you would only see one "ha", which violates RT.
>
> However, ATS doesn't seem to allow a sequence expression in the "in"
> position of a let expression, as this doesn't compile. Admittedly I'm
> just trying to see if ATS2 doesn't have RT in this particular case,
> but it would also be good to know about the sequence expressions here.
> -- 
> 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 post to this group, send email to ats-lang-users@googlegroups.com
> .
> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/5eba6b86-4146-4ba2-a87f-f8c511d902f0%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 post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/b5eac771-323c-da14-e639-b7e1822a4185%40iohk.io.


signature.asc
Description: OpenPGP digital signature