Referential transparency in ATS

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

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

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

[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

[Artyom Shalkhakov]

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 <brandon...@gmail.com>:

--

You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-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

[Hongwei Xi]

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

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

--

[Hongwei Xi]

>>then bad things happen (beta reduction is no longer valid!)

ML is call-by-value. It only supports beta-v (that is call-by-value beta).

There are a lot of problems with supporting beta. For instance, it is in general

very difficult to tell the memory usage of Haskell programs.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/b5eac771-323c-da14-e639-b7e1822a4185%40iohk.io.

[Brandon Barker]

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

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

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

[Julian Fondren]

On Wednesday, March 20, 2019 at 8:45:24 PM UTC-5, 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
}

Something like the ATS is certainly possible:

let ha = (print_string "ha") in ha; ha

And you get similar results in OCaml: 'ha' is bound to unit, and only one 'ha' is printed.

[Brandon Barker]

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.

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

[Vanessa McHale]

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

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/5391973a-4bd4-4238-a007-4dc08d1d9d4d%40googlegroups.com.

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

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/b21006ff-bc7e-d828-1462-4d9c7103feae%40iohk.io.

[Brandon Barker]

On Thu, Mar 21, 2019 at 8:18 PM gmhwxi <gmh...@gmail.com> 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).

 

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/3d13aac1-2f28-47af-afbd-6d9eced901db%40googlegroups.com.

--

Brandon Barker
brandon...@gmail.com

[Brandon Barker]

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.

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@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/3d13aac1-2f28-47af-afbd-6d9eced901db%40googlegroups.com.

--

Brandon Barker
brandon...@gmail.com

[Brandon Barker]

Effect type, not effect time! But it is time for bed.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/3d13aac1-2f28-47af-afbd-6d9eced901db%40googlegroups.com.

--

Brandon Barker
brandon...@gmail.com

--

You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-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/85a9cc71-d4e1-4168-94fa-ba64ae53561d%40googlegroups.com.

--

Brandon Barker
brandon...@gmail.com

[Artyom Shalkhakov]

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.

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.

 

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/3d13aac1-2f28-47af-afbd-6d9eced901db%40googlegroups.com.

--

Brandon Barker
brandon...@gmail.com

[Brandon Barker]

Hey Artyom,

Thanks for the very interesting analysis and response.

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!

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

Do you have or plan on having a repo to play around with this idea? If not I may try to start one (at some point).

 

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/9ff2fb00-6790-4541-9bc0-0a949a0c46e3%40googlegroups.com.

--

Brandon Barker
brandon...@gmail.com

[Brandon Barker]

OK, here is what I remembered seeing, but I don't know how useful this in the current discussion:

Function effects tags (not real keywords):
    ntm
    exn
    ref
    wrt
    all

Special functions/values (not keywords and invalid as identifiers):
    $effmask

Do you have or plan on having a repo to play around with this idea? If not I may try to start one (at some point).

I'm starting one, but got a bit sidetracked with trying to get atspkg working in my environment, as I wanted to use Vanessa's monads package as a basis for playing around with this. 

In summary, in ATS we don't really need the sequencing of monads since it is an eager language by default (but still benefit from purity isolation), but if we are modeling it in the above way, I suspect we might as well do so to benefit from the functions and laws that monads bring us. The big questions I have now are, can we get this sequencing to be zero-overhead in ATS, and can we get syntactic sugar for it (possibly in ATS3)?  For the first, we should know something after a bit of experimentation, but having Haskell-like do notation would be helpful for this as well the syntactic sugar benefit. 

The other question I still have relates to Hongwei's point: just having IO is rather limited in managing types of effects. I would need to look into this more. Unlike the example I posted above, Idris is apparently now using http://docs.idris-lang.org/en/latest/st/state.html to defined effects. But again, ATS is probably more powerful in this regard with its linear types: the core issue I was trying to tackle is just working in an ATS environment that doesn't allow mixing effectful and pure code without types to help guard against this. And it seems Artyom has presented the basis of a solution, which could likely be made a reality by tackling the above issues, including creating an ATS wrapper library that describes functions in terms of their Effects, if they are effectful. Maybe we just start with a simple type, IO, as a prototype, but generalize to Effect <static list of effects> later on - if anyone who has more experience with effects reads this, would appreciate your thoughts. I do think that for most people, if they don't want to think too much about Effects, having a map from most or all Effect types into IO would make this a bit easier to work with. Most of the time, people will probably be happy to work in IO, and going beyond that for some purposes is probably overkill. I suspect some people reading this may already think this proposal is overkill, if not downright problematic - but again, would appreciate feedback.

 

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@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/9ff2fb00-6790-4541-9bc0-0a949a0c46e3%40googlegroups.com.

--

Brandon Barker
brandon...@gmail.com

