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

  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

  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


-- Johan