[CST-2] Types

[Matthew Richards]

> Thanks for your reply, but I still don;t fully understand your solution:

Ok, I'll try to explain it (I've changed my mind about it being wrong, by
the way!)

> > Compose_g_d_e = \f:g->Opt_d, g:d->Opt_e ( \v:g (
>
> I guess it should be \v:d  ?

Looking at the type of Compose, it needs to take f and g, and return a
function of type g -> Opt_e.  Hence it should be \v:g.  The remainder should
then be of type Opt_e:

> >                      /\a' (\x':a', f':e->a' (

The type Opt_e is defined as  all a' (a' -> (e->a') -> a'  .  That is, an
Option is just something that takes a value x and a function f; if it's the
option's None, it returns the value x, and if it's Some y then it returns
f(y).

Hence the line above is required to give us something of the right type; the
rest should be something of type a':

> >                      (f v) a' x' (\v':d (

We apply f to v, giving us our result of type Opt_d.  We specialise its
bound type variable to a'.  Then consider:

 - If (f v) is None, we want the result to be None.  That corresponds to
returning the value x'

 - If (f v) is Some v', then we want to return the result of (g v').  So we
supply a function that takes the v', which is of type d, and returns:

                         (g v') a' x' f'

This is like above; if (g v') is None, we return x'; otherwise, the function
f' tells us what to do to the result.  I've corrected this slightly from my
original reply:

> >                      (g v') a' x' (\v'':e (f' v''))
>
> I think replacing (\v'':e (f' v'')) with f' directly would do the
> same job?

As you say,  \v''(f' v'') is just v'.

So, overall, we take 3 arguments and return something of type Opt_e.  An
Option is just something that takes a value x and a function f; if it's
None, the option returns the value x, and if it's Some y then it returns
f(y).

I hope this is at least vaguely comprehensible...

Matthew