23.4 Examples

 < Free Open Study > 



23.4 Examples

We now develop several examples of programming with polymorphism. To warm up, we start with a few small but increasingly tricky examples, showing some of the expressive power of System F. We then review the basic ideas of "ordinary" polymorphic programming with lists, trees, etc. The last two subsections introduce typed versions of the Church encodings of simple algebraic datatypes like booleans, numbers, and lists that we saw in Chapter 5 for the untyped lambda-calculus. Although these encodings are of small practical importanceit is easier to compile good code for these important features if they are built into high-level programming languages as primitivesthey make excellent exercises for understanding both the intricacies and the power of System F. In Chapter 24, we will see some additional applications of polymorphism in the domain of modular programming and abstract data types.

Warm-Ups

We have seen already how type abstraction and application can be used to define a single polymorphic identity function

   id = λX. λx:X. x;  id : "X. X  X 

and instantiate it to yield any concrete identity function that may be required:

   id [Nat];  <fun> : Nat  Nat   id [Nat] 0;  0 : Nat 

A more useful example is the polymorphic doubling function:

   double = λX. λf:XX. λa:X. f (f a);  double : "X. (XX)  X  X 

The abstraction on the type X allows us to obtain doubling functions for specific types by instantiating double with different type arguments:

   doubleNat = double [Nat];  doubleNat : (NatNat)  Nat  Nat   doubleNatArrowNat = double [NatNat];  doubleNatArrowNat : ((NatNat)NatNat)                        (NatNat)  Nat  Nat 

Once instantiated with a type argument, double can be further applied to an actual function and argument of appropriate types:

   double [Nat] (λx:Nat. succ(succ(x))) 3;  7 : Nat 

Here is a slightly trickier example: polymorphic self-application. Recall that, in the simply typed lambda-calculus, there is no way to type the untyped term λx. x x (Exercise 9.3.2). In System F, on the other hand, this term becomes typable if we give x a polymorphic type and instantiate it appropriately:

   selfApp = λx:"X.XX.  x ["X.XX] x;  selfApp : ("X. XX)  ("X. X  X) 

As a (slightly) more useful example of self application, we can apply the polymorphic double function to itself, yielding a polymorphic quadrupling function:

   quadruple = λX. double [XX] (double [X]);  quadruple : "X. (XX)  X  X 

23.4.1 Exercise [ ]

Using the typing rules in Figure 23-1, convince yourself that the terms above have the types given.

Polymorphic Lists

Most real-world programming with polymorphism is much more pedestrian than the tricky examples above. As an example of straightforward polymorphic programming, suppose our programming language is equipped with a type constructor List and term constructors for the usual list manipulation primitives, with the following types.

  nil : "X. List X   cons : "X. X  List X  List X   isnil : "X. List X  Bool   head : "X. List X  X   tail : "X. List X  List X 

When we first introduced lists in §11.12, we used "custom" inference rules to allow the operations to be applied to lists with elements of any type. Here, we can give the operations polymorphic types expressing exactly the same constraintsthat is, lists no longer need to be "baked into" the core language, but can simply be considered as a library providing several constants with particular polymorphic types. The same holds for the Ref type and the primitive operations on reference cells in Chapter 13, and many other common data and control structures.

We can use these primitives to define our own polymorphic operations on lists. For example, here is a polymorphic map function that takes a function from X to Y and a list of Xs and returns a list of Ys.

   map = λX. λY.          λf: XY.           (fix (λm: (List X)  (List Y).                   λl: List X.                    if isnil [X] l                      then nil [Y]                      else cons [Y] (f (head [X] l))                                    (m (tail [X] l))));  map : "X. "Y. (XY)  List X  List Y   l = cons [Nat] 4 (cons [Nat] 3 (cons [Nat] 2 (nil [Nat])));  l : List Nat   head [Nat] (map [Nat] [Nat] (λx:Nat. succ x) l);  5 : Nat 

23.4.2 Exercise [ ]

Convince yourself that map really has the type shown.

23.4.3 Exercise [Recommended, ⋆⋆]

Using map as a model, write a polymorphic list-reversing function:

   reverse : "X. List X  List X. 

This exercise is best done on-line. Use the fullomega checker and copy the contents of the file test.f from the fullomega directory to the top of your own input file. (The file contains definitions of the List constructor and associated operations that require the powerful abstraction facilities of System Fω, discussed in Chapter 29. You do not need to understand exactly how they work to proceed with the present exercise.)

23.4.4 Exercise [⋆⋆ ]

Write a simple polymorphic sorting function

   sort : "X. (XXBool)  (List X)  List X 

where the first argument is a comparison function for elements of type X.

Church Encodings

We saw in §5.2 that a variety of primitive data values such as booleans, numbers, and lists can be encoded as functions in the pure untyped lambda-calculus. In this section, we show how these Church encodings can also be carried out in System F. Readers may want to refer to §5.2 to refresh their intuitions about Church encodings.

