Here is a linear version:
https://pastebin.com/sqXcRhnf
Also, Command is a linear datatype (i.e., dataviewtype).
On Tue, Mar 26, 2019 at 9:02 AM Hongwei Xi <gmh...@gmail.com> 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.shalkha...@gmail.com> 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-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
>> <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/CAPPSPLrWrYGDfx%3D5EGD9mU5ZHV%2BFXhuxFXqsJy2P8kSYr9L7gg%40mail.gmail.com.
