What are "GADTs" in Haskell and what are some use-cases for them?

Generalized Algebraic Data Types (GADTs) are an extension of Haskell’s standard algebraic data types that allow more precise type information to be stored in the data constructors. This provides additional flexibility and expressiveness in the construction and pattern matching of data types.

To understand GADTs better, let’s first look at a simple example of a standard algebraic data type:

data Expr a where
  EInt :: Int -> Expr Int
  EBool :: Bool -> Expr Bool

Here, ‘Expr‘ is a polymorphic data type with a type variable ‘a‘. There are two data constructors, ‘EInt‘ and ‘EBool‘, that represent expressions of integers and booleans, respectively. The constructors store a single value of their respective types.

Now, let’s see how GADTs can improve this representation:

data Expr a where
  EInt :: Int -> Expr Int
  EBool :: Bool -> Expr Bool
  EAdd :: Expr Int -> Expr Int -> Expr Int
  EMul :: Expr Int -> Expr Int -> Expr Int
  EEq :: Expr Int -> Expr Int -> Expr Bool

With GADTs, we can define additional constructors like ‘EAdd‘, ‘EMul‘, and ‘EEq‘. Importantly, these constructors can now store more type information within them, allowing us to enforce different types for different operations in the data type definition.

Notice that the ‘EAdd‘ and ‘EMul‘ constructors accept two ‘Expr Int‘ values and return an ‘Expr Int‘ value. On the other hand, the ‘EEq‘ constructor accepts two ‘Expr Int‘ values but returns an ‘Expr Bool‘ value. This enforces stronger type guarantees in our data type, which can help catch errors early and improve optimizations.

Now let’s look at some use cases of GADTs.

1. **Expression evaluation**: GADTs can represent expressions with a well-defined type. This allows us to create an evaluator function that is total, meaning it can handle every possible input case without throwing a runtime error.

   eval :: Expr a -> a
   eval (EInt i) = i
   eval (EBool b) = b
   eval (EAdd e1 e2) = eval e1 + eval e2
   eval (EMul e1 e2) = eval e1 * eval e2
   eval (EEq e1 e2) = eval e1 == eval e2

The evaluator function pattern matches on the constructors and applies the appropriate operation, making use of the type information stored in the constructors.

2. **Typed embedding of domain-specific languages (DSLs)**: GADTs can be used to implement the type-safe embedding of domain-specific languages in Haskell. This is particularly useful for embedding languages with complex syntax and semantics that require strong type guarantees.

3. **Phantom types**: GADTs can be used together with phantom types to enforce additional invariants in the data type. Phantom types are type variables that don’t appear in the actual data constructors but are used to impose restrictions on the values.

Overall, GADTs provide a powerful way to express complex, statically-typed data structures, making it easier to write safe and efficient code in Haskell.