25
$\begingroup$

When I first learned Haskell, I was told that you use data keyword to define an "algebraic data type", or a "sum type". Then I learned the idea of catamorphism, which is related to the "initial F-algebra" -- that all such "algebraic data types" can be encoded as the colimit of its finite approximations. The name "algebraic data type" is an attribute to the fact that we're using an algebra to generate the type.

Then, I saw an article by Jason Hu (in Chinese) that Haskell does not have algebraic data types, because Haskell does not enforce strict positivity. I'm not sure if this is true, because some types that are not strictly positive may also be generated "algebraically", for instance coinductive types can be generated by "final F-coalgebra".

I tried to find some relevant resources on the internet. Wikipedia says algebraic data types are types generated by taking sums or products of basic types, which I think is true, but it doesn't mention recursive cases, while positivity can only be discussed when you have type recursion.

$\endgroup$
5
  • $\begingroup$ Of interest: Agda Strict positivity $\endgroup$
    – Guy Coder
    Feb 27 at 23:26
  • $\begingroup$ I think most people in the community would not want to conflate algebraic types and co-algebraic types. And so, things that can be generated by a final F-coalgebra wouldn't be consisted "in some sense ‘algebraic’". $\endgroup$ Feb 27 at 23:40
  • $\begingroup$ Strict positivity and positive/negative types are orthogonal concepts. $\endgroup$
    – Szumi Xie
    Feb 28 at 1:54
  • $\begingroup$ @SzumiXie modified to address your comments. Thanks for the correction! $\endgroup$
    – ice1000
    Feb 28 at 5:25
  • 1
    $\begingroup$ Wikipedia is not to be trusted too much on these matters. $\endgroup$ Feb 28 at 9:08

1 Answer 1

22
$\begingroup$

[Note: After some helpful off-line remarks by Martín Escardó I have edited the part about general recursive types. It was at best misleading by trying to paint too simple a picture.]

I will start with the classic notion of universal algebra and develop from it algebraic datatypes. Then I will discuss how they relate to coalgebraic datatypes and recursive types found in programming languages. Hopefully this will bring some clarity to what is what.

Signatures in universal algebra

In universal algebra a signature is a list of operations with their arities $$\sigma = [(\mathsf{op}_1, n_1), \ldots, (\mathsf{op}_k, n_k)].$$ Here $\mathsf{op}_i$ are symbols and $n_i \in \mathbb{N}$. Universal algebra also has equations but those play no role here so we shall ignore them. For example, the signature for a group might be $[(\mathsf{e}, 0), (\mathsf{i}, 1), (\mathsf{m}, 2)]$, for unit, inverse and multiplication, respectively.

We define the set $T_\sigma$ of terms inductively as:

  • $\mathsf{op}_i(t_1, \ldots, t_{n_i}) \in T_\sigma$ for $i \leq k$ and $t_1, \ldots, t_{n_i} \in T_\sigma$

(There better be some nullary operations or else $T_\sigma$ is empty.)

Initial algebras for polynomial functors

At least this is how an old textbook on algebra might do it. Let us bring in some category theory. First, we replace arities as numbers with arities as sets. Thus, instead of saying that we have $n_i$ terms $t_1, \ldots, t_{n_i} \in T_\sigma$ we shall say that we have a map $t : N_i \to T_\sigma$.

Next, let us allow operations with parameters. Each symbol $\mathsf{op}_i$ shall have a parameter set $S_i$ and an arity $N_i$. For instance, scalar multiplication in a real vector space would have $S_i = \mathbb{R}$ and $N_i = \{\star\}$, because it is a unary operation on vectors parameterized by a real number. An operation without a parameter set is one whose parameter set is a singleton set.

Thus a signature looks like this: $$\sigma = [(\mathsf{op}_1, S_1, N_1), \ldots, (\mathsf{op}_k, S_k, N_k)].$$ It determines a functor $P_\sigma : \mathsf{Set} \to \mathsf{Set}$ given by $$P_\sigma(X) = S_1 \times X^{N_1} + S_2 \times X^{N_2} + \cdots + S_k \times X^{N_k},$$ known as a polynomial functor (for obvious reasons). In category-theoretic language, the set of terms $T_\sigma$ is just the initial $P_\sigma$-algebra. It is a fixed point of $P_\sigma$, $$T_\sigma \cong S_1 \times T_\sigma^{N_1} + S_2 \times T_\sigma^{N_2} + \cdots + S_k \times T_\sigma^{N_k}. $$ Note that $P_\sigma$ may have many fixed points. For example, the final $P_\sigma$-coalgebra is also such a fixed point.

Algebraic and coalgebraic datatypes

As a datatype, $T_\sigma$ would be described as follows (I am dropping the subscript $\sigma$):

data T : Set where
  op_1 : S_1 × (N_1 → T) → T
  ...
  op_k : S_k × (N_k → T) → T

So this is just a different notation for an algebraic signature. It therefore makes sense to call the type determined by it an algebraic or inductive datatype, provided such a datatype really is inductive, i.e., it satisfies a suitable induction or recursion principle witnessing its initiality.

(A side remark: the "strict positivity" requirement that proof assistants impose on inductive definitions is just their way of making sure that the underlying functor determined by the given signature is nice enough to have an initial algebra.)