These encodings are interesting for two reasons. First, they give our understanding of type abstraction and application a good workout. Second, they demonstrate that System F, like the pure untyped lambda-calculus, is computationally a very rich language, in the sense that the pure system can express a large range of data and control structures. This means that, if we later design a full-scale programming language with System F as its core, we can add these features as primitives (for efficiency, and so that we can equip them with more convenient concrete syntax) without disturbing the fundamental properties of the core language. This will not be true of all interesting high-level language features, of course. For example, adding references to System F, as we did for λin Chapter 13, represents a real change in the fundamental computational nature of the system.

Let us begin with the Church booleans. Recall that, in the untyped lambda-calculus, we represented the boolean constants true and false by lambda-terms tru and fls defined like this:

   tru = λt. λf. t;   fls = λt. λf. f; 

Each of these terms takes two arguments and returns one of them. If we want to assign a common type to tru and fls, we had better assume that the two arguments have the same type (since the caller will not know whether it is interacting with tru or fls), but this type may be arbitrary (since tru and fls do not need to do anything with their arguments except return one of them). This leads us to the following type for tru and fls.

   CBool = "X.XXX; 

The System-F terms tru and fls are obtained by adding appropriate type annotations to the untyped versions above.

   tru = λX. λt:X. λf:X. t;  tru : CBool   fls = λX. λt:X. λf:X. f;  fls : CBool 

We can write common boolean operations like not by constructing a new boolean that uses an existing one to decide which of its arguments to return:

   not = λb:CBool. λX. λt:X. λf:X. b [X] f t;  not : CBool  CBool 

23.4.5 Exercise [Recommended, ]

Write a term and that takes two arguments of type CBool and computes their conjunction.

We can play a similar game with numbers. The Church numerals introduced in §5.2 encode each natural number n as a function that take two arguments s and z and applies s to z, n times:

   c0 = λs. λz. z;   c1 = λs. λz. s z;   c2 = λs. λz. s (s z);   c3 = λs. λz. s (s (s z)); 

Clearly, the z argument should have the same type as the domain of s, and the result returned by s should again have the same type. This leads us to the following type for Church numerals in System F:

   CNat = "X. (XX)  X  X; 

The elements of this type are obtained by adding appropriate annotations to the untyped Church numerals:

   c0  =  λX. λs:XX. λz:X. z;  c0 : CNat   c1   =  λX. λs:XX. λz:X. s z;  c1 : CNat   c2   =  λX. λs:XX. λz:X. s (s z);  c2 : CNat 

A typed successor function on Church numerals can be defined as follows.

   csucc = λn:CNat. λX. λs:XX. λz:X. s (n [X] s z);  csucc : CNat  CNat 

That is, csucc n returns an element of CNat that, given s and z, applies s to z, n times (by applying n to s and z), and then once more. Other arithmetic operations can be defined similarly. For example, addition can be defined either in terms of successor,

   cplus = λm:CNat. λn:CNat. m [CNat] csucc n;  cplus : CNat  CNat  CNat 

or more directly:

   cplus = λm:CNat. λn:CNat.  λX. λs:XX. λz:X. m [X] s (n [X] s z);  cplus : CNat  CNat  CNat 

If our language also includes primitive numbers (Figure 8-2), then we can convert from Church numerals to ordinary ones using the following function:

   cnat2nat = λm:CNat. m [Nat] (λx:Nat. succ(x)) 0;  cnat2nat : CNat  Nat 

This allows us to verify that our operations on Church numerals actually compute the desired arithmetic functions:

   cnat2nat (cplus (csucc c0) (csucc (csucc c0)));  3 : Nat 

23.4.6 Exercise [Recommended, ⋆⋆]

Write a function iszero that will return tru when applied to the Church numeral c0 and fls otherwise.

23.4.7 Exercise [⋆⋆ ]

Verify that the terms

   ctimes = λm:CNat. λn:CNat.  λX. λs:XX. n [X] (m [X] s);  ctimes : CNat  CNat  CNat   cexp = λm:CNat. λn:CNat.  λX. n [XX] (m [X]);  cexp : CNat  CNat  CNat 

have the indicated types. Give an informal argument that they implement the arithmetic multiplication and exponentiation operators.

23.4.8 Exercise [Recommended, ⋆⋆]

Show that the type

   PairNat = "X. (CNatCNatX)  X; 

can be used to represent pairs of numbers, by writing functions

   pairNat : CNatCNatPairNat;   fstNat : PairNatCNat;   sndNat : PairNatCNat; 

for constructing elements of this type from pairs of numbers and for accessing their first and second components.

23.4.9 Exercise [Recommended, ⋆⋆⋆]

Use the functions defined in Exercise 23.4.8 to write a function pred that computes the predecessor of a Church numeral (returning 0 if its input is 0). Hint: the key idea is developed in the example in §5.2. Define a function f : PairNatPairNat that maps the pair (i, j) into (i + 1, i)that is, it throws away the second component of its argument, copies the first component to the second, and increments the first. Then n applications of f to the starting pair (0, 0) yields the pair (n, n - 1), from which we extract the predecessor of n by projecting the second component.

23.4.10 Exercise [⋆⋆⋆]

