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

[Noam Zeilberger]

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.  How to
derive these valid laws while avoiding the unsound ones is sketched
very briefly in Section 4 of my paper "On the unity of duality" in the
current issue of APAL -- but I'm hoping to write something more
complete about this soon.  (If you are *very* curious, you can
download my thesis proposal.)

Noam