Hi Hongwei, On Tuesday, March 26, 2019 at 3:22:41 PM UTC+2, gmhwxi wrote: > > Here is a linear version: > > https://pastebin.com/sqXcRhnf > > Also, Command is a linear datatype (i.e., dataviewtype). > > Great! Now, what about boxing, can we do something with boxing? I expect such code, if it's really used in practice, to involve LOTS of these little objects. So it will probably behave badly if every call to a continuation involves a heap allocation... Let us be a bit more resource-conscious, please. :)
I did a similar example a while back where I used some CPS style to get rid of boxing: https://github.com/ashalkhakov/tfc/blob/master/src/SATS/cont.sats Basically we can 'co-opt' the ATS compiler to do all the plumbing. The closure call and its packing is non-uniform but the closure itself is uniform in size, since it's a pointer to the heap: https://github.com/ashalkhakov/tfc/blob/master/test/threads.dats To call a continuation, the return type must be statically known (at both the callee side and the caller side). So maybe we can do something similar here? > > > On Tue, Mar 26, 2019 at 9:02 AM Hongwei Xi <gmh...@gmail.com <javascript:>> > wrote: > >> Nice! >> >> But I am very surprised that this code actually works. >> My understanding is that It works because of a bug in patsopt :) >> >> Basically, runCommand should be implemented as a polymorphic function >> (instead of a function >> template). And 'a:t0ype' should be 'a:type'. >> >> fun runCommand: {a:type} Command(a) -> a >> >> Actually, I think that Command should be a linear type, which should you >> more fun! >> >> On Tue, Mar 26, 2019 at 5:49 AM Artyom Shalkhakov <artyom.s...@gmail.com >> <javascript:>> wrote: >> >>> I've made a gist: >>> >>> https://gist.github.com/ashalkhakov/c3577e97b20020fde31f84447fd1e056 >>> >>> It actually works. It illustrates the basics (sequencing, bind, input >>> and output). Nice. It doesn't have Haskell's "return" though, but that is >>> pretty simple to add (it's something that "creates" IO where there is no IO >>> at all...). >>> >>> The interpreter is using a continuation in the end. I chose this style >>> because the closure-function (i.e. our continuation) can be passed around >>> freely, whereas with a flat unboxed type it is sometimes difficult for the >>> C compiler to figure out the size of the variable. >>> >>> On Tuesday, March 26, 2019 at 10:11:11 AM UTC+2, Artyom Shalkhakov wrote: >>> >>>> Hi Brandon, >>>> >>>> On Friday, March 22, 2019 at 8:49:29 PM UTC+2, Brandon Barker wrote: >>>>> >>>>> Hey Artyom, >>>>> >>>>> Thanks for the very interesting analysis and response. >>>>> >>>>> >>>> Glad you found it useful! >>>> >>>> On Fri, Mar 22, 2019 at 4:06 AM Artyom Shalkhakov < >>>>> artyom.s...@gmail.com> wrote: >>>>> >>>>>> Hi Brandon, >>>>>> >>>>>> This is a very lively discussion, thanks for bringing it up. >>>>>> >>>>>> On Friday, March 22, 2019 at 5:48:07 AM UTC+2, Brandon Barker wrote: >>>>>>> >>>>>>> And for what it's worth, here is an Idris program for haha using >>>>>>> Effects: >>>>>>> >>>>>>> module Main >>>>>>> >>>>>>> >>>>>>> import Effects >>>>>>> import Effect.StdIO >>>>>>> >>>>>>> >>>>>>> hello : Eff () [STDIO] >>>>>>> hello = let ha = StdIO.putStr "ha" in ha *> ha >>>>>>> >>>>>>> >>>>>>> main : IO () >>>>>>> main = run hello >>>>>>> >>>>>>> >>>>>>> >>>>>>> It prints "ha" twice, despite being a strict language. I presume, >>>>>>> but am not sure, this is because the effect time requires it to be >>>>>>> re-evaluated each time. >>>>>>> >>>>>>> >>>>>>> >>>>>> Well, the type of "hello" says that the computation will use the >>>>>> STDIO effect as many times as is necessary. The way the computation is >>>>>> constructed, it is meant to issue commands in a given sequence. >>>>>> >>>>>> One peculiarity of PureScript is that of handling effects via the >>>>>> algebraic effects approach. It's not easy to do in a high-performance >>>>>> way, >>>>>> because you need a call/cc construct present in the language, and >>>>>> moreover >>>>>> a 'multi-shot' one at that (i.e. the continuation *may* be invoked zero, >>>>>> once or more times by the effect interpreter). In ATS a simpler way is >>>>>> to >>>>>> use template functions to define effects differently (e.g. during >>>>>> testing >>>>>> and during the actual execution) -- it's constrained compared to the >>>>>> call/cc for sure, but then you don't have to pay the price of the >>>>>> call/cc >>>>>> plumbing. Another thing about PureScript is that it uses row types to >>>>>> track >>>>>> the set of effects that a given Eff computation may involve during its >>>>>> evaluation. >>>>>> >>>>> >>>>> Not that it will invalidate anything you just said, but the above code >>>>> was Idris, but they may be similar in this regard (not sure). I need to >>>>> look into call/cc more at some point - not very familiar with this idea. >>>>> But I like where you are going with templates in ATS! >>>>> >>>> >>>> >>>> Haha, right! I mixed them up. I do remember reading about effects in >>>> 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-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/73270adc-4327-470b-b900-ae20e3b36cea%40googlegroups.com >>> >>> <https://groups.google.com/d/msgid/ats-lang-users/73270adc-4327-470b-b900-ae20e3b36cea%40googlegroups.com?utm_medium=email&utm_source=footer> >>> . >>> >> -- 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/fd79538d-97ac-4f54-b62d-ceeb08794036%40googlegroups.com.
