io7m | single-page | multi-page | archive (zip, signature)
5. The Type ZooA Crash Course In Algebraic Types
PreviousUp

Arithmetic expression interpreter
Specification
An arithmetic expression is one of the following:
  1. An integer constant.
  2. The sum of two arithmetic expressions.
  3. The product of two arithmetic expressions.
  4. The difference of two arithmetic expressions.
Evaluating an arithmetic expression requires the following steps:
  1. If the expression is a constant, return the constant.
  2. If the expression is an addition, evaluate the two subexpressions and then return the sum of their results.
  3. If the expression is a multiplication, evaluate the two subexpressions and then return the product of their results.
  4. If the expression is a subtraction, evaluate the two subexpressions and then return the difference of their results.
Implementation
First, it's possible to produce an almost line-for-line copy of the specification as a type:
module Expression where

data Expression
  = Constant       Integer
  | Addition       Expression Expression
  | Multiplication Expression Expression
  | Subtraction    Expression Expression
  deriving Show

The definition of the evaluation function is similarly trivial, and matches the textual specification:
module Interpreter where

import Expression

run :: Expression -> Integer
run (Constant       x)     = x
run (Addition       e0 e1) = (run e0) + (run e1)
run (Multiplication e0 e1) = (run e0) * (run e1)
run (Subtraction    e0 e1) = (run e0) - (run e1)

The run function is an example of an equational definition. The definition is the same as using a case expression in the body of the function, but more syntactically compact.
It's possible to evaluate expressions from the ghci interpreter for some assurance that the function really is correct:
ghci> import Interpreter

ghci> run (Constant 23)
23
ghci> run (Addition (Constant 23) (Constant 17))
40
ghci> run (Multiplication (Constant 23) (Constant 17))
391
The code has a large number of advantages over the original Java code:
  1. The compiler can statically guarantee that all expression types are handled: It knows exactly what forms an expression can take and will not let the programmer fail to handle them.
  2. Each type of expression can be uniquely distinguished simply by pattern matching: The type of the expression is represented by the constructor used to create it. There is no manual bookkeeping required on the part of the programmer.
  3. There are no nullable references. The code is immune to that class of bugs.
  4. The declarations are compact and follow the definitions given in the textual specification directly. There is a high degree of confidence that the program implements the specification as written, and implements it without surprises.
  5. The evaluation function is written using only structural recursion. This means that it operates on structures of decreasing size as it progresses: This gives a usable proof that the function terminates (which is essential when the code is subject to formal verification).

PreviousUp
5. The Type ZooA Crash Course In Algebraic Types