>>Incidentally, why is it needed to be a polymorphic function instead of a function template?
For otherwise the Bind constructor cannot be properly handled: The type variables 'a' and 'b' are unknown at run-time. On Thu, May 30, 2019 at 10:43 AM Brandon Barker <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/ats-lang-users/1c4e3296-1c65-4685-b897-020bf297c5a7%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 [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/CAPPSPLrAb%3DeewBBqCWZu80%3DquF0N9hZG75sfhRks%3DoM0VYLWqQ%40mail.gmail.com.
