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 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. > > >> >> >>> >>> >>>> On Thursday, March 21, 2019 at 11:33:35 PM UTC-4, Brandon Barker wrote: >>>>> >>>>> >>>>> >>>>> 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). >>>>> >>>>> >>>>>> >>>>>> 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 >>>>>>>>>> >>>>>>>>>> <https://groups.google.com/d/msgid/ats-lang-users/5eba6b86-4146-4ba2-a87f-f8c511d902f0%40googlegroups.com?utm_medium=email&utm_source=footer> >>>>>>>>>> . >>>>>>>>>> >>>>>>>>> >>>>>>>>> >>>>>>>>> -- >>>>>>>>> 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 >>>>>> >>>>>> <https://groups.google.com/d/msgid/ats-lang-users/3d13aac1-2f28-47af-afbd-6d9eced901db%40googlegroups.com?utm_medium=email&utm_source=footer> >>>>>> . >>>>>> >>>>> >>>>> >>>>> -- >>>>> 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/9ff2fb00-6790-4541-9bc0-0a949a0c46e3%40googlegroups.com >>> >>> <https://groups.google.com/d/msgid/ats-lang-users/9ff2fb00-6790-4541-9bc0-0a949a0c46e3%40googlegroups.com?utm_medium=email&utm_source=footer> >>> . >>> >> >> >> -- >> 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-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/73270adc-4327-470b-b900-ae20e3b36cea%40googlegroups.com.
