Arithmetic expression interpreter

Specification

An arithmetic expression is one of the following:

- An integer constant.
- The sum of two arithmetic expressions.
- The product of two arithmetic expressions.
- The difference of two arithmetic expressions.

Evaluating an arithmetic expression requires the following steps:

- If the expression is a constant, return the constant.
- If the expression is an addition, evaluate the two subexpressions and then return the sum of their results.
- If the expression is a multiplication, evaluate the two subexpressions and then return the product of their results.
- 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:

- 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.
- 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.
- There are no nullable references. The code is immune to that class of bugs.
- 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.
- 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).