Simple Expression Interpreters

Let’s start our investigation with an interpreter for a simple language of calculations involving + and - over numbers. We’ll use this first discussion to define an interpreter that calculates a value from such expressions. The language is basic, but we can start discussing important concepts of abstract and concrete syntax, abstract syntax trees, parsing, interpretation and testing. Pay less attention to the language than to the underlying methodology and concepts used to define an interpreter.

Concrete Syntax

Concrete Syntax is the textual language written by programmers as input to compilers and interpreters. When you think of a programming language, you think first of its concrete syntax. The block structure of C, s-expressions defining Lisp, and the functional syntax of Haskell are examples of concrete syntax that immediately associates with a particular language.

Concrete syntax is always described by a grammar consisting of an alphabet and a collection of grammar rules. As discussed in the introduction, the alphabet defines basic symbols or tokens in the concrete syntax while grammar rules define how those tokens are sequenced defining elements of the language. A term is any text string defined by the grammar. Similarly, a language is the smallest set of terms that satisfy a set of grammar rules. It is useful to think of a language as a set and a grammar as a specifier for that set. Using traditional set comprehension we can define a language, $L$, as:

where $G$ is a predicate that is true when $s$ satisfies $L$’s grammar rules.

Let’s define the concrete syntax for our first language that we will call AE for Arithmetic Expressions. Terms in AE are defined by the following grammar:

Hopefully this is familiar. Terms, $t$, in AE are either numbers or sums and differences nested arbitrarily.

The language AE is the set of all strings that can be created with the grammar. The strings:

3
1+5
3+5-1

are all terms in AE. While the strings:

A
1*5
A+B-C

are not terms in AE.

Let’s also define values in AE as numbers:

The set of values is a subset of the set of terms and represents terms that result from interpretation. The set of values define what we should get when we run an interpreter. We will define this more formally later, but for now remember that $v$ is an interpretation result.

If we define the predicate $ae(t)$ to be true when $t$ satisfies AE’s grammar rules, then the language can be defined as a set:

In AE we can express three things: (i) a number; (ii) adding two terms; and (iii) subtracting two terms. Not the most useful of languages, but we have to start somewhere.

This discussion is hopefully review of your formal language theory or theory of computing studies. If it isn’t, I suggest stopping now and studying some formal language theory. In addition to being foundational, it is beautiful and useful.

Inference Rules and Axioms

Knowing what AE looks like, let’s now define how terms in AE are interpreted. Before writing a Haskell interpreter, we should define formally the meaning of terms. We will use inference rules for this purpose. $\eval$ is the evaluation relation and $x \eval y$ is read x evaluates to y. As the name implies the relation states that evaluating $x$ results in $y$.

Our first inference rule tells us how to interpret numbers buy defining $\eval$ for $v$:

The $NumE$ rule says evaluating numeral syntax in gives us the corresponding number. Remember that $v$ is a number and what we’re saying is interpreting a constant number value gives back the constant number value. Note that when an ambiguity exists between syntax and terms used to define meaning, the underscore notation indicates syntax. For example, $\underline{v}$ is number syntax while $v$ is number value.

Addition and subtraction are more interesting and hint at how all our interpreters will be structured. The rule, $PlusE$ defines the interpretation of terms of the form $t_1+t_2$:

$PlusE$’s antecedents and consequent work together to define a recursive interpreter. The first antecedent states that $t_1 \eval v_1$ must be true before the consequent can be true. But $v_1$ is a variable whose value is the result of evaluating $t_1$. In effect, this antecedent says that $v_1$ must be the result of that evaluation. The second antecedent behaves similarly for $t_2$ and $v_2$. Both antecedents name the results of interpreting $t_1$ and $t_2$ as $v_1$ and $v_2$ respectively.

Now that we know the results of evaluating $t_1$ and $t_2$, defining their sum is simple. Because values in AE are numbers we use Haskell’s notion of addition to define the sum. Thus, the consequent is $t_1 \underline{+} t_2 \eval v_1 + v_2$.

We define subtraction similarly in the $MinusE$ rule:

Using this rule $2\underline{-}1$ evaluates to $1$ as it should. However, $1\underline{-}2$ evaluates to $-1$. As $\NUM$ values are defined to be non-negative, this is a problem. It’s easy enough to fix the $MinusE$ rule to only generate positive values:

