#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 :)
--
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/dff8a79d-1a11-471b-9ae8-10d3b54fc20f%40googlegroups.com.
