<p>Consider algebraic datatypes such as:</p>

<pre><code>data List a = Nil | Cons a (List a)
</code></pre>

<p>The return types of each constructor in a datatype are all the same: <code>Nil</code> and <code>Cons</code> both return <code>List a</code>. If we allow the constructors to return different types, we have a <a href="http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/data-type-extensions.html#gadt">GADT</a>:</p>

<pre><code>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 -&gt; NullableList a b -&gt; NullableList a NonEmpty
</code></pre>

<p><code>Occupied</code> has the type <code>a -&gt; NullableList a b -&gt; NullableList a NonEmpty</code>, while <code>Cons</code> has the type <code>a -&gt; List a -&gt; List a</code>. It is important to note that <code>NonEmpty</code> is a type, not a term. Another example:</p>

<pre><code>data Zero
data Succ n

data SizedList a t where
    Alone :: SizedList a Zero
    WithFriends :: a -&gt; SizedList a n -&gt; SizedList a (Succ n)
</code></pre>

<p>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.</p>

<pre><code>Inductive Parity := Even | Odd.

Definition flipParity (x:Parity) : Parity :=
  match x with
    | Even =&gt; Odd
    | Odd =&gt; Even
  end.

Fixpoint getParity (x:nat) : Parity :=
  match x with
    | 0 =&gt; Even
    | S n =&gt; 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 -&gt; Type :=
  Nil : forall P, ParityNatList P
| Cons : forall (x:nat) (P:option Parity), 
  ParityNatList P -&gt; ParityNatList 
  (match P, getParity x with
     | Some Even, Even =&gt; Some Even
     | Some Odd, Odd =&gt; Some Odd
     | _, _ =&gt; None
   end).
</code></pre>

<p>A side note: <a href="http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/kind-polymorphism-and-promotion.html">GHC has a mechanism for treating value constructors as type constructors</a>. 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.</p>

CC BY-SA 3.0
2012-03-08T18:14:07.413Z
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?
ninjagecko
CC BY-SA 3.0
2012-03-08T16:36:02.430Z
2012-03-08T16:36:02.430Z
jbapple
<p>Algebraic data types let you define types recursively. Concretely, suppose we have the datatype</p>

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

<p>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)$</p>

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

<p>and then defining $\mathsf{list}$ as </p>

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

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

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

<p>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:</p>

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

<p>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 <em>values</em> of the type theory. This lets you give types for length-indexed lists, and so on.</p>

CC BY-SA 3.0
2012-03-08T16:27:00.090Z
Thank you. Wouldn't that just mean, however, that "inductive type" in completely synonymous with "dependent type"?
ninjagecko
CC BY-SA 3.0
2012-03-08T16:38:10.367Z
@Neel: I've never seen types like `bush` called GADTs. I have seen them called nested or non-regular types.
jbapple
CC BY-SA 3.0
2012-03-08T16:56:40.317Z
@Neel, jbapple: Same here. A GADT is one where the type arguments can differ on the right-hand side of the arrow describing a constructor's type, not just on the left like in your example (note that e.g. SML always has allowed the latter).
Andreas Rossberg
CC BY-SA 3.0
2012-03-08T20:24:01.993Z
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.)
Neel Krishnaswami
CC BY-SA 3.0
2012-03-08T20:27:15.373Z
@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.
Neel Krishnaswami
CC BY-SA 3.0
2012-07-11T16:24:33.967Z
@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?
ninjagecko
CC BY-SA 3.0
2015-04-26T12:27:26.490Z
Sorry, for, perhaps, silly question, but what does mean the `Fⁱ(Ø)`? I.e. why it takes an empty set? Shouldn't it be `Fⁱ(i)?` *(which would stand in your formula for a function that takes every `i ∈ ℕ`)*?
Hi-Angel
CC BY-SA 3.0
2017-04-24T16:53:57.733Z
@Hi-Angel: $F^i$ means $F$ applied $i$ times, e.g., $F^3(x) = F(F(F(x)))$. So $F^1(\emptyset)$ only contains `Nil`, $F^2(\emptyset)$ contains all lists of length one (`Cons 1 Nil`, `Cons 2 Nil`, ...) and `Nil`, $F^3(\emptyset)$ contains all lists of length two and `Nil`, etc.
cic
CC BY-SA 4.0
2020-04-21T06:24:38.863Z
How can list (a type) be defined as a set?
Ell
CC BY-SA 3.0
2012-03-08T10:56:02.457Z
2012-03-08T10:56:02.457Z
Neel Krishnaswami
<p>Might anyone be able to explain the difference between:</p>

<ul>
<li>Algebraic Datatypes (which I am fairly familiar with)</li>
<li>Generalized Algebraic Datatypes (what makes them generalized?)</li>
<li>Inductive Types (e.g. Coq)</li>
</ul>

<p>(Especially inductive types.) Thank you.</p>

<lo.logic><pl.programming-languages><type-theory><dependent-type>
What's the difference between ADTs, GADTs, and inductive types?
ninjagecko
# What's the difference between ADTs, GADTs, and inductive types?

(Asked by: username_0 on 2012-03-08)

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.

**Tags:** lo.logic, pl.programming-languages, type-theory, dependent-type


---

## 2 answers

### Answer by username_2 on 2012-03-08. Score: 25 | Accepted answer

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.

> **Comments:**
> **username_0**: Thank you. Wouldn't that just mean, however, that "inductive type" in completely synonymous with "dependent type"?  
> **username_1**: @Neel: I've never seen types like `bush` called GADTs. I have seen them called nested or non-regular types.  
> **username_3**: @Neel, username_1: Same here. A GADT is one where the type arguments can differ on the right-hand side of the arrow describing a constructor's type, not just on the left like in your example (note that e.g. SML always has allowed the latter).  
> **username_2**: 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.)  
> **username_2**: @username_0: "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.  
> **username_0**: @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?  
> **username_4**: Sorry, for, perhaps, silly question, but what does mean the `Fⁱ(Ø)`? I.e. why it takes an empty set? Shouldn't it be `Fⁱ(i)?` *(which would stand in your formula for a function that takes every `i ∈ ℕ`)*?  
> **username_5**: @username_4: $F^i$ means $F$ applied $i$ times, e.g., $F^3(x) = F(F(F(x)))$. So $F^1(\emptyset)$ only contains `Nil`, $F^2(\emptyset)$ contains all lists of length one (`Cons 1 Nil`, `Cons 2 Nil`, ...) and `Nil`, $F^3(\emptyset)$ contains all lists of length two and `Nil`, etc.  
> **username_6**: How can list (a type) be defined as a set?  

---

### Answer by username_1 on 2012-03-08. Score: 20

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.

> **Comments:**
> **username_0**: 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?  

---