Actually, we could describe the final coalgebra with the exact same data, by writing something like

codata T : Set where
  op_1 : S_1 × (N_1 → T) → T
  ...
  op_k : S_k × (N_k → T) → T

The information, namely the algebraic signature, is the same, but the constructed type is now the final coalgebra, so it makes sene to call it a coinductive datatype, provided it satisfies suitable principles witnessing the fact that it is a final coalgebra.

General recursive types

Observe that we may generate all polynomial functors $P_\sigma$ using pre-existing types, the type constructors $\times$ and $+$, and powers by pre-existing types $X \mapsto X^S$. In fact, we get precisely the polynomial functors this way.

General recursive types arise when we allow other type constructors, for example we include function spaces $\to$. This leads to various complications, because it is not even clear at first how to turn something like $$Q(X) = (\mathsf{Nat} \to X) + (X \to \mathsf{Bool})$$ into a functor. Is it covariant or contravariant? And once we do figure out how to turn $Q$ into a functor, it is not clear anymore whether we should be taking the initial algebra or the final coalgebra. Nevertheless, all these complications can be resolved with the aid of algebraically compact categories. Without going too much into the details of general recursive types, let me say that the standard way to treat them is to model them in a category where the initial algebra and the final coalgebra coincide. These categories are typically categories of domains or predomains and require some getting used to and cannot be thought of naively as sets.

Types in programming languages

A programming language might therefore support some selection of the following:

  1. algebraic datatypes, also known as inductive datatypes,
  2. coalgebraic datatypes, also know as coinductive datatypes,
  3. general recursive types.

There may be further nuances that arise from the fact that a real-world programming language is not the same thing as a mathematical model, but let us not worry about that too much.

Proof assistants: Agda data and Coq's Inductive are algebraic datatypes. Proof assistants make provisions for coalebraic datatypes by other means. They do not have general recursive types as those allow arbitrary recursive definitions, which makes it possible to inhabit all types (and thereby ruin the logical content of types). Here is how one can use recursive types in Haskell to inhabit every type without any explicit recursive calls:

data Magic a = Abracadabra (Magic a -> a)

evil :: a
evil = spell (Abracadabra spell)
  where
    spell :: Magic a -> a
    spell (Abracadabra x) = x (Abracadabra x)

Programming languages: they do not care about propositions-as-types, so they are free to admit general recursive types, which they often do. When the general recursive types are specialized to algebraic signatures, they may yield something that looks like an inductive datatype, or a coinductive datatype, or neither, depending on the details of the underlying semantics.

Haskell data definitions allow general recursive types. In particular, Haskell's

data Nat = Zero | Succ Nat

gives the inital/final solution for the functor $X \mapsto 1 + X$, which is not the natural numbers, but rather the domain of lazy natural numbers whose elements are of the form:

  • Succ (Succ (Succ (⋯ Succ Zero) ⋯))) – the natural numbers
  • Succ (Succ (Succ (⋯ Succ ⊥) ⋯))) – the partial numbers
  • Succ (Succ (Succ (⋯ ⋯))) – infinity

I am explaining all this to make a point: Haskell's natural numbers are both initial and final, but are computed in a different category so we cannot just pretend that they live in sets.

OCaml and SML recursive type definitions also allow general recursive types. In particular, OCaml's

type nat = Zero | Succ of nat

gives the initial/final algebra for the functor $X \mapsto 1 + X$, which is the natural numbers, because it is computed in a different category.

Disclaimers:

  • As Pierre-Marie points out in the comments, OCaml allows certain limited cases of coinductively defined values, such as let rec infinity = Succ infinity. However, these do not provide general coinductive types, only certain regular trees, so let us ignore them.

  • In the spirit of the previous disclaimer, we should be aware that Haskell and OCaml as real-world languages do not actually have a complete mathematical semantics, or at least not one that we would want to discuss here. The above remarks about recursive types in Haskell and OCaml should be understood as applying to smallish well-defined fragments of the languages.

$\endgroup$
10
  • 2
    $\begingroup$ Actually, your type is not an ADT in OCaml. It also has infinite inhabitants, e.g. let rec infty = Succ infty. Anyways, since OCaml also has pointer equality even if we disallowed this kind of loops we would still be able to observe differences between two instances of the same natural. $\endgroup$ Feb 28 at 10:07
  • $\begingroup$ Is there a reasonable characterization of what Ocaml really is doing? I consider the silliness with cyclic trees to be a design mistake, mostly. $\endgroup$ Feb 28 at 10:21
  • $\begingroup$ I think that the official phrasing is that OCaml is a practical programming language. Note that even if OCaml ADTs allow ill-founded inhabitants, they are still values so that you can't get a random error when forcing them. The intended model is the underlying heap memory representation with pointers and whatnot. $\endgroup$ Feb 28 at 10:31
  • $\begingroup$ Since when do you choose your words carefully to criticize? $\endgroup$ Feb 28 at 10:36
  • 1
    $\begingroup$ OCaml is a fantastic language and I have totally never signed an NDA with the INRIA to not rant about OCaml. Any contrary mention is war disinformation. Have I already mentioned how fantastic a language OCaml was? $\endgroup$ Feb 28 at 10:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.