[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. Also, in most applications we would include among the terms some variables, but we're ignoring that point also.
Note that $T_\sigma$ satisfies the isomorphism
$$T_\sigma \cong T_\sigma^{n_1} + \cdots + T_\sigma^{n_i}.$$
If we write $P_\sigma(X) = X^{n_1} + \cdots + X^{n_i}$ then the above is written more succinctly as $T_\sigma \cong P_\sigma(T_\sigma)$. There are many such fixed points of $P_\sigma$, but $T_\sigma$ is special because it is the smallest one (in a sense to be made precise below).
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$ where $N_i$ has $n_i$ elements (and henceforth we use $N_i$ directly, forgetting about $n_i$).
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:
- algebraic datatypes, also known as inductive datatypes,
- coalgebraic datatypes, also know as coinductive datatypes,
- 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 numbersSucc (Succ (Succ (⋯ Succ ⊥) ⋯))) – the partial numbersSucc (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.
