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 > <javascript:>> 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 <javascript:>. >> To post to this group, send email to ats-lan...@googlegroups.com >> <javascript:>. >> 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 <javascript:> > -- 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/2433f94b-12ba-4829-9ff9-f958206721b0%40googlegroups.com.
