No such control as far as I know. Personally, I feel that the design of effect-tracking in ATS2 is a failure.
I am not yet sure how to do it in ATS3. Or do it at all? On Thursday, May 30, 2019 at 9:50:45 AM UTC-4, Brandon Barker wrote: > > After sleeping on it, I realize part of my last email doesn't have much > merit: namely the part about applications being able to enforce purity by > using "pure" functions high up in the call stack (e.g. program in that > example); most of such functions are exactly the ones that need to be > impure, due to having to also deal with IO. > > Would it be possible to have the compiler allow the user to control the > default effect type of functions? > > > On Wednesday, May 29, 2019 at 10:34:11 PM UTC-4, Brandon Barker wrote: >> >> Actually maybe it isn't necessary to have compiler flags - it should be >> reasonable, *I think*, to just have your top-level program function, call >> it program, be pure, then you could have e.g. >> >> main0 = program >> >> Which would force all other functions below it to be pure. Using effmask >> if absolutely necessary - maybe have the compiler print warnings for these >> though. >> >> Also, if main0 = pureProgram is too extreme, or if one is making a >> library, then either important portions of the program, or of the public >> API, could be made pure (or effectfully annotated) in the way that one >> wants to do. >> Maybe this is even being done already by ATS programmers to some extent. >> >> Best, >> >> On Wednesday, May 29, 2019 at 10:27:56 PM UTC-4, Brandon Barker wrote: >>> >>> OK, cool, I'm not sure which of the listed effects >>> <https://github.com/githwxi/ATS-Postiats/wiki/effects>it is catching >>> on, but we can all agree it isn't pure! >>> >>> I think this could still be useful. Using effmask like this seems a bit >>> like using unsafePerformIO >>> <https://hackage.haskell.org/package/base-4.12.0.0/docs/System-IO-Unsafe.html#v:unsafePerformIO> >>> >>> in Haskell; not great, and the one time I've seen it used in a library, it >>> has bitten me - since the library author violated one of the safety tenants >>> - but supposedly there are some good uses for it ;-). >>> >>> In the end it is hard to get this perfect (you'd need some really nice >>> static analysis tools to check what you're linking in from C-land or other >>> FFIs I imagine), but maybe we can work towards safer code in this way >>> without undue burden on the programmer. >>> >>> On Wednesday, May 29, 2019 at 10:11:38 PM UTC-4, Richard wrote: >>>> >>>> >>>> >>>> On Wednesday, May 29, 2019 at 9:54:57 PM UTC-4, Brandon Barker wrote: >>>>> >>>>> Hi Richard - thanks for the instructive examples; I clarified a >>>>> related point on the wiki. >>>>> >>>>> >>>>> On Wednesday, May 29, 2019 at 9:12:07 PM UTC-4, Richard wrote: >>>>>> >>>>>> >>>>>> #include "share/atspre_staload.hats" >>>>>> >>>>>> implement main0() = () >>>>>> >>>>>> // If I am not mistaken, all functions in ats have all effects (i.e. >>>>>> :<1>) by default. >>>>>> // note, :<0> is equivalent to :<> >>>>>> >>>>>> // Just some thoughts.... >>>>>> >>>>>> fun terminating .<>. (n: int):<> int = n * n >>>>>> >>>>>> // >>>>>> // Here we require to provide proof that the function terminates >>>>>> // so, we just insist that it does (.<>.) >>>>>> // >>>>>> // Well it does not seem to be a very effectful function so sure >>>>>> // though, what is the significance of purity in this case? >>>>>> // >>>>>> // Effects tracking in ats is not exactly a contract >>>>>> // For example, >>>>>> >>>>>> val terminate = terminating(0xb505) >>>>>> >>>>>> // >>>>>> // This typechecks fine however, do you notice something strange >>>>>> about the resulting value? >>>>>> // Passing a value larger than the square root of INTMAX causes >>>>>> arithmetic overflow... >>>>>> // >>>>>> // In this case, what good is a function annotated as pure if it can >>>>>> produce arithmetic overflow? >>>>>> // >>>>>> // Let us look at a different example, lets use dependent types to >>>>>> flush out this potential bug... >>>>>> // >>>>>> >>>>>> stadef IMAX = 2147483647 >>>>>> >>>>>> fun dependent {n:int | n*n <= IMAX} (n: int(n)): int(n*n) = n*n >>>>>> >>>>>> // 'depend' below fails typechecking, >>>>>> // unsolved constraint: >>>>>> // (46341 * 46341) <= IMAX >>>>>> val depend = dependent(0xb505) >>>>>> >>>>>> >>>>>> // however this typechecks, >>>>>> val depend = dependent(0xb504) >>>>>> >>>>>> >>>>>> >>>>>> >>>>>> On Wednesday, May 29, 2019 at 1:14:19 PM UTC-4, Brandon Barker wrote: >>>>>>> >>>>>>> Hi Guys, Thanks for the discussion. >>>>>>> >>>>>>> As usual I don't fully understand or recall some of the relevant >>>>>>> issues. >>>>>>> >>>>>>> In the online editor I quickly tried out this: >>>>>>> >>>>>>> fun double (n: int) :<1> int = n + n >>>>>>> >>>>>>> val () = println! ("double(5) = ", double(5)) >>>>>>> >>>>>>> >>>>>>> Which works. But changing :<1> to :<0> fails to compile; i also >>>>>>> tried a non-polymorphic identity function for ints and had the same >>>>>>> result. >>>>>>> So what does :<0> really mean? >>>>>>> >>>>>>> I think if we had (1), a way to keep track of purity, i.e., any >>>>>>> expressions returning unit must be equivalent to the expression () >>>>>>> (hopefully this isn't hard to check..), and (2), a way to tell the >>>>>>> compiler >>>>>>> to assume that ":" assumes :<0> by default, then we might just get >>>>>>> purity >>>>>>> checking done for free. >>>>>>> >>>>>> >>>>>> I think that requiring all functions to be pure in the current >>>>>> implementation of ats2 would produce an environment that would greatly >>>>>> decrease programming productivity :) >>>>>> >>>>>> >>>>> >>>>> I agree, that in its current definition, "pure" is actually stronger >>>>> than what I had in mind. I think letting the programmer choose the >>>>> default >>>>> effect type of functions could be useful when executing a build (though >>>>> it >>>>> would also have to take this into account, ideally, when linking with >>>>> other >>>>> ATS libraries). >>>>> >>>>> I was going to see if I could get what I wanted, starting by doing >>>>> this, and playing around with eliminating effects that don't jive with my >>>>> notion of "sort of pure" ;-): >>>>> >>>>> implement >>>>> main0 () = { >>>>> val () = println! ("double(5) = ", double(5)) >>>>> } >>>>> >>>>> fun double .<>. (n: int) :<0> int = ( >>>>> // print 'h'; >>>>> n + n >>>>> ) >>>>> >>>>> >>>>> >>>>> Unfortunately, this resulted in an error that I don't have time to >>>>> dive into tonight (was using version 0.3.11 out of convenience). Online, >>>>> it >>>>> works (see attached image). However, if I uncomment the print 'h' line, >>>>> it >>>>> fails, but i can't see the error online. >>>>> >>>> >>>> When un-commenting >>>> // print 'h'; >>>> the typechecker issues a warning stating that >>>> some disallowed effects may be incurred: 1 >>>> This is expected behavior as the function signature states that it is >>>> pure (:<0>) >>>> >>>> To further illustrate the difficulty in relying on effects, one can >>>> just as easily silence the compiler with one of the >>>> "ats-swiss-army-knives", >>>> fun double .<>. (n: int):<> int = >>>> ( >>>> $effmask{1}(print 'h'); >>>> n + n >>>> ) >>>> >>>> Here, we just tell the compiler "look, just ignore this one" :) >>>> >>> -- 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 [email protected]. To post to this group, send email to [email protected]. 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/7c5d5ac4-aeb1-4638-bbcc-4aaa4bdea501%40googlegroups.com.
