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. 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-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/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.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. 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/85a9cc71-d4e1-4168-94fa-ba64ae53561d%40googlegroups.com.
