Chapter 10: An ML Implementation of Simple Types

 < Free Open Study > 



The concrete realization of λ as an ML program follows the same lines as our implementation of the untyped lambda-calculus in Chapter 7. The main addition is a function typeof for calculating the type of a given term in a given context. Before we get to it, though, we need a little low-level machinery for manipulating contexts.

10.1 Contexts

Recall from Chapter 7 (p. 85) that a context is just a list of pairs of variable names and bindings:

   type context = (string * binding) list 

In Chapter 7, we used contexts just for converting between named and nameless forms of terms during parsing and printing. For this, we needed to know just the names of the variables; the binding type was defined as a trivial one-constructor datatype carrying no information at all:

   type binding = NameBind 

To implement the typechecker, we will need to use the context to carry typing assumptions about variables. We support this by adding a new constructor called VarBind to the binding type:

   type binding =       NameBind     | VarBind of ty 

[1]

Each VarBind constructor carries a typing assumption for the corresponding variable. We keep the old NameBind constructor in addition to VarBind, for the convenience of the printing and parsing functions, which don't care about typing assumptions. (A different implementation strategy would be to define two completely different context typesone for parsing and printing and another for typechecking.)

The typeof function uses a function addbinding to extend a context ctx with a new variable binding (x,bind); since contexts are represented as lists, addbinding is essentially just cons:

   let addbinding ctx x bind = (x,bind)::ctx 

Conversely, we use the function getTypeFromContext to extract the typing assumption associated with a particular variable i in a context ctx (the file information fi is used for printing an error message if i is out of range):

   let getTypeFromContext fi ctx i =     match getbinding fi ctx i with         VarBind(tyT)  tyT       | _  error fi         ("getTypeFromContext: Wrong kind of binding for variable "           (index2name fi ctx i)) 

The match provides some internal consistency checking: under normal circumstances, getTypeFromContext should always be called with a context where the ith binding is in fact a VarBind. In later chapters, though, we will add other forms of bindings (in particular, bindings for type variables), and it is possible that getTypeFromContext will get called with the wrong kind of variable. In this case, it uses the low-level error function to print a message, passing it an info so that it can report the file position where the error occurred.

   val error : info  string  'a 

The result type of the error function is the variable type a, which can be instantiated to any ML type (this makes sense because it is never going to return anyway: it prints a message and halts the program). Here, we need to assume that the result of error is a ty, since that is what the other branch of the match returns.

Note that we look up typing assumptions by index, since terms are represented internally in nameless form, with variables represented as numerical indices. The getbinding function simply looks up the ith binding in the given context:

   val getbinding : info  context  int  binding 

Its definition can be found in the simplebool implementation on the book's web site.

[1]The implementation described here corresponds to the simply typed lambda-calculus (Figure 9-1) with booleans (8-1). The code in this chapter can be found in the simplebool implementation in the web repository.



 < Free Open Study > 



Types and Programming Languages
Types and Programming Languages
ISBN: 0262162091
EAN: 2147483647
Year: 2002
Pages: 262

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net