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/94f30ac7-5f51-44f2-a490-1b4e93093fc9%40googlegroups.com.
