25.3 Terms

 < Free Open Study > 



25.3 Terms

At the level of terms, the work to be done is similar. We begin by extending the term datatype from Chapter 10 with the introduction and elimination forms for universal and existential types.

   type term =       TmVar of info * int * int     | TmAbs of info * string * ty * term     | TmApp of info * term * term     | TmTAbs of info * string * term     | TmTApp of info * term * ty     | TmPack of info * ty * term * ty     | TmUnpack of info * string * string * term * term 

The definitions of shifting and substitution for terms are similar to those in Chapter 10. However, let us write them here in terms of a common generic mapping function, as we did for types in the previous section. The mapping function looks like this:

   let tmmap onvar ontype c t =     let rec walk c t = match t with       TmVar(fi,x,n)  onvar fi c x n     | TmAbs(fi,x,tyT1,t2)  TmAbs(fi,x,ontype c tyT1,walk (c+1) t2)     | TmApp(fi,t1,t2)  TmApp(fi,walk c t1,walk c t2)     | TmTAbs(fi,tyX,t2)  TmTAbs(fi,tyX,walk (c+1) t2)     | TmTApp(fi,t1,tyT2)  TmTApp(fi,walk c t1,ontype c tyT2)     | TmPack(fi,tyT1,t2,tyT3)          TmPack(fi,ontype c tyT1,walk c t2,ontype c tyT3)     | TmUnpack(fi,tyX,x,t1,t2)          TmUnpack(fi,tyX,x,walk c t1,walk (c+2) t2)     in walk c t 

Note that tmmap takes four arguments-one more than tymap. To see why, notice that terms may contain two different types of variables: term variables as well as type variables embedded in type annotations in terms. So during shifting, for example, there are two kinds of "leaves" where we may need to do some real work: term variables and types. The ontype parameter tells the term mapper what to do when processing a term constructor containing a type annotation, as in the TmAbs case. If we were dealing with a larger language, there would be several more such cases.

Term shifting can be defined by giving tmmap appropriate arguments.

   let termShiftAbove d c t =     tmmap       (fun fi c x n  if x>=c then TmVar(fi,x+d,n+d)                        else TmVar(fi,x,n+d))       (typeShiftAbove d)       c t   let termShift d t = termShiftAbove d 0 t 

On term variables, we check the cutoff and construct a new variable, just as we did in typeShiftAbove. For types, we call the type shifting function defined in the previous section.

The function for substituting one term into another is similar.

   let termSubst j s t =     tmmap       (fun fi j x n  if x=j then termShift j s else TmVar(fi,x,n))       (fun j tyT  tyT)       j t 

Note that type annotations are not changed by termSubst (types cannot contain term variables, so a term substitution will never affect them).

We also need a function for substituting a type into a term-used, for example, in the evaluation rule for type applications:

This one can also be defined using the term mapper:

   let rec tytermSubst tyS j t =     tmmap (fun fi c x n  TmVar(fi,x,n))           (fun j tyT  typeSubst tyS j tyT) j t 

This time, the function that we pass to tmmap for dealing with term variables is the identity (it just reconstructs the original term variable); when we reach a type annotation, we perform a type-level substitution on it.

Finally, as we did for types, we define convenience functions packaging the basic substitution functions for use by eval and typeof.

   let termSubstTop s t =     termShift (-1) (termSubst 0 (termShift 1 s) t)   let tytermSubstTop tyS t =     termShift (-1) (tytermSubst (typeShift 1 tyS) 0 t) 



 < 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