25.2 Type Shifting and Substitution

---

25.2 Type Shifting and Substitution

Since types now contain variables, we need to define functions for shifting and substitution of types.

25.2.1 Exercise [⋆]

Using the term-shifting function in Definition 6.2.1 (page 79) as a model, write down a mathematical definition of an analogous function that shifts the variables in types.

In §7.2, we showed shifting and substitution for terms as two separate functions, but remarked that the implementation available from the book's web site actually uses a generic "mapping" function to perform both tasks. A similar mapping function can be used to define shifting and substitution for types. Let us look, now, at these mapping functions.

The basic observation is that shifting and substitution have exactly the same behavior on all constructors except variables. If we abstract out their behavior on variables, then they become identical. For example, here is the specialized shifting function for types that we get by mechanically transcribing the solution to Exercise 25.2.1 into OCaml:

   let typeShiftAbove d c tyT =     let rec walk c tyT = match tyT with         TyVar(x,n) → if x>=c then TyVar(x+d,n+d) else TyVar(x,n+d)       | TyArr(tyT1,tyT2) → TyArr(walk c tyT1,walk c tyT2)       | TyAll(tyX,tyT2) → TyAll(tyX,walk (c+1) tyT2)       | TySome(tyX,tyT2) → TySome(tyX,walk (c+1) tyT2)     in walk c tyT 

The arguments to this function include an amount d by which free variables should be shifted, a cutoff c below which we should not shift (to avoid shifting variables bound by quantifiers within the type), and a type tyT to be shifted.

Now, if we abstract out the TyVar clause from typeShiftAbove into a new argument onvar and drop the argument d, which was only mentioned in the TyVar clause, we obtain a generic mapping function

   let tymap onvar c tyT =     let rec walk c tyT = match tyT with       TyArr(tyT1,tyT2) → TyArr(walk c tyT1,walk c tyT2)     | TyVar(x,n) → onvar c x n     | TyAll(tyX,tyT2) → TyAll(tyX,walk (c+1) tyT2)     | TySome(tyX,tyT2) → TySome(tyX,walk (c+1) tyT2)     in walk c tyT 

from which we can recover the shifting function by supplying the TyVar clause (as a function abstracted on c, x, and n) as a parameter:

   let typeShiftAbove d c tyT =     tymap       (fun c x n → if x>=c then TyVar(x+d,n+d) else TyVar(x,n+d))       c tyT 

It is also convenient to define a specialized version of typeShiftAbove, to be used when the initial cut-off is 0:

   let typeShift d tyT = typeShiftAbove d 0 tyT 

We can also instantiate tymap to implement the operation of substituting a type tyS for the type variable numbered j in a type tyT:

   let typeSubst tyS j tyT =     tymap       (fun j x n → if x=j then (typeShift j tyS) else (TyVar(x,n)))       j tyT 

When we use type substitution during typechecking and evaluation, we will always be substituting for the 0th (outermost) variable, and we will want to shift the result so that that variable disappears. The helper function typeSubstTop does this for us.

   let typeSubstTop tyS tyT =     typeShift (-1) (typeSubst (typeShift 1 tyS) 0 tyT) 

---