30.2 Example

---

30.2 Example

We will see an extended example of programming using abstractions ranging over type operators in Chapter 32. Here is a much smaller one.

Recall the encoding of abstract data types in terms of existentials from §24.2. Suppose now that we want to implement an ADT of pairs, in the same way as we earlier implemented ADTs of types like counters. This ADT should provide operations for building pairs and taking them apart. Moreover, we would like these operations to be polymorphic, so that we can use them to build and use pairs of elements from any types S and T. That is, the abstract type that we provide should not be a proper type, but rather an abstract type constructor (or operator). It should be abstract in the same sense as the earlier ADTs: for each S and T, the pair operation should take an element of S and one of T and return an element of Pair S T, while fst and snd should take a Pair S T and return, respectively, an S or a T, and these facts should be all that a client of our abstraction knows about it.

From these requirements, we can read off the signature that we want our pair ADT to present to the world:

   PairSig = {$Pair::*⇛*⇛*,              {pair: "X.  "Y. X→Y→(Pair X Y),               fst: "X. "Y. (Pair X Y)→X,               snd: "X. "Y. (Pair X Y)→Y}}; 

That is, an implementation of pairs should provide a type operator Pair plus polymorphic functions pair, fst, and snd of the given types.

Here is one way of building a package with this type:

   pairADT =      {*λX. λY. "R. (X→Y→R) → R,       {pair = λX. λY. λx:X.  λy:Y.                 λR. λp:X→Y→R. p x y,        fst = λX. λY. λp: "R. (X→Y→R) → R.                 p [X] (λx:X. λy:Y. x),        snd = λX. λY. λp: "R. (X→Y→R) → R.                 p [Y] (λx:X. λy:Y. y)}} as PairSig; ▸ pairADT : PairSig 

The hidden representation type is the operator λX. λY. "R. (X→Y→R) → R that we have used before (§23.4) to represent pairs. The components pair, fst, and snd of the body are appropriate polymorphic functions.

Having defined pairADT, we can unpack it in the usual way.

   let {Pair,pair}=pairADT   in pair.fst [Nat] [Bool] (pair.pair [Nat] [Bool] 5 true); ▸ 5 : Nat 

---