OK, Perhaps playing around with your Command code <https://groups.google.com/d/msg/ats-lang-users/fICcWumT9RE/x0LW1StuAQAJ>, and if needed, adding some extra syntax for it in ATS3, might be promising.
Incidentally, why is it needed to be a polymorphic function instead of a function template? Belated apologies for hijacking this discussion. On Thursday, May 30, 2019 at 9:55:51 AM UTC-4, gmhwxi wrote: > > 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/1c4e3296-1c65-4685-b897-020bf297c5a7%40googlegroups.com.
