Ann a is the quotient of a by the total relation.

What's so special about the total relation?

There are only two relations which can be defined generically on all sets: the empty relation and the total relation (this can be proved by parametricity). The quotient by the empty relation is Identity. So the only interesting generic quotient is Ann.

Strictly speaking, sets are also equipped with the equality relation (and you can derive the disequality relation from it). But quotienting by the equality relation is the same as quotienting by the empty relation; and quotienting by the disequality relation is the same as quotienting by the total relation.

Other quotients can be defined on individual sets using abstract types.

A consequence of defining Ann generically on types is that it turns Ann into a functor. The functor structure is not particularly intersting. But Ann is also a monad.

(>>=) :: Ann a -> (a -> Ann b) -> Ann b

That is: you are allowed to “look inside” an Ann a only if you you are producing an Ann b to begin with. The program is not allowed to depend on the choice of representative, yet (>>=) gives the representative for us to play with. But it's alright: it's only going to affect the representative in Ann b, on which the program cannot depend either.

Something that I'd like to point out is that you really need the a in the (a -> Ann b) argument. The reason is that Ann is not isomorphic to Const (): Ann b is isomorphic to () if and only if b is inhabited. Ann Void, on the other hand, is isomorphic to Void. There is a sense in which all that's interesting about Ann stems from this fact.

The monadic (>>=) is more or less explicitly in use in many dependently typed theories (it is pretty hidden, but there in the typing rules for Prop in Coq). For further reading see [Propositions as [Types] ](https:/ieeexplore.ieee.orgabstractdocument8133549) and Implicit and noncomputational arguments using monads.

Algebras of Ann

I haven't talked about return yet

'return' :: a -> Ann a

It is the canonical projection to Ann a. It's exported as project as well.

This is really not relevant for the design or usage of the library, but it's a natural question to ask: the algebras of Ann (as a monad) are sets with at most 1 element. Let α :: Ann A -> A be such an algebra. Since Ann A has at most one element, α is constant. But, by the laws of algebra, we also have α ∘ return = id, in particular id :: A -> A is constant, therefore A has at most 1 element.

Conversely, if A has at most 1 element, then Ann A is isomorphic to A, in particular A is an algebra.

Is there an equivalent for subsets?

Frankly at this point, this is just me rambling about stuff that I find interesting. I'll get back to relevant stuff in the next section.

Subsets are the dual of quotients (in category-theory terms, quotients are co-equalisers while subsets are equalisers). However, the category of set is not its own dual, so that there is an interesting phenomenon for one doesn't imply that there is to the other.

In the case at hand, there are two generically definable predicates as well. The empty predicate and the full predicate. They both define boring subset (the empty set, and the identity functor, respectively). So really, Ann is the only interesting case of the bunch.

Extracting and IO

The type of extract is

extract :: Ann a -> IO a

There can't be a function `Ann a -> a` as this violates the quotient condition (concretely that the program isn't affected by the choice of representative of 'Ann a'). Well, more precisely, if such a function exists, it must be constant. The existence of such a function is a form of choice (of the axiom of choice fame). It's a very powerful principle, and probably not desirable. I should give a citation here, but no source comes to mind at the moment. You will have to trust me that in dependently typed language, this is equivalent to choice (in particular it implies the excluded middle, if 'Ann a' is used to represent propositions).

Ok, back to IO. We don't want the choice of representative to affect the semantics of the program, but we still want to print it out, so that the user get their debug message or whatnot. IO is our solution because it is allowed to do non-deterministic actions in IO (and printing usually involves IO, so it doesn't cost much). So the semantics of extract is “choose an arbitrary representative“; this representative need not be the same each time. Of course we don't actually want an arbitrary representative to be printed out: we want the one we put in. It would be difficult to give a different implementation anyway. So we know, that, really, we will get the representative we put in. But, strictly speaking, this is not, strictly speaking, part of the semantics of the function (at least I don't know how to make it so; it would be really nice to be able to).

This same trick is used in Tackling the awkward squad.

Quotients and equivalence relations

This is even less related to the core of the package than the rest of this section, but while we are on the subject of quotients, I'd like to address a point.

You may have noticed that I repeatedly spoke of quotienting by “a relation” throughout this document. If you are like me, though, you may have been taught that a set is quotiented by an equivalence relation. It's because equivalence classes form an equivalence relation. But it isn't essential to the definition of quotient.

A quotient \(X/R\) of a set \(X\) is defined by its universal property. Namely that a function \(f \in X/R \rightarrow C\)` is the same thing as a function \(f' \in X \rightarrow C\) such that \(x R y \Longrightarrow f x = f y\). That \(R\) is an equivalence relation doesn't play a role in this definition. It turns out, however, that quotienting by \(R\) or by its reflexive, symmetric and transitive closure yields the same set.