Union Types for Haskell!?
Johan Nordlander
nordland@cse.ogi.edu
Fri, 24 Nov 2000 22:32:10 -0800
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