Sounds like I have to fix atspkg :p If you want to use the monads package with npm + Makefiles, I suppose I could upload to npm (it might even be a good idea given the permanence of packages there).
As an aside: I suspect that what makes IO so nice in the context of Haskell is that you get the same result for the same inputs, every time. It turns out that many operations involving reads/writes to memory still satisfy this - and one would like to be able to express that, though I suspect it would be difficult. Cheers, Vanessa McHale On 3/23/19 2:06 PM, Brandon Barker wrote: > > > On Friday, March 22, 2019 at 2:49:29 PM UTC-4, Brandon Barker wrote: > > Hey Artyom, > > Thanks for the very interesting analysis and response. > > On Fri, Mar 22, 2019 at 4:06 AM Artyom Shalkhakov > <artyom.shalkha...@gmail.com <mailto:artyom.shalkha...@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: > > | > moduleMain > > > importEffects > importEffect.StdIO > > > hello :Eff()[STDIO] > hello =let ha =StdIO.putStr "ha"inha *>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! > > > 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 > > 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. > > > OK, here is what Iremembered seeing > <https://groups.google.com/d/msg/ats-lang-users/qsv05ivj5UY/LLqzjat-CgAJ>, > but I don't know how useful this in the current discussion: > > | > Functioneffects tags (notreal keywords): > ntm > exn > ref > wrt > all > > Specialfunctions/values (notkeywords andinvalid asidentifiers): > $effmask > | > > 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). > > > I'm starting one, but got a bit sidetracked with trying to get atspkg > working in my environment, as I wanted to use Vanessa's monads package > <https://github.com/vmchale/monads> as a basis for playing around with > this. > > In summary, in ATS we don't really need the sequencing of monads since > it is an eager language by default (but still benefit from purity > isolation), but if we are modeling it in the above way, I suspect we > might as well do so to benefit from the functions and laws that monads > bring us. The big questions I have now are, can we get this sequencing > to be zero-overhead in ATS, and can we get syntactic sugar for it > (possibly in ATS3)? For the first, we should know something after a > bit of experimentation, but having Haskell-like do notation would be > helpful for this as well the syntactic sugar benefit. > > The other question I still have relates to Hongwei's point: just > having IO is rather limited in managing types of effects. I would need > to look into this more. Unlike the example I posted above, Idris is > apparently now > using http://docs.idris-lang.org/en/latest/st/state.html to defined > effects. But again, ATS is probably more powerful in this regard with > its linear types: the core issue I was trying to tackle is just > working in an ATS environment that doesn't allow mixing effectful and > pure code without types to help guard against this. And it seems > Artyom has presented the basis of a solution, which could likely be > made a reality by tackling the above issues, including creating an ATS > wrapper library that describes functions in terms of their Effects, if > they are effectful. Maybe we just start with a simple type, IO, as a > prototype, but generalize to Effect <static list of effects> later on > - if anyone who has more experience with effects reads this, would > appreciate your thoughts. I do think that for most people, if they > don't want to think too much about Effects, having a map from most or > all Effect types into IO would make this a bit easier to work with. > Most of the time, people will probably be happy to work in IO, and > going beyond that for some purposes is probably overkill. I suspect > some people reading this may already think this proposal is overkill, > if not downright problematic - but again, would appreciate feedback. > > > > > > 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 > > <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 > > <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 > > <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 > > <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 > <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-users+unsubscr...@googlegroups.com > <mailto:ats-lang-users+unsubscr...@googlegroups.com>. > To post to this group, send email to > ats-lang-users@googlegroups.com > <mailto:ats-lang-users@googlegroups.com>. > Visit this group at > https://groups.google.com/group/ats-lang-users > <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.bar...@gmail.com <mailto:brandon.bar...@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 > <mailto:ats-lang-users+unsubscr...@googlegroups.com>. > To post to this group, send email to ats-lang-users@googlegroups.com > <mailto: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/2a3ab922-0844-484e-8131-24f76f61cf96%40googlegroups.com > <https://groups.google.com/d/msgid/ats-lang-users/2a3ab922-0844-484e-8131-24f76f61cf96%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/efd54407-af84-3035-a3a5-19ab9fea54dd%40iohk.io.
signature.asc
Description: OpenPGP digital signature
