23.6 Erasure, Typability, And Type Reconstruction

 < Free Open Study > 



23.6 Erasure, Typability, And Type Reconstruction

As we did for λ in §9.5, we can define a type erasure function mapping System F terms to untyped lambda-terms by stripping out all their type annotations (including all type abstractions and applications):

  •  

    erase(x)

    =

    x

    erase(λx:T1 . t2)

    =

    λx. erase(t2)

    erase(t1 t2)

    =

    erase(t1) erase(t2)

    erase(λX. t2)

    =

    erase(t2)

    erase(t1 [T2])

    =

    erase(t1)

A term M in the untyped lambda-calculus is said to be typable in System F if there is some well-typed term t such that erase(t) = m. The type reconstruction problem then asks, given an untyped term m, whether we can find some well-typed term that erases to m.

Type reconstruction for System F was one of the longest-standing problems in the programming languages literature, remaining open from the early 1970s until it was finally settled (negatively) by Wells in the early 1990s.

23.6.1 Theorem [Wells, 1994]

It is undecidable whether, given a closed term m of the untyped lambda-calculus, there is some well-typed term t in System F such that erase(t) = m.

Not only full type reconstruction but also various forms of partial type reconstruction are known to be undecidable for System F. For example, consider the following "partial erasure" function, which leaves intact all typing annotations except the arguments to type applications:

  •  

    erasep(x)

    =

    x

    erasep(λx:T1 . t2)

    =

    λx:T1 . erasep(t2)

    erasep(t1 t2)

    =

    erasep(t1) erasep(t2)

    erasep(λX. t2)

    =

    λX. erasep(t2)

    erasep(t1 [T2])

    =

    erasep(t1) []

Note that type applications are still marked (with empty square brackets) in the erased terms; we can see where they must occur, but not what type must be supplied.

23.6.2 Theorem [Boehm 1985, 1989]

It is undecidable whether, given a closed term s in which type applications are marked but the arguments are omitted, there is some well-typed System F term t such that erasep(t) = s.

Boehm showed that this form of type reconstruction was just as hard as higher-order unification, hence undecidable. Interestingly, this negative result led directly to a useful partial type reconstruction technique (Pfenning, 1988, 1993a) based on Huet's earlier work on effcient semi-algorithms for higher-order unification (Huet, 1975). Later improvements in this line of development have included using a more refined algorithm for higher-order constraint solving (Dowek, Hardin, Kirchner, and Pfenning, 1996), eliminating the troublesome possibilities of nontermination or generation of non-unique solutions. Experience with related algorithms in languages such as LEAP (Pfenning and Lee, 1991), Elf (Pfenning, 1989), and FX (O'Toole and Gifford, 1989) has shown them to be quite well behaved in practice.

A different approach to partial type reconstruction was sparked by Perry's observation that first-class existential types (see Chapter 24) can be integrated with ML's datatype mechanism (Perry, 1990); the idea was further developed by Läufer and Odersky (Läufer, 1992; Läufer and Odersky, 1994). In essence, datatype constructors and destructors can be regarded as explicit type annotations, marking where values must be injected into and projected from disjoint union types, where recursive types must be folded and unfolded, and (when existentials are added) where packing and unpacking must occur. This idea was extended to include first-class (impredicative) universal quantifiers by Rémy (1994). A more recent proposal by Odersky and Läufer (1996), further developed by Garrigue and Rémy (1997), conservatively extends ML-style type reconstruction by allowing programmers to explicitly annotate function arguments with types, which may (unlike the annotations that can be inferred automatically) contain embedded universal quantifiers, thus partly bridging the gap between ML and more powerful impredicative systems. This family of approaches to type reconstruction has the advantage of relative simplicity and clean integration with the polymorphism of ML.

A pragmatic approach to partial type reconstruction for systems involving both subtyping and impredicative polymorphism, called local type inference (or local type reconstruction), was proposed by Pierce and Turner (1998; also see Pierce and Turner, 1997; Hosoya and Pierce, 1999). Local type inference has appeared in several recent language designs, including GJ (Bracha, Odersky, Stoutamire, and Wadler, 1998) and Funnel (Odersky and Zenger, 2001), the latter introducing a more powerful form called colored local type inference (Odersky, Zenger, and Zenger, 2001).

A simpler but less predictable greedy type inference algorithm was proposed by Cardelli (1993); similar algorithms have also been used in proof-checkers for dependent type theories, such as NuPrl (Howe, 1988) and Lego (Pollack, 1990). The idea here is that any type annotation may be omitted by the programmer: a fresh unification variable X will be generated for each one by the parser. During typechecking, the subtype-checking algorithm may be asked to check whether some type S is a subtype T, where both S and T may contain unification variables. Subtype-checking proceeds as usual until a subgoal of the form X <: T or T <: X is encountered, at which point X is instantiated to T, thus satisfying the immediate constraint in the simplest possible way. However, setting X to T may not be the best possible choice, and this may cause later subtype-checks for types involving X to fail when a different choice would have allowed them to succeed; but, again, practical experience with this algorithm in Cardelli's implementation and in an early version of the Pict language (Pierce and Turner, 2000) shows that the algorithm's greedy choice is correct in nearly all cases. However, when it goes wrong, the greedy algorithm's behavior can be quite puzzling to the programmer, yielding mysterious errors far from the point where a suboptimal instantiation is made.

23.6.3 Exercise [⋆⋆⋆⋆]

The normalization property implies that the untyped term omega = (λx. xx) (λy. yy) cannot be typed in System F, since reduction of omega never reaches a normal form. However, it is possible to give a more direct, "combinatorial" proof of this fact, using just the rules defining the typing relation.

  1. Let us call a System F term exposed if it is a variable, an abstraction λx:T.t, or an application t s (i.e., if it is not a type abstraction λX.t or type application t [S]).

    Show that if t is well typed (in some context) and erase(t) = m, then there is some exposed term s such that erase(s) = m and s is well typed (possibly in a different context).

  2. Write as shorthand for a nested sequence of type abstractions of the form λX1...λXn.t. Similarly, write t [Ā] for a nested sequence of type applications ((t [A1])...[An-1]) [An] and for a nested sequence of polymorphic types "X1... "Xn.T. Note that these sequences are allowed to be empty. For example, if is the empty sequence of type variables, then is just T.

    Show that if erase(t) = m and Г t : T, then there exists some s of the form , for some sequence of type variables , some sequence of types Ā, and some exposed term u, with erase(s) = m and Г s : T.

  3. Show that if t is an exposed term of type T (under Г) and erase(t) = m n, then t has the form s u for some terms s and u such that erase(s) = m and erase(u) = n, with Г s : UT and Г u : U.

  4. Suppose x:T Î Г. Show that if Г u : U and erase(u) = x x, then either

    1. , where , or else

    2. , where for some sequences of types Ā and with and .

  5. Show that if erase(s) = λx.m and Г s : S, then S has the form , for some , S1, and S2.

  6. Define the leftmost leaf of a type T as follows:

    •  

      leftmost-leaf(X)

      =

      X

      leftmost-leaf(ST)

      =

      leftmost-leaf(S)

      leftmost-leaf("X.S)

      =

      leftmost-leaf(S).

    Show that if , then it must be the case that leftmost-leaf(T1) = Xi for some .

  7. Show that omega is not typable in System F.



 < 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