[CST-2] Types ex 6.3.4

[Mark Seaborn]

Peter Taylor <pjt33@hermes.cam.ac.uk> wrote:

> Has anyone got anywhere with Types ex 6.3.4 ?  I think it involves assuming
> the existence of an impossible T, but I'm not sure.

T isn't impossible:  map is a common example:

  map : (alpha1 -> alpha2) -> (tau(alpha1) -> tau(alpha2))

in this case, tau(a) = list(a).  (Writing tau(x) instead of the more
confusing tau[x/alpha].)

Here are the answers:

R = /\alpha. \f:tau(alpha)->alpha. \x:i. x alpha f

I = \x:tau(i). /\alpha. \f:tau(alpha)->alpha.
      f (T i alpha (R alpha f) x)

(This gives:
  R alpha f (I x) = I x alpha f
                  = f (I i alpha (R alpha f) x)
as the question wants.)

You can construct R and I mechanically:  when you need a value of type
\/alpha.y, write /\alpha.Y and try to find a Y with type y.

When you need a value of type x -> y, write \z:x.Y and try to find a Y
with type y.

If you need a value of type y, and you have a value f of type x -> y,
write f X, and try to find an X with type x.

In this question I don't think it's useful to think what R, I and T
could be used for, because the type i is not a useful type.

-- 
         Mark Seaborn
   - mseaborn@bigfoot.com - http://www.srcf.ucam.org/~mrs35/ -

 ``In our country, we put people in prison, we tear out their fingernails to
  achieve this result. What's your secret?'' -- Pravda editor, touring the US