effects

Functions can have various effects that may be tracked by the typechecker [1]. These are described immediately after the : in the function definition (note that there should be no space between the ':' and the '<>'). As well as :<> meaning pure and : (no '<>') meaning any effects may occur, there are various other things that can appear between the '<>' symbols.

• !exn - the function possibly raises exceptions
• !ntm - the function possibly is non-terminating
• !ref - the function possibly updates shared memory, i.e. can read from or write to a location that one knows exists but does not own
• 0 - the function is pure (i.e. has no effects; this differs somewhat from normal notions of purity in other languages, as one would have to e.g. prove a function terminates)
• 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 is linear and can be called only once
• prf - the function is a proof function
• !wrt - indicates that a function may write to a location it owns; for instance, ptr_set incurs such an effect
• !laz - indicates a form of effect associated with lazy-evaluation; see the ATS2 tutorial page

These can be combined, e.g. <lincloptr1>. Function effects are all of sort eff.