The new rule $MinusE+$ adds a third antecedent that specifies $v_1$ must be greater than or equal to $v_2$ The $MinusE+$ applies when: $v_1\geq v_2$ thus $v_1 - v_2$ will always be non-negative as required.

What does happen when $v_2 > v_1$? The new $MinusE+$ does not apply nor does any other evaluation rule. Subtraction when $v_2 > v_1$ is undefined. There is no rule that applies and thus no evaluation results. When evaluation is not complete in this way and the term being evaluated is not a value, we say that interpretation is stuck and the evaluation relation defined by $\eval$ is not total.

One way to fix this problem is to return $0$ when the result would be negative. This fix is captured with the rule $MinusEZero$:

Evaluation is now total, but subtraction in $AE$ has properties that might prove problematic. $0$ could be a legitimate subtraction result or it could indicate a problem. We call these designated values “magic values” and they prove problematic. An alternative is returning an error value:

This introduces a new value, $\bot$, called bottom that represents an error value. As a result, $\bot$ must be included in all other inference rules. What is $5+\bot$? Simply defining the result of any expression involving $\bot$ as $\bot$ requires new rules for each operator.

Often the best approach is to leave the relation as is and wait until implementation time to deal with errors. For now, this is the approach we will take.

Understanding the structure of these rules before moving forward is vital. They both define antecedents that name the results of other calculations. More specifically, other recursive calculations. When writing and defining interpreters, recursion is your best friend. We needn’t think now about calculating the values of $t_1$ and $t_2$, only that their values are calculated the same way all other values are calculated.

Abstract Syntax

Now we have both a concrete syntax and an evaluation semantics for AE defined using mathematical techniques. We need to transform both definitions into Haskell structures to build our first interpreter for AE. To do this, we will first define an abstract syntax for AE.

Concrete syntax is nice on the user side, but painful to work with directly when writing interpreters and compilers. If you want to try an experiment, write a Haskell program that will interpret the AE language directly. It can be done, but making changes or extending the language is laborious and potentially painful.

Abstract Syntax is a data structure representing parsed terms. This data structure is far more useful than concrete syntax when writing interpreters and compilers. Programs are data and abstract syntax is the data structure that represents them. An abstract syntax for AE written using a Haskell data type is:

data AE where
  Num :: Int -> AE
  Plus :: AE -> AE -> AE
  Minus :: AE -> AE -> AE
  deriving (Show,Eq)

where Num, Plus and Minus are the constructors of the data type AE that correspond with numbers, sums and differences in the AE concrete syntax. We use the term constructor because all values of type AE are constructed with one of these operations. By definition, the AE type contains all constructions using Plus, Minus and Num, and no more.

