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

[gc@pps.jussieu.fr]

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.

Please note that all of this is true only for Curry-style terms. In the JACM
paper on Semantic Subtyping I cited in my previous post,
http://www.pps.jussieu.fr/~gc/papers/semantic_subtyping.pdf
which uses call by value Church-style notation (1) [and of course (2)] is sound.
This and the difference with Davies and Pfenning 2000 paper are thouroughly
explained in Appendix A2 (cf. the "related work" subsection) ... if you survive 
to read till page 65 :-)

---Beppe---