💻 usethe.computer

Paper of the Day: “Generalized Algebraic Data Types and Object-Oriented Programming”
by Andrew Kennedy and Claudio V. Russo

2017-11-29

Today’s POTD presents a translation of a great tool from the functional programming community into the more mundane world of 90s-style object-oriented programming languages.

Since this particular idea has been slow to percolate through the programming world at large, this one will take a little buildup.

The algebraic data types (ADTs) provided by many functional programming language permit us to easily express recursive, polymorphic data structures built from alternations (sums) or combinations (products) of other types; pattern matching syntax lets us process them straightforwardly.

This is extremely helpful when defining “language translators” of the sort that sneak in to every programming project, whether one notices them or not. For example, we might define a simple language of expressions on integers, and an evaluation function for it (in Haskell syntax):

data Expr =
    Literal Int
  | Add Expr Expr
  | Sub Expr Expr
  | Mul Expr Expr
  | Div Expr Expr

eval :: Expr -> Int
eval (Literal n) = n
eval (Add e1 e2) = eval e1 + eval e2
eval (Sub e1 e2) = eval e1 - eval e2
eval (Mul e1 e2) = eval e1 * eval e2
eval (Div e1 e2) = eval e1 `div` eval e2

According to the folklore, those of us working in more common object-oriented languages can implement the same logic, using a class hierarchy with dynamic (virtual) dispatch to stand in for our sum type and pattern matching. It’s a little more wordy, but it accomplishes the same goal, and the translation is more-or-less mechanical with some practice. In C# (forgive me: I like lambda syntax and hate boilerplate, so it will be a bit terser than it could have been), we’d have:

// we'll represent our top-level ADT as an abstract class; this is the
//   type we'll work with in most client code.
abstract class Expr {
    // ADTs are "closed"; that is, the constructors specified in the
    //   type definition are all we'll ever have: we'll implement this in
    //   C# by building sealed inner classes with access to a private
    //   constructor
    private Expr() { }

    // every function we'd implement by pattern-matching for our ADT
    //   will be an abstract method on the equivalent type
    public abstract int Eval();

    public sealed class Literal : Expr {
        public int val;
        // subclasses implement the specific evaluation logic; this is
        //   equivalent to the per-pattern definitions in the ADT version
        public override int Eval() => val;
    }

    public sealed class Add : Expr {
        public Expr e1;
        public Expr e2;
        public override int Eval() => e1.Eval() + e2.Eval();
    }

    public sealed class Sub : Expr {
        public Expr e1;
        public Expr e2;
        public override int Eval() => e1.Eval() - e2.Eval();
    }

    public sealed class Mul : Expr {
        public Expr e1;
        public Expr e2;
        public override int Eval() => e1.Eval() * e2.Eval();
    }

    public sealed class Div : Expr {
        public Expr e1;
        public Expr e2;
        public override int Eval() => e1.Eval() / e2.Eval();
    }
}

// we can use our type like so:
class ExprDemo {
    static void Main()
    {
        var e = new Expr.Add {
            e1 = new Expr.Literal { val = 7 },
            e2 = new Expr.Mul {
                e1 = new Expr.Literal { val = 3 },
                e2 = new Expr.Literal { val = 5 }
            }
        };

        // prints "e.Eval() = 22"
        System.Console.WriteLine("e.Eval() = {0}", e.Eval());
    }
}

Suppose we extend our little “language” to include not just integer values and integer arithmetic, but an equality test (produing a boolean value) and a conditional (if-then-else) operation. Back to Haskell!

data Expr =
    Literal Int
  | Add Expr Expr
  | Sub Expr Expr
  | Mul Expr Expr
  | Div Expr Expr
  | Eql Expr Expr
  | IfThenElse Expr Expr Expr

The types for the interpreter aren’t entirely obvious; the Eql operation should compare two expressions which produce the same type (either an integer or a boolean) for equality, while the IfThenElse operation requires one expression which definitely evaluates to a boolean (the condition) and two others of matching type (the if-branch result and the else-branch result).

One possibility is to do the check and produce either a meaningful result of appropriate type, or an error value. Like so:

data ExprResult =
    IntResult Int
  | BoolResult Bool
  deriving Show

data ExprTy = IntTy | BoolTy deriving Show
data TypeError = TypeError { expected :: ExprTy , got :: ExprTy }
  deriving Show

eval :: Expr -> Either TypeError ExprResult

eval (Literal n) = Right (IntResult n)

eval (Add e1 e2) = do
  x <- eval e1
  y <- eval e2
  case (x, y) of
    (IntResult x, IntResult y) -> Right $ IntResult (x + y)
    (BoolResult _, _) -> Left $ TypeError IntTy BoolTy
    (_, BoolResult _) -> Left $ TypeError IntTy BoolTy

eval (Sub e1 e2) = do
  x <- eval e1
  y <- eval e2
  case (x, y) of
    (IntResult x, IntResult y) -> Right $ IntResult (x - y)
    (BoolResult _, _) -> Left $ TypeError IntTy BoolTy
    (_, BoolResult _) -> Left $ TypeError IntTy BoolTy

eval (Mul e1 e2) = do
  x <- eval e1
  y <- eval e2
  case (x, y) of
    (IntResult x, IntResult y) -> Right $ IntResult (x * y)
    (BoolResult _, _) -> Left $ TypeError IntTy BoolTy
    (_, BoolResult _) -> Left $ TypeError IntTy BoolTy

