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.
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this communityAlgebraic 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.
bush
called GADTs. I have seen them called nested or non-regular types.
$\endgroup$
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$
Jul 11, 2012 at 16:24
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.