I'm not sure what the point of an IO monad is in a strict language - Haskell has good reason to employ them, but I don't think it's really worth it in other cases (at least, I actually know much about PureScript, but I don't think ATS needs it).
I think the way that ATS uses linear types for IO is slightly different - it uses them to e.g. ensure a handle is closed. Linearity does also have the curious benefit of making it possible to have lazy/strict evaluation be the same; you can rule out the example you provide and you can rule out the bottom type. Cheers, Vanessa McHale On 3/21/19 12:28 PM, 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 > <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 > <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/5391973a-4bd4-4238-a007-4dc08d1d9d4d%40googlegroups.com > <https://groups.google.com/d/msgid/ats-lang-users/5391973a-4bd4-4238-a007-4dc08d1d9d4d%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/b21006ff-bc7e-d828-1462-4d9c7103feae%40iohk.io.
signature.asc
Description: OpenPGP digital signature
