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/cf518fbe-ddda-49a5-b8e3-f4a525b042c1%40googlegroups.com.
