21
$\begingroup$

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.

$\endgroup$
21
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ Thank you. Wouldn't that just mean, however, that "inductive type" in completely synonymous with "dependent type"? $\endgroup$ – ninjagecko Mar 8 '12 at 16:27
  • 4
    $\begingroup$ @Neel: I've never seen types like bush called GADTs. I have seen them called nested or non-regular types. $\endgroup$ – jbapple Mar 8 '12 at 16:38
  • 3
    $\begingroup$ Nested types are a special case of GADTs. The critical feature of a GADT is simply that it is a recursive definition at higher kind. (Changes to the rhs is basically syntactic sugar for adding a type equality as a component of the constructor.) $\endgroup$ – Neel Krishnaswami Mar 8 '12 at 20:24
  • 4
    $\begingroup$ @ninjagecko: "Inductive types" are types given semantics as the least fixed point of a constructor. Not all types can be described this way (functions cannot, and neither can infinite types such as streams). Dependent types describe types which permit program terms to occur in them (that is, types can "depend on" terms). Since Coq is a dependent type theory, the inductive types it lets you define are also dependent. But non-dependent type theories can support inductive types as well, and those inductive types won't be dependent. $\endgroup$ – Neel Krishnaswami Mar 8 '12 at 20:27
  • 2
    $\begingroup$ @NeelKrishnaswami: Would you be so kind as to clarify your answer by enumerating the "first few smallest" elements of the types of bush a? In this example, is it Nest Leaf(a) Leaf(a) Leaf(a) Leaf(a), or Nest ((Nest Leaf(a) Leaf(a)) (Nest Leaf(a) Leaf(a))) as one example of the set? $\endgroup$ – ninjagecko Jul 11 '12 at 16:24
19
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thank you. "Inductive types in programming languages that have dependent types" What then would an inductive type look like in a language with no dependent types, and can you have non-inductive (but GADT-like) dependent types? $\endgroup$ – ninjagecko Mar 8 '12 at 18:14

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.