Features

Function Effects

Note

This part is taken from Chris Double’s blog and a discussion on ATS google group. Thanks to all the contributions in the blog and group thread.

For a function like fun foo (someargs: sometype):<> sometype, the :<> part is used to describe effects of functions. There is a sort eff exclusively for function effects. You can do things like :<>, :<lin,prf> and so on. The meaning of them are as follows.

:<>

pure, no effects at all

!exn

the function possibly raises exceptions

!ntm

the function possibly is non-terminating

!ref

the function possibly updates shared memory, which means reading from or writing to a location that it knows exists but does not own.

!wrt

(ATS2 only) the function may write to a location it owns

0

the function is pure (has no effects)

1

the function can have all effects

fun

the function is an ordinary, non-closure, function

clo

the function is a stack allocated closure

cloptr

the function is a linear closure that must be explicitly freed

cloref

the function is a peristent closure that requires the garbage collector to be freed.

lin

the function i slinear and can be called only once

prf

the function is a proof function

Quantifiers

In ATS, [] is mostly used as extential quantifier, while {} is mostly used as universal quantifier.

For example, suppose MUL encodes the multiplication relationship as defined here, we can write something like this.

prfun mutiplication_is_total {m,n:int} (): [p:int] MUL (m, n, p)

which will be interpreted as

For all integers m and n, there exists some integer p such that MUL (m, n, p) is ture.