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?
My understanding is that every value in Haskell is a member of exactly one type. Well, that's not exactly true: it might be better to say that every Haskell value represents a set of 'items', each of which has exactly one fully-specified type (i.e. a type with no free type-variables). For instance, in such definitions as data Maybe a = Nothing | Just a the value that the constructor 'Nothing' gives has type 'Maybe a', which represents a set of 'items' that have such types as 'Maybe Boolean', 'Maybe String' etc. This rules out union types and OOP-style polymorphism. It also makes it difficult to make arrays of values of mixed type.
Does this lead to losing the principal type property?
Yes.
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'?
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. -- Ashley Yakeley, Seattle WA