3
$\begingroup$

Following Wadler's paper "Recursive types for free" and having spent some months on reconstructing the proof that $\exists A. ~ A \times (A\to F~ A)$ is the terminal $F$-coalgebra, I am still not able to prove one step that appears to be important.

Wadler denotes $\exists A. ~ A \times (A\to F~ A)$ by T and defines the functions:

unfold  :  forall X. (X -> F X) -> X -> T
unfold  =  \(X : *) -> \(k : X -> F X) -> \(x : T) -> (X, (k,x))

out     :  T -> F T
out     =  \(t : T) -> case t of { (X,(k,x)) -> F (unfold X k) (k x) }

in      :  F T -> T
in      =  unfold (F T) (F out)

In Wadler's notation, the tuple (X, x) is a packed form of the existentially-typed value built from a specific type X and a value x : P X for some type constructor P.

The main question is to prove that out and in are inverses. Equivalently, to prove that any $F$-coalgebra has a unique map to T.

Wadler does not actually show a detailed proof but mentions that the proof requires the parametricity assumption for unfold:

          k                               unfold X k     
   X ----------> F X                   X -----------> T
   |              |                    |              |
   |              |                    |              |
 h |              | F h   implies    h |              | id
   |              |                    |              |
   |              |                    |              |
   X' ---------> F X'                  X' ----------> T
          k'                             unfold X' k'

The precondition is that h is an F-coalgebra morphism between F-coalgebras X and X'.

This can be written as the relational property that, for any types $X$, $X'$, for any functions $h : X\to X'$, $k : X\to F~X$, $k' : X'\to F~X'$, such that $F(h) \circ k = k'\circ h$ we will then have $\mathrm{unfold}~X~k = \mathrm{unfold}~X'~k' \circ h$. Indeed, this is a consequence of the "free theorem" (i.e., the relational naturality law) for the type signature of unfold.

I have applied this assumption, and I tried applying various other "free theorems", but I still cannot derive $\mathrm{in} \circ \mathrm{out} = \mathrm{id}$. I can only derive a weaker property: $$\mathrm{in} \circ \mathrm{out} = \mathrm{unfold} ~T~\mathrm{out}$$

So, it remains to prove that $\mathrm{unfold} ~T~\mathrm{out} = \mathrm{id}$ but I don't see how this can be proved from parametricity assumptions.

In other words, what I am missing is to prove that, for any value t : T, $$ \mathrm{unfold} ~T~\mathrm{out}~t =t$$

I also tried to encode the existential type in System F. For instance, we then get:

 T = forall R. (forall X. (X -> F X) -> X -> R) -> R

I applied relational parametricity to derive the free theorem for T, but that did not seem to help. I can show that the function $\mathrm{unfold} ~T~\mathrm{out}$ of type $T\to T$ is idempotent, but I cannot show that it is an identity function.

However, I can make progress with a weaker assumption: that any value of type T is a result of unfold applied to some arguments (not necessarily to T and out). In other words, it appears to be necessary to assume that unfold is surjective. But it is not clear how to prove that. (A related question is Is the encoding of existential types in System F adequate? .)

If we assume that any value of type T is obtained as unfold R c r with some type R and some c : R -> F R, r : R then we can apply the "free theorem" of unfold with types X = R and X' = T, with functions h = unfold R c, k = c, k' = out, and obtain (having already shown that unfold R c is an F-coalgebra morphism):

 unfold R c r = unfold T out (unfold R c r)

If we denote t = unfold R c r then we obtain the desired equation t = unfold T out t.

But this equation holds only for t : T that are obtained by applying unfold to some arguments (t = unfold R c r). The equation t = unfold T out t does not follow for arbitrary t : T withough the assumption that any value of type T is obtained as unfold R c r with some R, c, r.

So, the question is, how to prove t = unfold T out t for arbitrary t : T, or how to prove that an arbitrary t : T can be expressed as unfold R c r. (Can we prove that in System F with the encoding of T as shown above, and using parametricity?)

With that, I can complete the proof that in and out are inverses, and that T is a terminal $F$-coalgebra.

Am I missing something? Wadler also cryptically says that another necessary assumption is "the surjective pairing rule" that he writes as:

case t of {(X,y) -> h (X,y)}  =  h t

This is perhaps related to my missing assumption that unfold is surjective. However, I cannot make sense of Wadler's notation as written in this equation. The function h seems to be used in a contradictory way. In the left-hand side, the type of h's argument is the type of a pair (X, y) - a (dependent) pair consisting of a type and a value. In the right-hand side, the type of h's argument is the existential type that does not expose its encapsulated type or value. It is not the type of a pair.

The function h does not seem to be possible to typecheck if encoded in System F. The existential type is encoded as a function, not as a pair.

What is the missing step or a missing assumption here?

Improve this question
$\endgroup$
0

2 Answers 2

Reset to default
3
$\begingroup$

The surjective pairing rule is really just as written there by Wadler. Andrej's interpretation is correct. What the equation h t = case t of { (X, y) -> h (X, y) } buys you is that on the left, h is applied to a variable, whereas on the right, h is applied to a constructor. That lets you lift any property you can prove about h on terms that are constructed using the constructor to a property on any input t, which is precisely what you want out of a property called "surjectivity of constructor".

