today i read the blog post about dependent types and ats [1]
the following function was given:
fun add_int {m,n:int} (a: int m, b: int n): int (m + n) = a + b
however, i assume that the sort (n:int) uses infinite precision integers whereas
the type of a uses 32bit ints. then the dependent type int(m+n) only holds if
the addition does not wrap. i tried the following example which should not
compile,
but it does. that is bad because accessing an array in (gtz) would lead to
crashes.
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"
fun gtz {n:int| n>0 } ( a: int(n) ) : int(n) = a where {
val () = println!("a=", a)
}
fun add {m,n:int} ( a: int(m), b: int(n) ) : int(m+n) = a+b
implmnt main0 ( ) = {
val () = println!("1+2=", add(1,2))
val () = println!("=", add(0x80000000, 0x80000000))
val n = add(0x80000000, 0x7fffffff)
val n = gtz(n)
//val m = add(1,~1)
//val m = gtz(m)
}
$ ./test
1+2=3
=0
a=-1
or did i misunderstood something?
[1](https://bluishcoder.co.nz/2018/01/03/writing-basic-proofs-in-ats.html)
--
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/9f7773df-9e46-4039-a0a1-30b9d46fb8bb%40googlegroups.com.
