Re: Union Types for Haskell!?

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