Generalized algebraic data types

Created: 2023-01-12 16:31

Generalized algebraic data type

generalization of parametric algebraic data types

data Expr a where
    ExpBool  :: Bool     -> Expr Bool
    ExpInt   :: Int      -> Expr Int
    ExpEqual :: Expr Int -> Expr Int  -> Expr Bool

By pattern matching on a GADT (on the value level) we discover some information about it from the type level. This is not the case with regular ADTs. Here’s an extended example A little type checker

Example, given the following definition of natural numbers and Vector.

data Nat = Zero | Succ Nat
 
data Vec :: Type -> Nat -> Type where
  Nil  :: Vec a 'Zero
  Cons :: a -> Vec a n -> Vec a ('Succ n)

We can define a total head function that doesn’t require pattern matching on the Nil case, since there will never be a Nil case.

head :: Vec a ('Succ n) -> a
head :: (Cons x _) = x

And pattern matching on Nil would result in an error, since GHC knows that 'Succ a has no Nil case.

head :: Vec a ('Succ n) -> a
head :: Nil = _