eval (Div e1 e2) = do
  x <- eval e1
  y <- eval e2
  case (x, y) of
    (IntResult x, IntResult y) -> Right $ IntResult (x `div` y)
    (BoolResult _, _) -> Left $ TypeError IntTy BoolTy
    (_, BoolResult _) -> Left $ TypeError IntTy BoolTy

eval (Eql e1 e2) = do
  x <- eval e1
  y <- eval e2
  case (x, y) of
    (IntResult x, IntResult y) -> Right $ BoolResult (x == y)
    (BoolResult x, BoolResult y) -> Right $ BoolResult (x == y)
    (IntResult _, _) -> Left $ TypeError IntTy BoolTy
    (BoolResult _, _) -> Left $ TypeError BoolTy IntTy 

eval (IfThenElse cond eIf eElse) = do
  c <- eval cond
  x <- eval eIf
  y <- eval eElse
  case (c, x, y) of
    (BoolResult c, IntResult x, IntResult y) ->
      Right $ IntResult $ if c then x else y
    (BoolResult c, BoolResult x, BoolResult y) ->
      Right $ BoolResult $ if c then x else y
    (IntResult _, _, _) -> 
      Left $ TypeError BoolTy IntTy
    (_, IntResult _, BoolResult _) -> 
      Left $ TypeError IntTy BoolTy
    (_, BoolResult _, IntResult _) -> 
      Left $ TypeError BoolTy IntTy

We can then evaluate both valid and invalid expressions, and verify that the “typechecker” does its job:

eval $ IfThenElse (Eql (Mul (Literal 3) (Literal 7)) (Literal 21))
                  (Literal 1)
                  (Literal 0)
=> Right (IntResult 1)

eval $ IfThenElse (Eql (Mul (Literal 3) (Literal 7)) (Literal 21))
                  (Eql (Literal 1) (Literal 1))
                  (Literal 0)
=> Left (TypeError {expected = BoolTy, got = IntTy})

Don’t worry, the point isn’t to go into Haskell’s monadic error handling or do syntax. Let’s just observe that our evaluator does work, correctly resolving an integer result from the first conditional, and pointing out that the second conditional provides an “if” branch of yielding a boolean but an “else” branch yielding an integer (that’s the Left (TypeError ..)).

However, it was extraordinarily tedious: we had to write out each possible combination of valid and invalid subexpressions for each evaluation rule. What if we could instead ensure that only valid expressions could be constructed?

It turns out that we can, using an extension to ADTs known as generalized algebraic data types, or GADTs. GADTs give us the ability to refine the types of our values in each constructor: this permits us to enforce our type safety rules directly in the host language (Haskell) type system, and forbid invalid expressions from even being constructed.

As a consequence, our evaluator is back to almost its original simplicity! It no longer has to worry about detecting type errors. Observe:

{-# LANGUAGE GADTs #-}

data Expr a where
  Literal :: Int -> Expr Int
  Add :: Expr Int -> Expr Int -> Expr Int
  Sub :: Expr Int -> Expr Int -> Expr Int
  Mul :: Expr Int -> Expr Int -> Expr Int
  Div :: Expr Int -> Expr Int -> Expr Int
  Eql :: Eq a => Expr a -> Expr a -> Expr Bool
  IfThenElse :: Expr Bool -> Expr a -> Expr a -> Expr a

eval :: Expr a -> a
eval (Literal n) = n
eval (Add e1 e2) = eval e1 + eval e2
eval (Sub e1 e2) = eval e1 - eval e2
eval (Mul e1 e2) = eval e1 * eval e2
eval (Div e1 e2) = eval e1 `div` eval e2
eval (Eql e1 e2) = eval e1 == eval e2
eval (IfThenElse cond eIf eElse) = if eval cond then eval eIf else eval eElse

We can still construct and evaluate valid expressions, but when we try to construct our “bad example”:

let badEx = IfThenElse (Eql (Mul (Literal 3) (Literal 7)) (Literal 21))
                       (Eql (Literal 1) (Literal 1))
                       (Literal 0)

=>

error:
  * Couldn't match type `Int' with `Bool'
    Expected type: Expr Bool
      Actual type: Expr Int
  * In the third argument of `IfThenElse', namely `(Literal 0)'

This is really pretty fantastic! We’ve been able to express our typing rules very directly, have them enforced by our host language, and keep the evaluator simple.

Can we get this kind of power in our object-oriented languages? Today’s paper of the day provides an answer: yes, with some caveats, if you have generics (that is, parametric polymorphism of the kind provided by C# or Java).

Kennedy and Russo show a translation for GADTs and many GADT-manipulating programs into the type system of C#. Along the way they encounter some rough spots which require the introduction of uncheckable type casts, and suggest some language improvements. C# programmers may notice that the switch enhancement they suggest is similar to the type-based switch that was introduced to the language recently; however, the version suggested by Kennedy and Russo is strictly more powerful, as their switch makes use of the type-refinement provided by GADTs to let the compiler “know more” about the relevant types in each arm of the switch.

At the end, they provide typing judgments and evaluation rules for their proposed language extensions; this part gets a bit formal, and given the language evolution since 2015 it’s more of a glimpse into a future that might have been. Nonetheless, I’d encourage any object-oriented programmers (by choice or circumstance) with an interest in more “typeful” data modeling to check out the paper.

We’ll try to keep tomorrow’s paper a little lighter and the write-up a little briefer! This one took a bit of justification, as ADTs and GADTs are quite unfamiliar outside of functional programming circles.