Some Uses of the Intersection Type
by Stuart F. Allen, Robert L. Constable
We will present a perspicuous example using the intersection type to express specifications from which one may extract recursive programs (a while-loop in this case), that do not use their bounds.
We will also discuss the use of "guarded types", which are intersection types Isect(x:A.B) in which B does not depend on x. This type constructor is a variation on Malcolm and Chisolm's so-called "polymorphic function" type constructor, (1989?).