Effect System

Anselm makes prodigious use of an effect system.

Allocators

I remain uncertain as to whether Anselm will allow for custom allocators, but treating allocation as an effect would be an incredibly natural way to introduce them.

Transparent vs. Opaque Effects

Depending on the circumstances, we might want to restrict the visibility of the effects of computations to those which enclose them. For example, if we have a function which internally mutates state, but only local state, in some cases we can treat that function as being, effectively, pure but in others we wouldn't. For example, an eventual goal is to add SMT-style proof automation to Anselm, but as a result we wouldn't want even internally stateful computations to appear in type-valued computation because otherwise elaboration into, e.g. WhyML could be tricky. Or in real-time code we might want to absolute ensure that no dynamic memory allocation occurs within the enclosed computation.

Gaunilo

Gaunilo's set of primitive effects are, for now, quite simple:

down
circle "bidi"
arrow
circle "total"
arrow
circle "div"

Unlike many other dependently-typed languages, Anselm has no totality checker. Instead, special recursion schemes (which are known to always terminate) are built into the language and endowed with the total effect.