[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

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/2a3ab922-0844-484e-8131-24f76f61cf96%40googlegroups.com.

[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 <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 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: Haskell seems to use the idea of monad transformers to get around this but I do not find it particularly satisfying so far

In Haskell there exists special support for the IO monad in the runtime and in the compiler; without such support I don't think it will be feasible to program in this way (since we will have to pay the price for the construction of terms even in the simplest of cases!).

 

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

Well, in my post I was talking mostly about algebraic effect handlers, and in ATS we have effect types. The former I'm interested in mostly because of modular testing. The latter, I think, is used mostly for tracking the dynamic terms that can be safely erased from the program with no change to said program's behavior.

 

Do you have or plan on having a repo to play around with this idea? If not I may try to start one (at some point).

Well, I'll post it as a gist on github. I think there does exist a connection between the algebraic effect handlers and function templates that I would like to pursue, but I'm short on time.

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

[Hongwei Xi]

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!

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/73270adc-4327-470b-b900-ae20e3b36cea%40googlegroups.com.

[Hongwei Xi]

Here is a linear version:

https://pastebin.com/sqXcRhnf

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

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

[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. :)

[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'?

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/fd79538d-97ac-4f54-b62d-ceeb08794036%40googlegroups.com.

[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...).

[Hongwei Xi]

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

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

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 >> a?) -<cloptr1> Command(b))

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

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/2367999b-fb1e-420e-b966-42c6f4aced66%40googlegroups.com.

[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? >> 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 >> a?) -<cloptr1> 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. :)

[Hongwei Xi]

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

Typo: vtype should be vt@ype.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/9ee1b434-b31e-4bca-9a24-c2a240a46172%40googlegroups.com.

[Hongwei Xi]

Boxing is removed:

https://pastebin.com/JacNgK2t

Some hacks are used to make it work...

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

[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`"


 

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

[Brandon Barker]

Thanks, Dambaev, for the excellent explanation.

[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 

    return v = IteratorM (return v)

instance Applicative IteratorM where

    pure v = IteratorM (pure v)

    -- :: f (a -> b) -> f a -> f b

    (<*>) (IteratorM first) (IteratorM second) = 

        IteratorM ( first <*> second)

instance Functor IteratorM where

    -- :: (a -> b) -> f a -> f b

    fmap f (IteratorM first) = IteratorM (fmap f first)

foreign import ccall "gtk_tree_selection_get_selected" :: Ptr () -> IO (Ptr ())
gtk_tree_selection_with_selected :: GtkTreeView-> (Iterator-> IteratorM a)-> IO a
gtk_tree_selection_with_selected (GtkTreeView tree) nested = c_gtk_tree_selection_get_selected tree >> \ptr-> nested (Iterator ptr)

gtk_tree_view_iter_set_color :: Iterator-> Color-> IteratorM ()
gtk_tree_view_iter_set_color (Iterator iter) color = IteratorM (c_gtk_tree_view_iter_set_color iter color)

foreign import ccall "gtk_tree_model_get_path" :: Ptr ()-> Ptr ()-> IO (Ptr ())
gtk_tree_model_get_path :: GtkTreeView-> Iterator-> IteratorM GtkTreePath -- let's pretend, that it uses GtkTreeView for simplicity
gtk_tree_model_get_path (GtkTreeView tree) (Iterator iter) = IteratorM (c_gtk_tree_model_get_path tree iter)

Main.hs

module Main where
import Iterator
import GtkTreeView

foreign import ccall "g_signal_emit" g_signal_emit:: Ptr CChar -> IO ()
foreign import ccall "g_signal_connect" g_signal_connect :: Ptr CChar-> (Ptr ()-> IO ())-> Ptr () -> IO ()


handler :: GtkTreeView-> IO ()
handler tree = gtk_tree_view_delete_by_index tree 0 -- deleting first row

main :: IO ()
main = do
  tree <- gtk_tree_view_new_with_model
  g_signal_connect "CHDIR" handler tree
  -- insert 1 row into tree here ...
  gtk_tree_selection_with_selected tree $ \iter-> do
    let a = 1 + 2 -- valid, can use pure expressions inside IteratorM
    path <- gtk_tree_model_get_path iter -- valid
    gtk_tree_view_set_color iter Blue -- valid
    {- g_signal_emit "CHDIR" -- compile time error here, as it not IteratorM -}
  g_signal_emit "CHDIR" -- valid here, as we are not anymore inside gtk_tree_slection_with_selected nested: iter is out of scope now

One possible issue here is that Iterator value can escape from `gtk_tree_selection_with_selected` function, but this can be fixed with return type of `IO ()`.

So this example motivates me to search for ability to have similar modeling of side effects in ATS2 by using something like `datatype IO (a:t@ype) = IO of (RealWorld-> (RealWorld, a)`.

Or am I missing something and this issue can be solved in ATS2 as well, without rewriting standard library and patching compiler?

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

--
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 view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/3a2e5526-0dc7-41f0-b992-340b0e6a5564%40googlegroups.com.

[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`?

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

--
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 view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/4a5064b4-357e-4055-b1af-44373e076592%40googlegroups.com.

[Dambaev Alexander]

Thanks for directions to investigate!

[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

[Dambaev Alexander]

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

[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 <gmh...@gmail.com> 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 <brandon...@gmail.com>:

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-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/3d13aac1-2f28-47af-afbd-6d9eced901db%40googlegroups.com.

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

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lan...@googlegroups.com.

[Brandon Barker]

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

[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