Refinement types and computational duality
Noam Zeilberger · 2009
One lesson learned painfully over the past twenty years is the perilous interaction of Curry-style typing with evaluation order and side-effects. This led eventually to the value restriction on polymorphism in ML, as well as, more recently, to similar artifacts in type systems for ML with intersection and union refinement types. For example, some of the traditional subtyping laws for unions and intersections are unsound in the presence of effects, while union-elimination requires an evaluation context restriction in addition to the value restriction on intersection-introduction.