There is another way of computing the predecessor function on Church numerals. Let k stand for the untyped lambda-term λx. λy. x and i for λx. x. The untyped lambda-term

   vpred = λn. λs. λz. n (λp. λq. q (p s)) (k z) i 

(from Barendregt, 1992, who attributes it to J. Velmans) computes the predecessor of an untyped Church numeral. Show that this term can be typed in System F by adding type abstractions and applications as necessary and annotating the bound variables in the untyped term with appropriate types. For extra credit, explain why it works!

Encoding Lists

As a final example, let us extend the Church encodings of numbers to lists. This is a nice demonstration of the expressive power of pure System F, since it shows that all of the programming examples in the subsection above on polymorphic list manipulation can actually be expressed in the pure language. (For convenience, we do use the fix construct for defining general recursive functions, but essentially the same constructions can be carried out without it. See Exercises 23.4.11 and 23.4.12.)

We saw in Exercise 5.2.8 that lists can be encoded in the untyped lambda-calculus in a fashion quite similar to the encoding of natural numbers. In effect, a number in unary notation is like a list of dummy elements. Generalizing this idea to elements of any type, we arrive at a Church encoding for lists, where a list with elements x, y, and z is represented as a function that, given any function f and starting value v, calculates f x (f y (f z v)). In OCaml terminology, a list is represented as its own fold_right function.

The type List X of lists with elements of type X is defined as follows:

   List X = "R. (XRR)  R  R; 

The nil value for this representation of lists easy to write.[2]

   nil = λX. (λR. λc:XRR. λn:R. n) as List X;  nil : "X. List X 

The cons and isnil operations are also easy:

   cons = λX. λhd:X. λtl:List X.            (λR. λc:XRR. λn:R. c hd (tl [R] c n)) as List X;  cons : "X. X  List X  List X   isnil = λX. λl:List X. l [Bool] (λhd:X. λtl:Bool. false) true;  isnil : "X. List X  Bool 

For the head operation, we need to work a little harder. The first difficulty is what to do about head of the empty list. We can address this by recalling that, if we have a general fixed point operator in the language, we can use it to construct an expression of any type. In fact, using type abstraction, we can go further and write a single, uniform function that, given a type X, yields a function from Unit to X that diverges when applied to unit.

   diverge = λX. λ_:Unit. fix (λx:X. x);  diverge : "X. Unit  X 

Now we can use diverge [X] unit as the "result" of head [X] nil.

   head = λX. λl:List X. l [X] (λhd:X. λtl:X. hd) (diverge [X] unit);  head : "X. List X  X 

Unfortunately, this definition is not yet quite what we want: it will always diverge, even when applied to non-empty lists. To get the right behavior, we need to reorganize it a little so that diverge[X] is not actually passed its Unit argument when it is supplied as an argument to l. This is accomplished by removing the unit argument and changing the type of the first argument to l correspondingly:

   head =     λX. λl:List X.       (l [UnitX] (λhd:X. λtl:UnitX. λ_:Unit. hd) (diverge [X]))       unit;  head : "X. List X  X 

That is, l is applied to a function of type X(UnitX)(UnitX) and a base value of type UnitX, and it constructs a function of type UnitX. In the case where l represents the empty list, this result will be diverge[X]; but in the case where l represents a non-empty list, the result will be a function that takes unit and returns the head element of l. The result from l is applied to unit at the end to get the actual head element (or, if we are unlucky, diverge), so that head has the type we expect.

For the tail function, we use the abbreviation Pair X Y (generalizing the PairNat type from Exercise 23.4.8) for the Church encoding of pairs with first component of type X and second component of type Y:

   Pair X Y = "R. (XYR)  R; 

The operations on pairs are simple generalizations of the operations on the type PairNat above:

  pair : "X. "Y. X  Y  Pair X Y   fst : "X. "Y. Pair X Y  X   snd : "X. "Y. Pair X Y  Y 

Now the tail function can be written like this:

   tail =     λX. λl: List X.       (fst [List X] [List X] (          l [Pair (List X) (List X)]            (λhd: X. λtl: Pair (List X) (List X).              pair [List X] [List X]                (snd [List X] [List X] tl)                (cons [X] hd (snd [List X] [List X] tl)))            (pair [List X] [List X] (nil [X]) (nil [X]))));  tail : "X. List X  List X 

23.4.11 Exercise [⋆⋆]

Strictly speaking, the examples in this subsection have not been expressed in pure System F, since we used the fix operator to construct a value to be "returned" when head is applied to an empty list. Write an alternative version of head that takes an extra parameter to be returned (instead of diverging) when the list is empty.

23.4.12 Exercise [Recommended, ⋆⋆⋆]

In pure System F (without fix), write a function insert of type

   "X. (XXBool)  List X  X  List X 

that takes a comparison function, a sorted list, and a new element, and inserts the element into the list at the appropriate point (i.e., after all the elements smaller than it). Next, use insert to build a sorting function for lists in pure System F.

[2]The as annotation here helps the typechecker print the type of nil in a readable form. As we saw in §11.4, all the typecheckers used in this book perform a simple abbreviation-collapsing step before printing types, but the collapsing function is not smart enough to deal automatically with "parametric abbreviations" like List.



 < 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