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. > 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 <javascript:>> >> 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 <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/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 <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/9ff2fb00-6790-4541-9bc0-0a949a0c46e3%40googlegroups.com.
