Exercise 3.18
See Exercise 3.14. We define the type $Tree$, representing the set of binary trees with boolean-labelled nodes and leaves, by
$$Tree ≡ Πα : ∗. (Bool →α) →(Bool →α →α →α) →α$$
Then $λα : ∗. λu : Bool →α. λv : Bool →α →α →α. M$ has type $Tree$, for every λ2-term $M$ of type $α$.
(a) Sketch the three trees that are represented if we take for M, respectively:
$u \; False$
$v \; True(u \; False)(u \; True)$
$v \; True(u \; True)(v \; False(u \; True)(u \; False))$
(b) Give a λ2-term which, on input a polymorphic boolean $p$ and two trees $s$ and $t$, delivers the combined tree with $p$ on top, left subtree $s$ and right subtree $t$.
(a) The value of a node is of type Bool. The function $u$ represents a leaf, a terminal node, and the function $v$ represents a node with two sub-trees.
The following diagram shows representations of the three terms (click to enlarge).
(b) The desired λ2-term must have a type $Bool → Tree → Tree → Tree$.
We have $s$ and $t$ as follows:
$$ s ≡ λα : ∗. λu : Bool →α. λv : Bool →α →α →α. M_s $$
$$ t ≡ λα : ∗. λu : Bool →α. λv : Bool →α →α →α. M_t $$
Here $M_s$ and $M_t$ have type $α$, and the entire term has type $Tree$.
The combined tree is as follows:
$$ λα : ∗. λu : Bool →α. λv : Bool →α →α →α. v (p)(M_s)(M_t) $$
We can derive $M_s:α$ and $M_t:α$ from $s$ and $t$ as follows
$$M_s = sαuv, \quad M_t = tαuv$$
So the combined tree is:
$$ λα : ∗. λu : Bool →α. λv : Bool →α →α →α. v(p)(sαuv)(tαuv) $$
We can write the desired λ2-term with type $Bool → Tree → Tree → Tree$.
$$ λp:Bool. λs,t:Tree . ( λα : ∗. λu : Bool →α. λv : Bool →α →α →α. v(p)(sαuv)(tαuv) )$$
