Type-Safe Expression Evaluators with ADTs

Hello! Welcome to the next lesson in our course on programming theory.

In our last few lessons, we've assembled the core toolkit of the functional programmer's approach to data: defining data structures with product types and sum types (together, ADTs), and processing them elegantly with pattern matching.

Today, we'll synthesize these concepts to tackle a classic and powerful application: building a type-safe expression evaluator. This is a cornerstone pattern in functional programming, demonstrating how to embed the rules of a small language directly into the type system, catching errors at compile time rather than runtime.

This lesson directly addresses the learning outcome: Model a type-safe expression evaluator using algebraic data types, demonstrating a central design pattern of functional languages.

We will proceed in three steps:

1. We'll start by defining a simple expression language using the ADT and pattern matching techniques you're now familiar with.
2. We'll identify a crucial weakness in this simple model: it can represent nonsensical programs (like 3 + true), pushing type errors to runtime.
3. Finally, we'll introduce Generalized Algebraic Data Types (GADTs), an extension to ADTs that allows us to build a truly type-safe model where such nonsensical programs are impossible to even construct.

1. Modeling Expressions with ADTs

Let's say we want to represent and evaluate simple arithmetic expressions involving integers, like (5 + 10) * 2. Based on our previous lessons, a natural way to model this in a functional language is with a recursive sum type.

In a Haskell-like syntax, this would be:

data Expr =
    LitInt Int         -- A literal integer, e.g., 5
  | Add Expr Expr      -- The addition of two expressions
  | Mul Expr Expr      -- The multiplication of two expressions

Here, Expr is a sum type with three variants (constructors): LitInt, Add, and Mul. The Add and Mul constructors are recursive, each containing two sub-expressions.

An expression like (5 + 10) * 2 would be represented by the value:
Mul (Add (LitInt 5) (LitInt 10)) (LitInt 2)

Writing an evaluator for this is a straightforward application of pattern matching, as we saw in the last lesson.

eval :: Expr -> Int
eval (LitInt n)   = n
eval (Add e1 e2) = (eval e1) + (eval e2)
eval (Mul e1 e2) = (eval e1) * (eval e2)

This is clean and declarative. Your reference text, Concepts in Programming Languages, shows an almost identical structure using Scala's case class mechanism, which, as we've discussed, is an object-oriented implementation of ADTs.

2. The Limits of Simple ADTs: The Problem of Type Safety

The Expr type works perfectly as long as our language only contains integers. But what happens when we want to extend our language? Let's add booleans and conditional if-then-else expressions.

Our ADT might now look like this:

data Expr =
    LitInt Int
  | LitBool Bool
  | Add Expr Expr
  | If Expr Expr Expr  -- If <condition> then <branch1> else <branch2>

Now, we have a serious problem. Our Expr type is too permissive. It allows us to construct values that represent nonsensical programs. For example:

• Add (LitInt 3) (LitBool True)
• If (LitInt 5) (LitInt 1) (LitInt 2)

The first expression tries to add an integer and a boolean. The second uses an integer as the condition for an If expression. These are type errors. However, with our current Expr definition, they are perfectly valid values of the Expr type.

An eval function would have to handle these invalid states at runtime, likely by throwing an exception. This undermines the goal of using the type system to guarantee correctness. The problem is that the type Expr doesn't distinguish between an expression that produces an integer and one that produces a boolean.

3. The Solution: Generalized Algebraic Data Types (GADTs)

To solve this, we need a way to encode the result type of an expression within the type of the expression itself. We want a type like Expr Int for expressions that evaluate to an integer, and Expr Bool for those that evaluate to a boolean.

This is exactly what Generalized Algebraic Data Types (GADTs) are for. A GADT looks like a regular ADT, but it allows each constructor to explicitly specify the type of the value it creates. This gives us fine-grained control over what values can be constructed.

The following resource provides a clear motivation for GADTs and shows how they are defined in OCaml.

Let's look at the GADT for our expression language, this time using Haskell's GADT syntax, which is quite explicit.

data Expr a where
  LitInt  :: Int -> Expr Int
  LitBool :: Bool -> Expr Bool
  Add     :: Expr Int -> Expr Int -> Expr Int
  If      :: Expr Bool -> Expr a -> Expr a -> Expr a

Let's break this down:

• data Expr a where ...: This declares a GADT named Expr which is parameterized by a type a. This a will represent the result type of the expression.
• LitInt :: Int -> Expr Int: The LitInt constructor takes an Int and produces a value of type Expr Int.
• LitBool :: Bool -> Expr Bool: The LitBool constructor takes a Bool and produces a value of type Expr Bool.
• Add :: Expr Int -> Expr Int -> Expr Int: The Add constructor is the key. It only accepts two arguments of type Expr Int and produces an Expr Int.
• If :: Expr Bool -> Expr a -> Expr a -> Expr a: The If constructor requires its first argument (the condition) to be an Expr Bool. It requires the next two arguments (the branches) to be of the same type, Expr a, and the whole expression also has that type.

With this GADT, the nonsensical expressions from before are now compile-time errors.

• Add (LitInt 3) (LitBool True): This is rejected. The second argument to Add must be Expr Int, but LitBool True has type Expr Bool.
• If (LitInt 5) ...: This is rejected. The first argument to If must be Expr Bool, but LitInt 5 has type Expr Int.

The evaluator function now has a much more revealing type signature: eval :: Expr a -> a. It takes an expression of type a and returns a value of type a.

eval :: Expr a -> a
eval (LitInt n)    = n
eval (LitBool b)   = b
eval (Add e1 e2)   = eval e1 + eval e2
eval (If c t e)    = if eval c then eval t else eval e

When the compiler type-checks this function, pattern matching on a GADT gives it extra information. For example, when it sees the pattern Add e1 e2, it knows from the GADT definition that the type of the whole pattern is Expr Int. Therefore, the result of the eval must be an Int, and the expression eval e1 + eval e2 is correctly typed.

This pattern of using a GADT to represent the abstract syntax tree of a language is extremely powerful and is used to implement type-safe compilers and domain-specific languages (DSLs).

For a more advanced look at this pattern in action, the following video shows how to build a type-safe interpreter for a small lambda calculus.

Conclusion

Today we saw how to move from a simple but unsafe data model to a highly robust, type-safe one by leveraging more advanced features of a functional type system.

Key Takeaways:

• A standard ADT is excellent for modeling the shape of data like an expression tree, and pattern matching is the natural way to process it.
• However, a simple ADT can be too permissive, allowing the representation of ill-typed programs that lead to runtime errors.
• Generalized Algebraic Data Types (GADTs) solve this by allowing constructors to specify precise return types. This lets us encode the static semantics (type rules) of a language directly into its data representation.
• The result is a model where ill-typed programs are un-representable and are caught at compile time, a core tenet of modern functional programming. This pattern is fundamental to building safe compilers, interpreters, and DSLs.

Next Lesson Preview:

Having seen a sophisticated application of ADTs, we will step back slightly to examine another, more common, but equally powerful use of sum types. In the next lesson, we will explore how sum types like Option/Maybe are used to handle the absence of a value, providing a type-safe alternative to null references and preventing a whole class of common runtime errors.