Ashley Yakeley writes:
At 2000-11-24 02:02, Bernd =?iso-8859-2?Q?Holzm=FCller?= wrote:
When I got to know Haskell, I was expecting a construct for union types like:
data B = ... data C = ... type A = B | C | D -- A accepts values of either B or C or D (cf. the "Either a" type in the Prelude)
but this is not valid Haskell. Is there any reason for this restriction in the Haskell type system?
[...]
Does this lead to losing the principal type property?
Yes.
No, not if you update your notion of an instance to reflect the extended type system. [Whether one really wants complete type inference in this setting is another question, though.]
And, if so, would you please give me an example where the principal type does not exist any more when introducing union types in the form above?
Certainly. Consider, in your extended Haskell:
data B = B1 | B2 data C = ... type A = B | C | D -- A accepts values of either B or C or D
Both A and B are types for B1, but neither is a substitution-instance of the other. This violates the principal type property whereby for every term x, either x is not typable or there exists a type T such that every type assignable to x is a substitution-instance of T.
A better question might be, having extended the type system (and indeed the notion of 'type') in this way, how do I need to modify the concept of 'principal type'?
Polymorphic subtyping systems provide an answer to this question. My favourite reference in this field is @techreport{henglein:polysub, AUTHOR = {Henglein, Fritz}, YEAR = {1996}, TITLE = {Syntactic Properties of Polymorphic Subtyping}, INSTITUTION = {DIKU, University of Copenhagen}, type = {TOPPS Technical Report (D-report series)}, number = {D-293}, month = {May} }
Do any papers exist about this topic? Is there any Haskell compiler supporting union types?
You might look at O'Haskell, which I understand has some kind of OOP-style polymorphism. I don't know if it has union types though.
Indeed, O'Haskell is able to express the desired type structure rather directly: data B = B1 | B2 data C = ... data D = ... data A > B, C, D -- A accepts values of either B or C or D. The principal type for B1 is B, reflecting the fact that we can obtain every other valid type for B1 from B using either substitution (not needed here) or subtyping (since only supertypes of B are allowed to contain B1). For more info on O'Haskell, please consult http://www.cs.chalmers.se/~nordland/ohaskell/ -- Johan