Union Types for Haskell!?

[Ashley Yakeley]

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