This is probably obvious or something I just missed, but I see it now and
then, e.g. the “<>” in the function below
fun string_get_char_at
{n:int}
{i:nat | i < n} (
str: string n, i: size_t i
) :<> c1har
= “atspre_string_get_char_at”
I think you’ve got all of them 
In ATS2, there is also ‘!wrt’, which indicates that a function may write to
a location it owns. For instance, ptr_set incurs such an effect. In
contrast, ‘!ref’ means reading from or writing to a location that one knows
exists but does not own.
:<> means that this functions is pure, that is, it does not cause
observable effects.
As well as :<> meaning pure there are various other things that can appear
between the ‘<>’ symbols. I describe some of them here:
http://www.bluishcoder.co.nz/2010/06/13/functions-in-ats.html
Basically:
!exn - the function possibly raises exceptions
!ntm - the function possibly is non-terminating
!ref - the function possibly updates shared memory
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
These can be combined, eg. .
Are there any I’ve missed or got wrong?
Yes. Exclusively for function effects.
I was looking over list.sats and noticed what looked like a sort called
"eff". Is this a sort exclusively for function effects?