20.1 Examples

 < Free Open Study > 



20.1 Examples

Lists

First, let's finish off the example of lists of numbers that we started above. To program with lists, we need a constant nil, a constructor cons for adding an element to the front of an existing list, an isnil operation that takes a list and returns a boolean, and destructors hd and tl for extracting the head and tail of a non-empty list. We defined all these as built-in operations in Figure 11-13; our job here is to build them from simpler parts.

The definitions of nil and cons follow directly from the definition of NatList as a two-field variant type.

   nil = <nil=unit> as NatList;  nil : NatList   cons = λn:Nat. λl:NatList. <cons={n,l}> as NatList;  cons : Nat  NatList  NatList 

(Recall from §11.10 that expressions of the form <l=t> as T are used to introduce values of variant types: the value t is tagged with the label l and "injected" into the variant type T. Also, note that the typechecker here automatically "unfolds" the recursive type NatList to the variant type <nil:Unit, cons:{Nat,NatList}>.)

The rest of the basic operations on lists involve testing their structure and extracting appropriate parts. They are all implemented in terms of case.

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

We've arbitrarily decided to define hd of an empty list to be 0 and tl of the empty list to be the empty list. We might alternatively have raised exceptions in these cases.

We can use all these definitions together to write a recursive function that sums the elements of a list:

   sumlist = fix (λs:NatListNat. λl:NatList.                    if isnil l then 0 else plus (hd l) (s (tl l)));  sumlist : NatList  Nat   mylist = cons 2 (cons 3 (cons 5 nil));   sumlist mylist;  10 : Nat 

Note that, although NatList itself is an infinitely long type expression, all its elements are finite lists (because there is no way to use the pairing and tagging primitives or the call-by-value fix to build infinitely large structures).

20.1.1 Exercise [⋆⋆]

One presentation of labeled binary trees defines a tree to be either a leaf (with no label) or else an interior node with a numeric label and two child trees. Define a type NatTree and suitable operations for constructing, destructing, and testing trees. Write a function that performs a depth-first traversal of a tree and returns a list of the labels it finds. Use the fullequirec checker to test your code.

Hungry Functions

Another example illustrating a somewhat trickier use of recursive types is a type of "hungry functions" that can accept any number of numeric arguments and always return a new function that is hungry for more:

   Hungry = μA. NatA; 

An element of this type can be defined using the fix operator:

   f = fix (λf: NatHungry. λn:Nat. f);  f : Hungry   f 0 1 2 3 4 5;  <fun> : Hungry 

Streams

A more useful variant of the Hungry type above is the type Stream of functions that can consume an arbitrary number of unit values, each time returning a pair of a number and a new stream.

   Stream = μA. Unit{Nat,A}; 

We can define two "destructors" for streams; if s is a stream, then hd s is the first number it returns when we pass it unit.

   hd = λ:Stream. (s unit).1;  hd : Stream  Nat 

Similarly, tl s is the new stream that we obtain when we pass unit to s.

   tl = λs:Stream. (s unit).2;  tl : Stream  Stream 

To construct a stream, we use fix as above:

   upfrom0 = fix (λf: NatStream. λn:Nat. λ_:Unit. {n,f (succ n)}) 0;  upfrom0 : Stream   hd upfrom0;  0 : Nat   hd (tl (tl (tl upfrom0)));  3 : Nat 

20.1.2 Exercise [Recommended, ⋆⋆]

Define a stream that yields successive elements of the Fibonacci sequence (1, 1, 2, 3, 5, 8, 13, ...).

Streams can be further generalized to a simple form of processes-functions that accept a number and return a number and a new process.

   Process = μA. Nat{Nat,A}; 

For example, here is a process that, at each step, returns the sum of all the numbers it has been given so far:

   p = fix (λf: NatProcess. λacc:Nat. λn:Nat.              let newacc = plus acc n in              {newacc, f newacc}) 0;  p : Process 

As we did for streams, we can define auxiliary functions for interacting with processes:

   curr = λs:Process. (s 0).1;  curr : Process  Nat   send = λn:Nat. λs:Process. (s n).2;  send : Nat  Process  Process 

If we send the process p the numbers 5, 3, and 20, the number it returns in response to the last interaction is 28.

   curr (send 20 (send 3 (send 5 p)));  28 : Nat 

Objects

A slight rearrangement of the last example gives us another familiar idiom of interacting with data: objects. For instance, here is the type of counter objects that keep track of a number and allow us to either query or increment it:

   Counter = μC. {get:Nat, inc:UnitC}; 

Note that our treatment of objects here is purely functional (like the one in Chapter 19 and unlike Chapter 18): sending a counter object the inc message does not cause this object to mutate its state internally; instead, the operation returns a new counter object with incremented internal state. The use of recursive types here allows us to specify that the returned object has exactly the same type as the original.

The only difference between these objects and the processes discussed above is that an object is a recursively defined record (containing a function), whereas a process was a recursively defined function (returning a tuple). The reason this change in point of view is useful is that we can extend our record to include more than one function-for example, a decrement operation:

   Counter = μC. {get:Nat, inc:UnitC, dec:UnitC}; 

