[TYPES] Formal treatment of intersection/union/arrow subtyping?

[Rowan Davies]

On Fri, Apr 11, 2008 at 6:12 AM, Paul B Levy <P.B.Levy at cs.bham.ac.uk> wrote:

>
> What's not valid, if I understand you correctly, is
>
> (3)    F T1 & F T2 <: F (T1 & T2)    which is why (1) fails in CBV
>
> (4)    U (S1 | S2) <: U S1 | U S2    which is why (2) fails in CBN.
>
> I was aware of (3), but (4) is new to me.
>

Just a small note that the zero-ary case of the failure of (4) makes
particular sense.

  U bot <:  bot  does not hold.

Intuitively, this is because it's possible to have a thunk that contains a
computation that never yields a value.