lectures-1-2-3.md

What is algebraic about algebraic effects and handlers?

The purpose of the first lecture is to review algebraic theories and related concepts, and connect them with computational effects. We shall start on the mathematical side of things and gradually derive from it a programming language.

The contents of this lecture is a bit ambitious. It is likely that the part about comodels will spill over to the second lecture.

Outline

• signatures, terms, and algebraic theories
• models of an algebraic theory
• free models of an algebraic theory
• generalization to parameterized operations with arbitrary arities
• sequencing and generic operations
• handlers
• comodels and tensoring of comodels and models

Reading material

Pretty much everything that will be said in the first lecture is written up in What is algebraic about algebraic effects and handlers?, which still a bit rough around the edges, so if you see a typo please let me know.

Problems

Problem: the theory of an associative unital operation

Consider the theory T of an associative operation with a unit. It has a constant ε and a binary operation · satisfying equations

(x · y) · z = x · (y · z)
ε · x = x
x · ε = x

Give a useful description of the free model of T generated by a set X. You can either guess an explicit construction of free models and show that it has the required universal property, or you can analyze the free model construction (equivalence classes of well-founded trees) and provide a simple description of it.

Problem: the theory of apocalypse

We formulate an algebraic theory Time in it is possible to explicitly record passage of time. The theory has a single unary operation tick and no equations. Each application of tick records the passage of one time step.

Problem: Give a useful description of the free model of the theory, generated by a set X.

Problem: Let a given fixed natural number n be given. Describe a theory Apocalypse which extends the theory Time so that a computation crashes (aborts, necessarily terminates) if it performs more than n of ticks. Give a useful description of its free models.

Advice: do not concern yourself with any sort of operational semantics which somehow "aborts" after n ticks. Instead, use equations and postulate that certain computations are equal to an aborted one.

Problem: the theory of partial maps

The models of the empty theory are precisely sets and functions. Is there a theory whose models form (a category equivalent to) the category of sets and partial functions?

Recall that a partial function f : A ⇀ B is an ordinary function f : S → B defined on a subset S ⊆ A. (How do we define composition of partial functions?)

Problem: models in the category of models

In Example 1.27 of the reading material it is calculated that a model of the theory Group in the category Mod(Group) is an abelian group. We may generalize this idea and ask about models of theory T₁ in the category of models Mod(T₂) of theory T₂.

The tensor product T₁ ⊗ T₂ of algebraic theories T₁ and T₂ is a theory such that the category of models of T₁ in the category Mod(T₂) is equivalent to the category of models of T₁ ⊗ T₂.

Hint: start by outlining what data is needed to have a T₁-model in Mod(T₂) is, and pay attention to the fact that the operations of T₁ must be interpreted as T₂-homomorphisms. That will tell you what the ingredients of T₁ ⊗ T₂ should be.

Problem: Morita equivalence

It may happen that two theories T₁ and T₂ have equivalent categories of models, i.e.,

Mod(T₁) ≃ Mod(T₂)

In such a case we say that T₁ and T₂ are Morita equivalent.

Let T be an algebraic theory and t a term in context x₁, …, xᵢ. Define a definitional extension T+[op:=t] to be the theory T extended with an additional operation op and equation

x₁, …, xᵢ | op(x₁, …, xᵢ) = t

We say that op is a defined operation.

Problem: Confirm the intuitive feeling that T+[op:=t] by proving that T and T+[op:=t] are Morita equivalent.

Problem: Formulate the idea of a definitional extension so that we allow an arbitrary set of defined operations, and show that we still have Morita equivalence.

Problem: the theory of a given set

Given any set A, define the theory T(A) of the set A as follows:

• for every n and every map f : Aⁿ → A, op(f) is an n-ary operation

• for all f : Aⁱ → A, g : Aʲ → A and h₁, …, hᵢ : Aʲ → A, if

    f ∘ (h₁, …, hᵢ) = g
  

  then we have an equation

    x₁, …, xⱼ | op(f)(op(h₁)(x₁,…,xⱼ), …, hᵢ(x₁,…,xⱼ)) = g(x₁, …, xⱼ)
  

Problem: Is T({0,1}) Morita equivalent to another, well-known algebraic theory?

Problem: a comodel for non-determinism

In Example 4.6 of the reading material it is shown that there is no comodel of non-determinism in the category of sets. Can you suggest a category in which we get a reasonable comodel of non-determinism?

Problem: formalization of algebraic theories

If you prefer avoiding doing Real Math, you can formalize algebraic theories and their comodels in your favorite proof assistant. A possible starting point is this gist, and a good goal is the construction of the free model of a theory generated by a set (or a type).

Because the free model requires quotienting, you should think ahead on how you are going to do that. Some possibilities are:

• use homotopy type theory and make sure that the types involved are h-Sets
• use setoids
• suggest your own solution

It may be wiser to first show as a warm-up exercise that theories without equations have initial models, as that only requires the construction of well-founded trees (which are inductive types).