We already know that given types, we can form new types with these types at hand (like pairs/tuples). An algebraic data type (ADT) is a kind of composite type, a type formed by combining other types. Values of algebraic types are analyzed with pattern matching, which identifies a value by its constructor or field names and extracts the data it contains.

In a nutshell, an ADT is something:

1. that you can do pattern match on,
2. that you can tell how a term can be constructed,
3. has finite numbers of constructors.

In other words, ADT describes how a term of a given type is constructed (from bottom to top). So, Coq’s Inductive keywords define ADTs. An ADT must require finite constructors of a given term while Co-Algebraic Data Types loosen this requirement and may contain infinite constructors, as we have already seen in inf-1 in B521.

Since we use lazy evaluation in Racket, we cannot check if a given term is really a well-formed ADT because totality and positivity are not checked. Languages like Haskell that lack such checks may allow an infinitely constructed term to be existing. Haskell only assumes an ADT has finite number of constructors but does not pose any restriction semantically.

In Coq’s manual:

The objects of an inductive type are well-founded with respect to the constructors of the type. We may use co-induction to relax this requirement. The ability to define coinductive types by constructors, hereafter called positive coinductive types, however, is known to break subject reduction.

For more information, please refer to Coinductive (chlipala.net).

Examples:

Definition Pair (A B: Type): Type := (A * B)%type.(* ADT *)
Inductive Union: Type :=
	| inl: A -> Union
	| inr: B -> Union
.

CoInductive stream : Set :=
	| seq: nat -> stream -> stream
.

Then what is a GADT? It is a generalization of parametric algebraic data types (first-class phantom type). In a GADT, the product constructors (called data constructors in Haskell) can provide an explicit instantiation of the ADT as the type instantiation of their return value, where, in ML and Haskell 98, the indices of the range of each data constructor must be type variables bound at the top level of the data type definition. There is no way to do what we did here, where we, for instance, say that TPlus is a constructor building a tbinop whose indices are all fixed at Nat.

GADT allow you to explicitly write down the types of the constructors. Coq’s Inductive data types are themselves GADTs.

-- Without GADT.
data Expr = I Int
          | B Bool           -- boolean constants
          | Add Expr Expr
          | Mul Expr Expr
          | Eq  Expr Expr    -- equality test

eval :: Expr -> Either Int Bool

eval (Add e1 e2) = eval e1 + eval e2 -- ??? we cannot add Bool to Int, but there is no way to check it.

{-# LANGUAGE GADTs #-}

data Expr a where
    I   :: Int  -> Expr Int
    B   :: Bool -> Expr Bool
    Add :: Expr Int -> Expr Int -> Expr Int
    Mul :: Expr Int -> Expr Int -> Expr Int
    Eq  :: Eq a => Expr a -> Expr a -> Expr Bool

eval :: Expr a -> a
eval (I n) = n
eval (B b) = b
eval (Add e1 e2) = eval e1 + eval e2
eval (Mul e1 e2) = eval e1 * eval e2
eval (Eq  e1 e2) = eval e1 == eval e2

To summarize, GADTs allows us to restrict the types of constructors and thus enable us to take advantage of Haskell's type system for our domain specific languages. “constructors as just being functions”.

data expr a where
	constant :: a -> expr a
  app      :: (expr s -> t) -> expr s -> expr t
  lam      :: expr s -> expr t -> expr (s -> t)

In particular, they ensure that any expr can be interpreted as a well-typed Haskell expression. Without using GADTs we'd need to use sum types to represent the values in our terms and handle type errors because we cannot encode types in expr and we must pattern match on each case at runtime.