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/ec901dd9-70b0-4054-81c8-564620d7f6e7%40googlegroups.com.
