Before moving ahead to functions, let’s spend a bit of time looking at type checking when adding Booleans to BAE. Let’s define a new language BAE with Booleans (
BBAE) that simply adds the same boolean operators added to
AE to get
ABE. Let’s quickly walk through our standard methodology for extending a language and add at the same time add type checking. We’ll treat this almost like an exercise with some quick commentary, but not a great deal of detail.
The first step is extending concrete syntax and adding new values if necessary. The concrete syntax for
BBAE is literally the concrete syntax of
Similarly, there are no new values that do not appear in
BAE. We simply compose the values from those to languages:
We now have a syntax for
BBAE to work from. On to the parser and pretty printer.
The abstract syntax of
BBAE follows immediately from its concrete syntax. One can simply copy-and-paste the elements of
BAE into a single AST resulting in:
A quick check (no pun intended) reveals that we have an abstract syntax element for each language element. One can literally walk through the concrete syntax and map constructs to their constructors.
The parser, pretty printer, and generator for
BBAE are simple extensions of
BAE. For brevity, we’ll move on without including them in the discussion. However, you’ll find code for all three in the
BBAE source files. Note that the
ABE generator must be modified to account for keeping track of generated identifiers. This is a simple addition, but easy to miss.
Like the syntax definition, the definition for eval composes rules from
BAE. Literally nothing changes:
How does this work? We’ve combined two languages with their own constructs by simply combining rules. How do they know about each other during interpretation? The trick is in the definition of
t and its associated abstract syntax. As long as we have a rule for every abstract syntax element, recursive calls to the interpreter take care of integrating the languages. Said differently, in virtually every rule we can interpret subterms of terms by simply calling the interpreter without regard to the specifics of the subterm. Recursion is your friend here.
The property that allows us to compose languages in this way is orthogonality. The valuation rules for one expression do not interact with other specific expressions. For example, while
isZero uses the value of its argument expression, that expression can be any properly formed language expression. Orthogonality is an important design principle that dramatically simplifies language design and implementation.
We now have a mathematical definition for the evaluation relation.
Now the implementation details for the evaluator. Here things are not quite as simple as composing previous interpreters. We’ll need to spend some time thinking through how we want our interpreters to behave before diving into the code.
What should the interpreter return? Previously we’ve implemented interpreters that return:
Eithererror messages or AST values
The plan is to eventually write a type checker for this language. AST values are sufficient for this
eval implementation because we hope to predict success before execution. Haskell values would be fine, but we want to use our earlier technique for implementing error messages. The
Either implementation was specifically for catching errors at runtime and that is not required for a type checking interpreter.
What about the environment?
Env remains unchanged from previous implementations because the environment remains a simple list of identifier/value pairs. Nothing changes other than the type stored in the environment changing to
This gives us the expected type signature for the
eval will accept an environment and abstract syntax term and produce an abstract syntax term.
Evaluation cases for each AST element are defined by evaluation rules and taken verbatim from the
BAE interpreters. Again, orthogonality helps us out. The resulting function looks like this:
eval uses the Haskell
error function rather than returning value. Given that we call a type checker before evaluating an expression, why do we need to do this? As it turns out, that
error instance will never be called. Type checking assures that all variables are bound and the “Variable not found” case will not occur. However, Haskell requires case statements to completely cover a type. The language has no way of determining the
Nothing case will not be called. We could have the code literally do anything in the
Nothing case, but we choose to generate an error knowing that something is horribly wrong if it is actually generated.
The interpretation final function that composes the interpreter and parser is identical to that for
BAE. Specifically, call the parser and evaluate the result with an initial, empty environment:
We now have an interpreter for
BBAE that requires testing. By defining
interp in the same manner as
BAE, the test function for
eval literally does not change:
With everything in place, we evaluate over just a few cases and quickly learn that
eval without any dynamic error checking or static type checking fails. Hopefully this is not surprising to you.
The next step is defining and implementing a type checker to statically determine if a
BBAE expression will execute.
Type rules for
ABE expressions remain unchanged in
BBAE. Numbers remain of type $\tnum$ and Booleans $\tbool$:
Unary and binary operations similarly remain the same:
The new concept in this language is identifiers introduced by
bind and used anywhere in expressions. How do we determine the type of identifiers? To get an idea, recall how
bind using an environment. when evaluating a
x takes the value
b. We use an environment to hold bindings of identifiers to values. Can we do the same thing with types of identifiers? Specifically, create a environment-like structure that maintains bindings of identifiers to types and simply look up type in that structure?
The environment-like structure that contains types will be called a context and is frequently represented by $\Gamma$. Like the environment, it is a list of pairs and behaves in exactly the same fashion. The difference is each pair consists of an identifier and type rather than identifier and value.
We will use the notation $(x,T)$ to represent the binding of a variable to some type and the Haskell list append $(x,T):\Gamma$ to represent addition of new binding to a context. Finally, $(x,T)\in\Gamma$ represents finding the first instance of $(x,T)$ in $\Gamma$.
The rule for
bind adds the newly bound identifier with its type to the context and finds the type of the
The type of the body becomes the type of the
bind. This makes sense as the body is what gets evaluated when the
bind is evaluated. It’s also interesting to think of
bind as a special expression that simply adds to the environment or context.
One more type rule for identifiers is needed to finish the definition. It simply looks up a type binding $(v,T)$ in $\Gamma$ and asserts that $v:T$ is true when the type binding is found:
This lookup is quite similar to the lookup used when the environment is used. In fact, functions for manipulating the environment and context are identical.
Now we implement the
typeof function. First the standard data type for the two types expressions defined for
Now we build out the type checker from the type checking rules. Like the
eval function earlier, virtually all type checking code comes from the
ABE type checkers.
typeof accepts a context and AST and returns either an error message or a type:
Note that we’re using the
Either construct to return the type or error. However, we’re not using
Either as a monad in this type inference function. The
typeof signature is eerily similar to the
eval signature. We’ll come back to that later, but it’s worth thinking about why that’s the case.
Here’s the complete code for the
There’s really nothing to see here. Our technique for defining languages and specifying their evaluation and type characteristics makes it simple to compose orthogonal language elements. Things will get harder as we add other constructs, but for now things are pretty easy.
Could it be that testing the
BBAE evaluator is as simple as composing the
BAE QuickCheck capabilities? Fortunately, it is. We simply need to generate arbitrary terms that include terms from both the
BAE language subsets.
As usual, we first make the
BBAE data type an instance of
Arbitrary and define the
arbitrary function. The use of
genBBAE is where the generator for
BBAE is integrated:
The hard work for the generator itself is already done. First, we’ll define generators for the numeric elements of
Now the elements that involve both numbers and booleans:
Finally, the elements that involve identifiers and their values:
Now we simply put everything together into a single generator:
What changes here from the previous generators is the list of generators passed to
oneof. Instead of choosing only expressions from the numeric expression or the boolean expressions, we now choose from both. For values, things work similarly choosing from both Boolean and numeric values.
Three things worth thinking about are happening in this chapter. First, we are going from beginning to end defining a new language. We started with syntax, defined evaluation and implemented an evaluation function, defined a type system and implemented a type checker, and concluded with QuickCheck functions for testing. This is the methodology we use for defining languages at work.
Second, we see how composition of orthogonal language constructs makes this reasonably simple. How many times in the chapter did we talk about composing elements of previous interpreters? Usually that was a simple cut-and-past operation. The only real exception being the arbitrary test case generator where we had to compose the language subsets.
Finally, we introduced the concept of a context that behaves like an environment for types. An interesting difference is the environment is a runtime construct while the context is used during static analysis. The reason is values cannot be known until runtime, but types are known statically. This is not true for all languages, but is true for our languages.
Remember these things moving forward. The step-by-step approach for defining a language and the composition of orthogonal language constructs are important design concepts. Context is something we will continue to use throughout our study.
evalErr :: Env -> BBAE -> Either String BBAEfor for
BBAEthat returns either a string error message or a value following interpretation.
evalErrfunction with the
evalTypefunction using the same techniques used for
errorfunction will never be called in
evalgiven that all expressions given to
evalsuccessfully type check.
Eitheras a monad.
Download source for all interpreter code from this chapter.