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

[Paul B Levy]

On Thu, 10 Apr 2008, Noam Zeilberger wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> You should also be aware that in the presence of effects, this rule:
>
> (1)  S->T1 & S->T2 <: S->(T1 & T2)
>
> is unsound for call-by-value functions, while this rule:
>
> (2)  S1->T & S2->T <: (S1 | S2)->T
>
> is unsound for call-by-name functions.  To understand why (1) fails
> for CBV, you can read the paper "Intersection types and computational
> effects" by Davies and Pfenning in ICFP 00.  (2) is unsound under CBN
> "by reason of duality"--although the subtyping principle is not
> mentioned explicitly there, the paper "Tridirectional typechecking" by
> Dunfield and Pfenning in POPL 04 should give you an intuition for why
> not to expect (2) in CBN with effects.
>
> On the other hand, (1) is valid under CBN, and (2) under CBV.

Very interesting.

And in call-by-push-value, both are valid.

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.

Paul



-- 
Paul Blain Levy              email: pbl at cs.bham.ac.uk
School of Computer Science, University of Birmingham
Birmingham B15 2TT, U.K.      tel: +44 121-414-4792
http://www.cs.bham.ac.uk/~pbl