What's the difference between ADTs, GADTs, and inductive types?

Question

Might anyone be able to explain the difference between:

• Algebraic Datatypes (which I am fairly familiar with)
• Generalized Algebraic Datatypes (what makes them generalized?)
• Inductive Types (e.g. Coq)

(Especially inductive types.) Thank you.

Answer 1

Algebraic data types let you define types recursively. Concretely, suppose we have the datatype

$$ \mathsf{data\;list = Nil \;\;|\;\; Cons\;of\;\mathbb{N} \times list} $$

What this means is that $\mathsf{list}$ is the smallest set generated by the $\mathsf{Nil}$ and $\mathsf{Cons}$ operators. We can formalize this by defining the operator $F(X)$

$$ F(X) == \{ \mathsf{Nil} \} \cup \{ \mathsf{Cons}(n, x) \;|\; n \in \mathbb{N} \land x \in X \} $$

and then defining $\mathsf{list}$ as

$$ \mathsf{list} = \bigcup_{i \in \mathbb{N}} F^i(\emptyset) $$

A generalized ADT is what we get when define a type operator recursively. For example, we might define the following type constructor:

$$ \mathsf{bush}\;a = \mathsf{Leaf\;of\;}a \;\;|\;\; \mathsf{Nest\;of\;bush}(a \times a) $$

This type means that an element of $\mathsf{bush\;}a$ is a tuple of $a$s of length $2^n$ for some $n$, since each time we go into the $\mathsf{Nest}$ constructor the type argument is paired with itself. So we can define the operator we want to take a fixed point of as:

$$ F(R) = \lambda X.\; \{ \mathsf{Leaf}(x) \;|\; x \in X\} \cup \{ \mathsf{Nest}(v) \;|\; v \in R(X) \} $$

An inductive type in Coq is essentially a GADT, where the indexes of the type operator are not restricted to other types (as in, for example, Haskell), but can also be indexed by values of the type theory. This lets you give types for length-indexed lists, and so on.

Answer 2

Consider algebraic datatypes such as:

data List a = Nil | Cons a (List a)

The return types of each constructor in a datatype are all the same: Nil and Cons both return List a. If we allow the constructors to return different types, we have a GADT:

data Empty -- this is an empty data declaration; Empty has no constructors
data NonEmpty

data NullableList a t where
    Vacant :: NullableList a Empty
    Occupied :: a -> NullableList a b -> NullableList a NonEmpty

Occupied has the type a -> NullableList a b -> NullableList a NonEmpty, while Cons has the type a -> List a -> List a. It is important to note that NonEmpty is a type, not a term. Another example:

data Zero
data Succ n

data SizedList a t where
    Alone :: SizedList a Zero
    WithFriends :: a -> SizedList a n -> SizedList a (Succ n)

Inductive types in programming languages that have dependent types allow the return types of the constructors to depend on the values (not just the types) of the arguments.

Inductive Parity := Even | Odd.

Definition flipParity (x:Parity) : Parity :=
  match x with
    | Even => Odd
    | Odd => Even
  end.

Fixpoint getParity (x:nat) : Parity :=
  match x with
    | 0 => Even
    | S n => flipParity (getParity n)
  end.

(*
A ParityNatList (Some P) is a list in which each member
is a natural number with parity P.
*)

Inductive ParityNatList : option Parity -> Type :=
  Nil : forall P, ParityNatList P
| Cons : forall (x:nat) (P:option Parity), 
  ParityNatList P -> ParityNatList 
  (match P, getParity x with
     | Some Even, Even => Some Even
     | Some Odd, Odd => Some Odd
     | _, _ => None
   end).

A side note: GHC has a mechanism for treating value constructors as type constructors. This is not the same as the dependent inductive types that Coq has, but it lessens the syntactic burden of GADTs somewhat, and it can lead to better error messages.