M. Widera and C. Beierle. An Approach to Checking the Non-Disjointness of Types in Functional Programming. Informatik Berichte 281, FernUniversität Hagen, Januar 2001.
This work motivates a new approach to type checking functional programs building a bridge between static typing and soft typing. A type language for this approach can be very precise; e.g. it may contain large and detailed subtyping hierarchies. Furthermore, certain requirements on the type language must be met that differ from usual type definitions. A type language appropriate for the new typing approach is defined in the first part of this work. It turns out that it is a central question for our new type checker to check whether two types denote sets of values that are non-disjoint. Since our type language allows for the occurrence of type variables we are furthermore interested in restricting these variables as much as possible without reducing the set of common elements of two types. The second part of this work specifies an algorithm CE that approximates this question and proves the main properties of CE.
Available: PS, BibTeX