20.2 Formalities

 < Free Open Study > 



20.2 Formalities

In the literature on type systems, there are two basic approaches to recursive types. The essential difference between them is captured in their response to a simple question: What is the relation between the type μX.T and its one-step unfolding? For example, what is the relation between NatList and <nil:Unit,cons:{Nat,NatList}>?

  1. The equi-recursive approach takes these two type expressions as definitionally equalinterchangeable in all contextssince they stand for the same infinite tree.[6] It is the typechecker's responsibility to make sure that a term of one type will be allowed as an argument to a function expecting the other, etc.

    The pleasant thing about the equi-recursive treatment is that allowing type expressions to be infinite[7] is the only alteration to the declarative presentations of the systems we already understand. Existing definitions, safety theorems, and proofs remain unchanged, as long as they do not depend on induction on type expressions (which naturally no longer works).

    Of course, the implementation of equi-recursive types requires some work, since typechecking algorithms cannot work directly with infinite structures. Exactly how this can be achieved is the topic of Chapter 21.

  2. The iso-recursive approach, on the other hand, takes a recursive type and its unfolding as different, but isomorphic.

    Formally, the unfolding of a recursive type μX.T is the type obtained by taking the body T and replacing all occurrences of X by the whole recursive typei.e., using the standard notation for substitution, it is [X (μX.T)]T. For example, the type NatList, i.e.,

       μX.<nil:Unit,cons:{Nat,X}>, 

    unfolds to

       <nil:Unit, cons:{Nat, μX.<nil:Unit,cons:{Nat,X}>}>. 

    In a system with iso-recursive types, we introduce, for each recursive type μX.T, a pair of functions

       unfold[μX.T]   :  μX.T  [X  μX.T]T   fold[μX.T]     :  [X  μX.T]T X.T 

    that "witness the isomorphism" by mapping values back and forth between the two types:

    The fold and unfold maps are provided as primitives by the language, as described in Figure 20-1. The fact that they form an isomorphism is captured by the evaluation rule E-UNFLDFLD, which annihilates a fold when it meets a corresponding unfold. (The evaluation rule does not require the type annotations on the fold and the unfold to be the same, since we would have to invoke the typechecker at run time to verify such a constraint. However, in the evaluation of a well-typed program, these two type annotations will be equal whenever E-UNFLDFLD is applied.)


    Figure 20-1: Iso-Recursive Types (λμ)

Both approaches are widely used in both theoretical studies and programming language designs. The equi-recursive style is arguably more intuitive, but places stronger demands on the typechecker, which must effectively infer the points where fold and unfold annotations should occur. Moreover, the interactions between equi-recursive types and other advanced typing features such as bounded quantification and type operators can be quite complex, leading to significant theoretical difficulties (e.g. Ghelli, 1993; Colazzo and Ghelli, 1999) or even undecidable typechecking problems (Solomon, 1978).

The iso-recursive style is notationally somewhat heavier, requiring programs to be decorated with fold and unfold instructions wherever recursive types are used. In practice, however, these annotations can often be "hidden" by coalescing them with other annotations. In languages in the ML family, for example, every datatype definition implicitly introduces a recursive type. Each use of one of the constructors to build a value of the datatype implicitly includes a fold, and each constructor appearing in a pattern match implicitly forces an unfold. Similarly, in Java each class definition implicitly introduces a recursive type, and invoking a method on an object involves an implicit unfold. This felicitous overlap of mechanisms makes the iso-recursive style quite palatable in practice.

For example, here is the NatList example in iso-recursive form. First, it is convenient to define an abbreviation for the unfolded form of NatList:

   NLBody = <nil:Unit, cons:{Nat,NatList}>; 

Now, nil is defined by building a variant, of type NLBody, and then folding it up as a NatList; cons is similar.

   nil = fold [NatList] (<nil=unit> as NLBody);   cons = λn:Nat. λl:NatList. fold [NatList] <cons={n,l}> as NLBody; 

Conversely, the definitions of the isnil, hd, and tl operations need to take a NatList and consider it as a variant so that they can perform a case analysis on its tag. This is achieved by unfolding the argument l:

   isnil = λl:NatList.            case unfold [NatList] l of              <nil=u>  true            | <cons=p>  false;   hd = λl:NatList.          case unfold [NatList] l of            <nil=u>  0          | <cons=p>  p.1;   tl = λl:NatList.          case unfold [NatList] l of            <nil=u>  l          | <cons=p>  p.2; 

20.2.1 Exercise [Recommended, ⋆⋆]

Reformulate some of the other examples in §20.1 (in particular, the fixT example on page 273) with explicit fold and unfold annotations. Check them using the fullisorec checker.

20.2.2 Exercise [⋆⋆ ]

Sketch proofs of the progress and preservation theorems for the iso-recursive system.

[6]The mapping from μ-types to their infinite tree expansions is defined precisely in §21.8.

[7]Strictly speaking, we should say regularsee §21.7.



 < 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