Function Effects


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
the function possibly raises exceptions
the function possibly is non-terminating
the function possibly updates shared memory, which means reading from or writing to a location that it knows exists but does not own.
(ATS2 only) the function may write to a location it owns
the function is pure (has no effects)
the function can have all effects
the function is an ordinary, non-closure, function
the function is a stack allocated closure
the function is a linear closure that must be explicitly freed
the function is a peristent closure that requires the garbage collector to be freed.
the function i slinear and can be called only once
the function is a proof function


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.