t = case t of { (X, y) -> (X, y) }                             -- by surjective pairing (h = id)
  = case t of { (X, (k, x)) -> (X, (k, x)) }                   -- by surjective pairing for products
  = case t of { (X, (k, x)) -> unfold X k x }                  -- by definition of unfold
  = case t of { (X, (k, x)) -> unfold T out (unfold X k x) }   -- by unfold X k x = unfold T out (unfold X k x)
  = case t of { (X, (k, x)) -> unfold T out (X, (k, x)) }      -- by definition of unfold
  = unfold T out t                                             -- by surjective pairing (h = unfold T out)
Improve this answer
$\endgroup$
11
  • $\begingroup$ Thank you, I will have to go through this in more detail. For now I have two questions: 1) What is the type of h, and how can it be that the same h is applied on the left to a variable t of type ∃X. P X, but on the right the same h is applied to a pair (X, y)? 2) To "lift any property on constructed terms to a property on any input" seems the same to me as to introduce ∃-intro as Andrej did and then say that any t : ∃X. P X must be of the form t = ∃-intro X y for some X : * and y : P X. Or, the same as to say that unfold is surjective. How can we prove that in System F? $\endgroup$
    – winitzki
    Commented Jun 4 at 6:40
  • $\begingroup$ 1) h : E P -> R for some R. 2) You can't. You can imagine a model where every value is tagged with 0 or 1, and the semantics of terms are tagged with 0. Thus constructors are not surjective since they can't construct 1-tagged values, and yet the tag is unobservable, which allows equations like surjective pairing as an approximation of surjectivity. $\endgroup$
    – Li-yao Xia
    Commented Jun 4 at 7:13
  • $\begingroup$ 1) If h : E P -> R then h cannot be applied to the pair (X, y), and h can only be applied to opaque values of type E P. What am I missing here? 2) Wadler says that the "surjective pairing rule" follows in parametric models. Can it be proved then? $\endgroup$
    – winitzki
    Commented Jun 4 at 8:11
  • $\begingroup$ @winitzki: What is the type of (X, y)? If its type is the same as the domain of h, then h (X, y) is valid by the typing rule for application. The typing rules do not have any side conditions or extra premisess requiring one to check "opaqueness". $\endgroup$
    – Andrej Bauer
    Commented Jun 4 at 8:22
  • $\begingroup$ @AndrejBauer Apparently, Wadler's notation (X, y) is too confusing to me and hinders my reasoning about those terms. Your notation (∃-intro X y) is clearer, as it shows that we are actually using a constructor to build a value of type E P. But to make things actually quite clear, I'd like to encode Wadler's notation in System F. Then $E~P=\forall R.~(\forall X.~P~X\to R)\to R$, Wadler's constructor (X, y) becomes $\Lambda R.~\lambda(k:\forall A.~P~A\to R).~k~X~y$, and Wadler's eliminator (case t of {(X,y) -> w}) : W becomes $t~W~(\Lambda X.~\lambda(y:P~X).~w)$. Is that right? $\endgroup$
    – winitzki
    Commented Jun 4 at 9:03
1
$\begingroup$

Is this not just confusion about notation? If the notation (X, y) is used to signify the introduction rule for ∃ then it does make sense to apply h to a pair (X, y) because it is not really a pair in the sense of simple binary product.

In other words, suppose we write something like ∃-intro X y as the proof term for the introduction rule of exists, i.e.,

∃-intro : (X : Type) → {P : X → Type} → (y : P X) → ∃ X . P X

then the surjective pairing rule becomes

case t of {∃-intro X y -> h (∃-intro X y)}  =  h t

where h : (∃ X . P X) → Y and t : ∃ X . P X. As far as I can tell the application of h is well-typed on both sides.

Improve this answer
$\endgroup$
3
  • $\begingroup$ As far as I understand, the notation case t of {(X, x) -> h X x} is supposed to unpack the existential type into its parts. Under case, we may use the type X and the value x. In my view, by h (X , x) means a function h with a type parameter X and a value parameter x : P X. But your interpretation essentially says case t of { Foo -> h Foo } = h Foo where Foo : $\exists X.~P~X$ and I don't see what this notation brings us. This is not an eliminator for Foo, as it does not destructure Foo. I don't think Wadler meant that. But what did he mean? How to use this equation? $\endgroup$
    – winitzki
    Commented Jun 3 at 13:24
  • $\begingroup$ In your notation ∃-intro X y is an introduction rule. In the scope where we write ∃-intro X y, we are also allowed to see X and y. Then I would transform your syntax into case t of {∃-intro X y -> h' X y} = h (∃-intro X y). And it just looks like a trivial rewriting of h (∃-intro X y) into h' X y where the difference between h and h' is purely syntactical. How can we make progress with the proof, using that? Are we going to assume that all values of type ∃ X . P X are always of the form ∃-intro X y for some X and y? $\endgroup$
    – winitzki
    Commented Jun 3 at 13:31
  • $\begingroup$ I see your dilemma now, thanks for explaining. $\endgroup$
    – Andrej Bauer
    Commented Jun 3 at 15:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.