24.3 Encoding Existentials

 < Free Open Study > 



24.3 Encoding Existentials

The encoding of pairs as a polymorphic type in §23.4 suggests a similar encoding for existential types in terms of universal types, using the intuition that an element of an existential type is a pair of a type and a value:

That is, an existential package is thought of as a data value that, given a result type and a continuation, calls the continuation to yield a final result. The continuation takes two argumentsa type X and a value of type Tand uses them in computing the final result.

Given this encoding of existential types, the encoding of the packaging and unpackaging constructs is essentially forced. To encode a package

   {*S,t} as {$X,T} 

we must use S and t to build a value of type "Y. ("X. TY) Y. This type begins with a universal quantifier, the body of which is an arrow type. An element of this type should therefore begin with two abstractions:

To complete the job, we need to return a result of type Y; clearly, the only way to do this is to apply f to some appropriate arguments. First, we supply the type S (this is a natural choice, being the only type we have lying around at the moment):

Now, the type application f [S] has type [X S](TY), i.e., ([X S]T)Y. We can thus supply t (which, by rule T-PACK, has type [X S]T) as the next argument:

The type of the whole application f [S] t is now Y, as required.

To encode the unpacking construct let {X,x}=t1 in t2, we proceed similarly. First, the typing rule T-UNPACK tells us that t1 should have some type {$X,T11}, that t2 should have type T2 (under an extended context binding X and x:T11), and that T2 is the type we expect for the whole let...in... expression.[6] As in the Church encodings in §23.4, the intuition here is that the introduction form ({*S,t}) is encoded as an active value that "performs its own elimination." So the encoding of the elimination form here should simply take the existential package t1 and apply it to enough arguments to yield a result of the desired type T2:

The first argument to t1 should be the desired result type of the whole expression, i.e., T2:

Now, the application t1 [T2] has type ("X. T11T2) T2. That is, if we can now supply another argument of type ("X.T11T2), we will be finished. Such an argument can be obtained by abstracting the body t2 on the variables X and x:

This finishes the encoding.

24.3.1 Exercise [Recommended, ⋆⋆ ]

Take a blank piece of paper and, without looking at the above encoding, regenerate it from scratch.

24.3.2 Exercise [⋆⋆⋆]

What must we prove to be confident that this encoding of existentials is correct?

24.3.3 Exercise [⋆⋆⋆⋆]

Can we go the other direction, encoding universal types in terms of existential types?

[6]Strictly speaking, the fact that the translation requires these extra bits of type information not present in the syntax of terms means that what we are translating is actually typing derivations, not terms. We have seen a similar situation in the definition of the coercion semantics for subtyping in §15.6.



 < 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