To create a counter object, we use the fixed-point combinator, as we did above.

   c = let create = fix (λf: {x:Nat}Counter. λs: {x:Nat}.                           {get = s.x,                            inc = λ_:Unit. f {x=succ(s.x)},                            dec = λ_:Unit. f {x=pred(s.x)} })       in create {x=0};  c : Counter 

To invoke one of c's operations, we simply project out the appropriate field:

   c1 = c.inc unit;   c2 = c1.inc unit;   c2.get;  2 : Nat 

20.1.3 Exercise [⋆⋆]

Extend the Counter type and the counter c above to include backup and reset operations (as we did in §18.7): invoking backup causes the counter to store its current value in a separate internal register; calling reset causes the counter's value to be reset to the value in this register.

Recursive Values From Recursive Types

A more surprising use of recursive types-and one that clearly reveals their expressive power-is a well-typed implementation of the fixed-point combinator. For any type T, we can define a fixed-point constructor for functions on T as follows.

   fixT  = λf:TT. (λx:(μA.AT). f (x x)) (λx:(μA.AT). f (x x));  fixT : (TT)  T 

Note that, if we erase types, this term is precisely the untyped fixed point combinator that we saw on page 65.

The key trick here is using a recursive type to type the two occurrences of the subexpression x x. As we observed in Exercise 9.3.2, typing this term requires that x have an arrow type whose domain is the type of x itself. Clearly, there is no finite type with this property, but the infinite type μA.AT does the job perfectly.

A corollary of this example is that the presence of recursive types breaks the strong normalization property: we can use the fixT combinator to write a well-typed term whose evaluation (when applied to unit) will diverge.

   divergeT = λ_:Unit. fixT (λx:T. x);  divergeT : Unit  T 

Moreover, since we can can obtain such terms for every type, it follows that every type in this system is inhabited, unlike λ.[4]

Untyped Lambda-Calculus, Redux

Perhaps the best illustration of the power of recursive types is the fact that we can embed the whole untyped lambda-calculus-in a well-typed way-into a statically typed language with recursive types. Let D be the following type:[5]

   D = μX.XX; 

Define an "injection function" lam mapping functions from D to D into elements of D as follows:

   lam = λf:DD. f as D;  lam : D 

To apply one element of D to another, we simply unfold the type of the first, yielding a function, and apply this to the second:

   ap = λf:D. λa:D. f a;  ap : D 

Now, suppose M is a closed lambda-term involving just variables, abstractions, and applications. Then we can construct an element of D representing M, written M*, in a uniform way as follows:

   x*        =  x   (λx.M)*   =  lam (λx:D. M*)   (MN)*     =  ap M* N* 

For example, here is the untyped fixed point combinator expressed as an element of D:

   fixD = lam (λf:D.             ap (lam (λx:D. ap f (ap x x)))                (lam (λx:D. ap f (ap x x))));  fixD : D 

This embedding of the pure lambda-calculus can be extended to include features such as numbers. We change the definition of D to a variant type with one tag for numbers and one for functions:

   D = μX. <nat:Nat, fn:XX>; 

That is, an element of D is either a number or a function from D to D, tagged nat or fn, respectively. The implementation of the lam constructor is essentially the same as before:

   lam = λf:DD. <fn=f> as D;  lam : (DD)  D 

The implementation of ap, though, is different in an interesting way:

   ap = λf:D. λa:D.            case f of              <nat=n>  divergeD unit            | <fn=f>  f a;  ap : D  D  D 

Before we can apply f to a, we need to extract a function from f with a case. This forces us to specify how application behaves when f is not a function. (In this example, we just diverge; we could also raise an exception.) Note how closely the tag-checking here resembles the run-time tag checking in an implementation of a dynamically typed language such as Scheme. In this sense, typed computation may be said to "include" untyped or dynamically typed computation.

Similar tag checking is needed in order to define the successor function on elements of D:

   suc = λf:D. case f of                     <nat=n>  (<nat=succ n> as D)                   | <fn=f>  divergeD unit;  suc : D  D 

The injection of 0 into D is trivial:

   zro = <nat=0> as D;   zro : D 

20.1.4 Exercise []

Extend this encoding with booleans and conditionals, and encode the terms if false then 1 else 0 and if false then 1 else false as elements of D. What happens when we evaluate these terms?

20.1.5 Exercise [Recommended, ⋆⋆]

Extend the datatype D to include records

   D = μX. <nat:Nat, fn:XX, rcd:NatX>; 

and implement record construction and field projection. For simplicity, use natural numbers as field labels-i.e., records are represented as functions from natural numbers to elements of D. Use the fullequirec checker to test your extension.

[4]This fact makes systems with recursive types useless as logics: if we interpret types as logical propositions following the Curry-Howard correspondence (see §9.4) and read "type T is inhabited" as "proposition T is provable," then the fact that every type is inhabited means that every proposition in the logic is provable-that is, the logic is inconsistent.

[5]Readers familiar with denotational semantics will observe that D's definition is precisely the defining property of the universal domains used in semantic models of the pure lambda-calculus.



 < 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