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.
--
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 ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
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/9b7facd2-db6d-4c90-b6b8-ba34bba7cb5d%40googlegroups.com.
