There was some discussion on arithmetic overflow in the following archive:
https://sourceforge.net/p/ats-lang/mailman/ats-lang-users/?viewmonth=201304 Try to search 'overflow' to find those messages. Your observation is correct: static '+' and dynamic '+' do not agree. So the type-soundness of ATS needs to assume that no arithmetic overflow happens at run-time (if you use '+'). However, this is not a fundamental limitation of ATS. ###### Here is an example that shows a way to address the arith overflow issue: https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/MISC/arith_overflow.dats When doing binary search, the middle point can be computed using (l+r)/2, where l and r are left and right indices, respectively. But (l+r) may overflow. The above example shows a way to capture this potential overflow. To address this issue, one can use l+(r-l)/2 instead of (l+r)/2, and the example verifies it. On Wednesday, January 3, 2018 at 4:17:43 PM UTC-5, cmp xchg wrote: > > > 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/07d98e16-c31f-4170-a960-55adbfc422c7%40googlegroups.com.