All terms in AE have associated data structures in the abstract syntax. For example (Num 1) is the abstract syntax for 1. (Plus (Num 1) (Num 3)) is the abstract syntax for 1+3. (Minus (Plus (Num 3 (Num 5)) (Num 1)) is the abstract syntax for 3+5-1. For the abstract syntax to be effective, every term in the concrete syntax must have an associated term in the abstract syntax. Remember the properties of relations you learned in your discrete math class? They come in handy right now. The relationship between concrete syntax and associated abstract syntax should be a total function. Concrete syntax terms should have exactly one abstract syntax value and all concrete syntax terms should be associated with an abstract syntax value. Always remember that errors are outputs.

From this point forward I will use the TLA¹ AST when referring to abstract syntax data structures. AST stands for abstract syntax tree. Haskell data types naturally form trees and trees are perfect representations for abstract syntax. I’ll come back to this later, but for now remember that AST, abstract syntax, and abstract syntax tree refer to the same Haskell data type.

Parsers and Pretty Printers

A parser is a program that translates concrete syntax into an AST. It checks the syntax of its input, generates error messages if the syntax is bad, and generates an AST if the syntax is good. The signature of a parser for the AE language is:

parseAE :: String -> AE

Give parseAE a string and it will return an AE if it does not throw an error. A parser’s signature for any language will be a string to the datatype for that language’s abstract syntax.

A pretty printer is the inverse of a parser. It translates an AE data structure into a string representing the concrete syntax. The signature of a pretty printer for the AE language is:

pprintAE :: AE -> String

Give pprintAE an AE data structure and it will return a string. The pretty printer’s signature for any language will be the datatype for that language’s abstract syntax to a string.

If parseAE and pprintAE are correct, then the following equivalence should hold for any string representing legal concrete syntax:

pprintAE (parseAE s) == s

If we parse a string and pretty print the result, we back the string. A useful relationship for testing these tools.

This course is not about building parsers and pretty printers. This task is largely automated, Haskell provides tools for building parsers, and parser generators are widely available for other languages. I will provide examples using Parsec, a monadic parser combinator tool for writing and composing parsers. After some setup, Parsec is not difficult to extend to the languages we would like to discuss. For more details there are a number of online tutorials and chapters in major Haskell texts. For now, let’s assume we have the parseAE and pprintAE functions available.

Evaluator

An evaluator converts an abstract syntax term into a value. As noted earlier, values represent valid interpretation results. If an evaluator produces anything besides a value, something went wrong. Either the input is invalid, the evaluator is written wrong, or the language definition is problematic. We’ll talk more about these issues later. For now, let’s look at an evaluator where everything works as it should.

How should the evaluator be constructed? The data type defined for the abstract syntax gives us a big clue. If the constructors from the data type define every possible AST element, then defining an evaluator for each element of the data type should do the trick. We need to define how the interpreter behaves on each constructor from the AE datatype.

First, let’s get the eval signature down. Our evaluator will take an element of AE and produce a value, where a value is defined as a number. In the AST, numbers are of the form (Num n) where n is a Haskell Int. Unfortunately, we can’t capture value-ness in our signature, so we’ll say that eval returns Maybe AE. We’ll use Maybe to allow eval to return a value or an error. The signature for eval is:

eval :: AE -> Maybe AE

We now define eval’s cases, one for each AE constructor starting with the Num constructor. (Num 3), for example, represents a constant 3 in the AE abstract syntax. Without much thought it should be clear that as a constant, (Num 3) evaluates to (Num 3). Numbers are values in AE, thus they should not be evaluated further making this consistent with our formal definition. Thankfully, this is exactly what our inference rule for evaluating numbers says if we remember that $v$ represents $\NUM$:

The value associated with an AE number is the Haskell equivalent. Thus, the eval case for (Num n) just returns its argument:

(Num n) = return (Num n)

Because return = Just, eval (Num 3) returns (Just (Num 3))

We now have an evaluator for literal numbers, but nothing more.

The next constructor, Plus, represents a more interesting case. We have a rule named $PlusE$ that defines evaluation of t1+t2:

The inference rule is defined in terms of concrete rather than abstract syntax, so we have to do a bit of translation work. $t_1\underline{+}t_2$ translates quickly into (Plus t1 t2). If t1 evaluates to (Num v1) and t2 evaluates to (Num v2) then (Plus t1 t2) evaluates to (Num v1)+(Num v2). There is no + operation in Haskell for (Num n) constructions, this we need to write one to define addition in AE. We can define addition in AE in terms of addition in Haskell. Specifically:

(Num n) + (Num m) == (Num n+m)

There are many ways to construct this operation in Haskell. Let’s use a lifting function that will allow us to define any operation in AE using an operation from Haskell:

liftNum :: (Int -> Int -> Int) -> AE -> AE -> AE
liftNum f (Num l) (Num r) = (Num (f l r))

liftNum takes a binary function over integers and two Num constructions. It lifts the binary operation into Num by extracting the Int values, applying the operation, and putting the result back in Num. While we could not use + on Num constructions directly, we can use liftNum to define addition in AE:

(Num n) + (Num m) == (liftNum (+) n m)

We can define other AE operations similarly.

Now we have everything needed to define Plus. This inference rule can be almost directly translated into Haskell using do to evaluate antecedents, calculate the and return the value defined by the consequent:

(Plus t1 t2) = do v1 <- eval t1
                  v2 <- eval t2
                  return (liftNum (+) v1 v2)

While the lifting function is pretty cool, there is a potentially better way. We can use Haskell’s pattern matching capability to extract good values and filter out bad values. Consider this use of the do notation:

(Plus t1 t2) = do (Num v1) <- eval t1
                  (Num v2) <- eval t2
                  return (Num v1+v2)

It turns out that the <- notation is not a simple assignment operator. eval t1 and eval t2 behave as they always have returning values of type AE. However, the notation (Num v1) <- eval t1 causes the result from eval t1 to be matched with (Num v1). v1 is a variable, but Num is a constructor. If eval t1 returns a value (Num 3) pattern matching succeeds and v1 is bound to 3. If a match fails, the result is an error and the monadic value Nothing gets returned.

The translation from inference rule to Haskell follows standard rule of thumb. The do bindings manage the rule antecedents, performing evaluation and binding variables. The return is the consequent and evaluates the term. While only a rule-of-thumb, it will prove useful.

Finally, The Minus constructor case is identical to the Plus constructor case except values are subtracted rather than added together. For completeness, here is the subtraction case:

(Minus t1 t2) = do (Num v1) <- eval t1
                   (Num v2) <- eval t2
                   return (Num v1-v2)

Putting the cases together in the following evaluator for AE that reduces every abstract syntax term to a value:

eval :: AE -> Maybe AE
eval (Num x) = return (Num x)
eval (Plus t1 t2) = do (Num v1) <- (eval t1)
                       (Num v2) <- (eval t2)
                       return (Num v1+v2)
eval (Minus t1 t2) = do (Num v1) <- (eval t1)
                        (Num v2) <- (eval t2)
                        return (Num v1-v2)

The evaluator follows a pattern that every evaluator we write will follow. Each constructor from the AST definition has a case in the eval function that evaluates that constructor. This pattern and the accompanying data construct gives us three nice language properties - completeness, determinicity, and normalization

Completeness says that every term constructed in AE will be evaluated by eval. Can we prove that? The Haskell data construct gives us exceptionally nice properties for free, without direct proof. By definition, every value in the abstract syntax for AE is constructed with Num, Plus, and Minus . There are no other AE values. This is true of any type defined using data in Haskell. All values of the type are constructed with its constructors.

We know AE is complete because there is one inference rule for every syntax construct and one case in eval for each inference rule. The eval function has one case for each constructor from AE. Because all AE values are built with those constructors, there is a case for every AE value in the eval function. While not a proof, this gives strong evidence that our language definition is complete.

Determinicity says that if we call eval on any term, we will get the same result. This is an exceptionally important property as we do bit want the same call to eval resulting in different values. We know AE is deterministic because there is one inference rule for interpreting each element of the concrete syntax. In turn we know that eval is deterministic because there is precisely one case in the definition for each AE constructor. Given (Num n) there is one rule and one eval case. Given Plus there is one rule and one eval case.

Normalization says that a call to eval on any term constructed in AE will terminate. Again, a pretty bold statement. Can we prove it? The elements of a Haskell data type specifically and algebraic types generally have are well-ordered. In mathematics, well-ordered means that every subset of a set has a least element. Getting from well-ordered to guaranteed termination takes a bit of work, but the gist is that components of a constructor are smaller than the constructor itself. Each recursive call on the parts of a term is made on a smaller term. Consider eval (Plus t1 t2) where t1 and t2 can be viewed as smaller than (Plus t1 t2). Because every set of AE terms has a least element, pulling a term apart into its pieces will eventually get to that least element.

The least elements of AE are those constructed by (Num n). When the evaluator reaches the least element, it cannot go further and terminates. Every call to eval gets closer to the least element. Note that those least elements are what we defined as values. This is not a coincidence. Not only does AE terminate, it always terminates with a value. Said in terms we all understand, the AE evaluator never crashes for any element of AE.

All Together Now

Before we say more about AE, let’s put all the pieces together into a single definition. Definition of AE is now complete syntactically, semantically and operationally:

• Syntax is defined by the AE grammar
• Semantics is defined by the AE inference rules
• Operations are defined by eval and parse.

First we defined a concrete syntax for terms:

and syntactic definition of values:

Then we defined basic inference rules formally defining how AE is interpreted:

We implemented a parser from the grammar and an evaluator from the inference rules:

eval :: AE -> Maybe AE
eval (Num x) = return (Num x)
eval (Plus t1 t2) = do (Num v1) <- (eval t1)
                       (Num v2) <- (eval t2)
                       return (Num v1+v2)
eval (Minus t1 t2) = do (Num v1) <- (eval t1)
                        (Num v2) <- (eval t2)
                        return (Num v1-v2)

Given the parser and evaluator for AE, we can now define a language interpreter, interp, that puts everything together:

interp :: String -> Maybe AE
interp = eval . parseAE

In words, interp is the composition of parseAE and eval. This notation uses Haskell’s function composition to define that parse will be called first and the output passed to eval. If parseAE throws an error, interp will terminate without passing a value to eval.

If you are unfamiliar with the point-free style and the use of function composition, interp can be defined in a more traditional manner as:

interp x = eval (parseAE x)

Use the notation you are comfortable with. There is no advantage to either, but function composition more closely resembles the mathematics of interpreter construction.

Discussion

AE is a silly language that is less powerful than one of those bank calculators you get when you open a checking account. It adds and subtracts numbers. However, we need to start somewhere and AE is good for that.

Completeness, Determinicity, and Normalizing

We said earlier that eval is complete, deterministic and normalizing. Complete in that any element of AE can be interpreted, deterministic in that there is one way to interpret any element of AE, and normalizing in that every interpretation of and AE element terminates.

Unfortunately, these nice properties result from AE being a trivial language. Completeness and deterministic are properties we will seek to preserve as we add features. However, normalizing will prove problematic when we add recursion and looping.

Correctness

Another important question, one might say the most important question is whether eval is correct. How do we define correctness? We have the evaluation relation, $t\eval v$ that relates terms to values and we have eval :: AE -> AE that is a function from terms to values. The simplest correctness definition is:

This states that evaluating any $t$ results in a value that is related to $t$ by the evaluation relation, $t\eval v$. By this definition, is our interpreter correct? How would you go about proving this condition?

Induction and Extensionality

There is one property of AE structures that underlies our discussion. The AE abstract syntax and algebraic types have both inductive and extensionality principles. The inductive principle allows us to prove properties over AE and the extensionality principle allows us to determine if two AE structures are equivalent. We won’t use either principle yet, so let’s define them informally for now.

Induction over AE says that some property, $p$, is true for all elements of AE if we can:

1. Prove $p$ directly for base cases
2. Prove $p$ for inductive cases by assuming $p$ for the case’s pieces

What are the base and inductive cases? For AE, Num is the base case while Plus and Minus are inductive cases. Num is a base case because it is not constructed from other elements of AE. We can see this in the data definition. It is also reflected in the definition of eval where there is no recursive call for Num. Plus and Minus both depend on other AE constructions in their definition and eval cases. Stated in terms of the AE concrete syntax, the induction principle states that $p$ is true for any AE term $t$ when:

Extensionality is simpler to state. Two terms in AE are equivalent if they use the same constructor and their parts are equivalent. For any $t$ and $t’$, $t=t’$ if one of the following cases applies:

Thus if no case applies, then the terms are not equal. So, $t_1+t_2$ will never be equal to $t_1’-t_2’$.

Definitions

Lots of definitions to get us started:

• Concrete Syntax - The textual form of a language used by programmers to write code
• Abstract Syntax - The data structure representation of a language used by tools
• Parser - Translates from concrete syntax to abstract syntax
• Evaluation - Converts abstract syntax into a value.
• Value - A good result from evaluation
• Interpreter - Any program that translates syntax from one form into another
• Algebraic Type - Uses sums and products to define types. Haskell’s data system defines algebraic types
• Termination - Halting
• Deterministic - Every invocation with the same inputs generates the same outputs
• Normalization - Every invocation halts
• Induction - Proof principle commonly used for countably infinite structures
• Extensionality - Proof principle used to show two structures are equal.

Exercises

1. Add multiplication and division to AE. Do we lose any of our nice properties by doing this?
2. Rewrite the eval function to return a Haskell Int rather than an AE value. This is an alternative to returning the Haskell datatype.
3. Rewrite AE replacing the Plus and Minus constructors in the AST with a single constructor Binop op t1 t2 where op is the represented binary operation. You will need to change the parser to generate Binop rather than Plus and Minus. Think carefully about what op should be. If you do it right, you should be able to add any operator to AE by simply changing the parser.

Source

• Download source for all interpreter code from this chapter.
• Download source for the parser utilities used by the interpreters.

Notes

Documentation for the Parsec Expression Parser