Haskell

This is not a Haskell text. I will cover some things in Haskell you might not be aware of, but I make no claims about writing big, beautiful Haskell. Monads, GADTs, and point-free style come to mind quickly as important concepts that we’ll use. However, don’t read this book to learn Haskell. There are much better sources both online and as traditional books:

• Learn you a Haskell for Great Good
• Haskell Book

Data Types and Recursion

Understanding Haskell data types and recursion is critical to understanding how interpreters work. Recursion is your friend and will serve you well. When we define a simple data type like this example for lists:

data IntList where
  Null :: IntList
  Cons :: Int -> IntList -> IntList 

IntList is the new data type and Null and Cons are constructors for that type. All values of IntList are constructed with Null and Cons. The constructs:

Null
Cons 1 Null
Cons 1 (Cons 2 Null)

all define values of type IntList.

We also get a recursive framework for processing values from the new type. If we want to write a size function for IntList we define size over every IntList constructor:

size :: IntList -> Int
size Null = 0
size Cons x xs = size xs + 1

Null is the base case and Cons the recursive case for this definition. We an similarly define a function that sums the values in IntList:

sum :: IntList -> Int
sum Null = 0
sum Cons x xs = x _ (sum xs)

The structure of IntList allows us to build any such function using the same approach. In fact, any type created with data is such that a recursive function can be written using this pattern to process any such structure. This is a powerful principle we will use repeatedly throughout this text.

The do Notation

Haskell’s do notation is a commonly used abstraction allowing sequential execution of monadic code. If you are at all familiar with Haskell, you’ve likely seen this notation at work. I suspect you’ve also tried hard to avoid the details of monadic computation and are reconsidering reading this text now that the monad has entered the conversation.

Fear not. We will use the monadic do notation to order computations in parsers and test procedures. Early in the text we won’t need to understand the details of monadic computation. We’ll ease into monads and applicative functors later on after we have a better handle on how interpreters are written.

For now, here’s what you need to know. In the following do example, three operations are performed in sequence. f x is called first and the result bound to identifier a. g x is called next, and again the result bound to identifier b. Finally, a + b is calculated and returned as the result of the computation:

do {
	a <- f x;
	b <- g y;
	return (a + b)
}

The trick is that f and g must be monadic. You can’t do this with arbitrary functions. The thing you get back is also monadic and not a simple value. The benefit is the same do notation works for any monad. Just choose a monad to encapsulate your computations and you get the do notation for free.

Let’s see how this works with the Maybe monad with a very simple example. Define two functions that return Maybe types:

f x = if x > 3 then Just x else Nothing
g x = if x < 4 then Nothing else Just x

These two functions are rather arbitrary, but both take integers and return Maybe Int based on their input with respect to a constant value. There is nothing to see here other than both return Maybe types.

Now a simple function test that uses do to sequence calculations:

test1 = do {
  a <- f 4 ;
  b <- g a ;
  return (a + b)
  }
test1
== Just 8

You can see the sequential calculation. a is calculated first and b calculated from a. Both a and b determine the return value. Simple sequential execution.

But there’s more!

If either the a or b calculation results in Nothing, the sequence of calculations returns Nothing:

test2 = do {
  a <- f 2 ;
  b <- g a ;
  return (a + b)
  }
test2
== Nothing

All the handing of Nothing normally done with case statements is handled underneath the hood by the bind. No need to check things in the calculation of b or the function g.

Finally, all functions are written over Int and not Maybe. g’s argument is an Int and + takes two Ints. The do notation handles Just and in the <- sequence. f returns Just 4 in the first example, but a gets bound to 4. This is a wonderfully powerful feature that we’ll discuss later. For now, these examples show how the do notation sequences calculations and binds values to identifiers - a topic we’ll dive into shortly.

One plea before moving on. Don’t avoid monads. They are truly beautiful computation structures that support a powerful, new abstraction for computing. Spend some time with them and write your own. The experience will serve you well!

Notations

Several standard notations are used throughout for various kinds of things we need to discuss. Mathematics, Haskell and Expressions are used to represent formal definitions, implementation code, and source language code respecitively. We also need a meta-language for describing our languages and their meanings.

Math

Throughout this document mathematical statements are formatted using embedded $\LaTeX$ using Mathjax:

Haskell

Similarly, Haskell code is formatted using the traditional Haskell style:

data AE = Num Int
	    | Plus AE AE
	    | Minus AE AE
	      deriving (Show,Eq)

Expressions

Concrete syntax for the various languages we develop interpreters for is formatted much like Haskell, but without syntax highlighting:

bind f = lambda x in x + 1 in
  app f 3

Meta Language

A meta-language is exactly what the name implies - the language above the language. It is used to define the various aspects of the languages we will study.

Grammars

Grammars are represented using ::= to define variables and | to express alternative. Any symbol in all caps is considered a variable. The following trivial grammar defines an expression languages consisting of sum and difference operations:

Any symbol to the left of the ::= definition symbol is a meta-variable defined by the definition to the right. The symbol $t$ represents anything defined by the expression to the right. Note also that any subscripted or superscripted $t$ such as $t_k$ or $t’$ is definitionally the same as $t$.

There are a few pre-defined meta-variables that include $\NUM$ for integer numbers and $\NAT$ for natural numbers. We’re not worried about writing parsers in this book, but specifying them proves useful.

Inference Rules

Inference rules define immediate consequences like the definition of $\wedge$-introduction:

This says that if we know $A$ and we know $B$, then we immediately know $A \wedge B$. More generally:

says if $A_0$ through $A_n$ are known to hold, then $C$ is known to hold. $A_k$ are called antecedents and $C$ is called a consequent.

An inference rule having no preconditions defines an axiom:

If nothing need be true to know $A$, then $A$ is always true.

Derivations

A derivation strings inference rules together by using the consequent of one or more rules as the antecedent of another. Consider the derivation of the symmetric property of conjunction can be derived as follows:

1. $A \wedge B \vdash B$ by $\wedge$-elim
2. $A \wedge B \vdash A$ by $\wedge$-elim
3. $B, A \vdash B \wedge A$ by $\wedge$-intro

When such a derivation exists, we can say the following:

This is read $A\wedge B$ derives $B\wedge A$. If a derivation has no precondition it defines a theorem. For example, the symmetric property of conjunction is expressed as:

Evaluation

Similarly, a multi-step evaluation strings together evaluation rules application. For example, a simple arithmetic expression evaluates in the following way:

1+3-4
== 4-4
== 0

1+3-4 evaluates in one step to 4-4 and again to 0. In this case each occurance of == represents the application of an evalion rule.

Code

Download source for do examples from this chapter.

Notes