Re: Union Types for Haskell!?

Fergus Henderson <fjh@xxxxxxxxxxx> writes:

[...]
>       (2) Allow pattern matching on values of particular types,
>           using `case'.
[...]
> If we allow (2), then some programming mistakes that previously
> were type errors would instead become just inexhaustive pattern
> matches for which you get a run-time error.
> 
> For example:
> 
>       foo :: Maybe a -> b -> Maybe b
>       foo x y = case list of
>                       [] -> Nothing
>                       (x:xs) -> Just x
>               where list = case x of
>                       Nothing -> 0    -- oops, meant [] instead of 0
>                       Just foo -> [y]
>                               
> If union types were allowed, with (2) above, this example would be
> legal, with `list' having the union type { [a], Integer }.

if you disallow undeclared union types, you'll catch easily this kind of errors.

> But `foo Nothing 42' would evaluate to bottom, since the `case list'
> expression has no case with a pattern of type Integer.
> 
> So allowing union types in this way would reduce static type safety,
> at least unless we also forbid inexhaustive pattern matches.

well allowing inexhaustive pattern matching always leads to less type
safetyness, no news :)

And of course subtyping also reduce type safetyness. 
But it is the same for type classes. No one is more safe than using '+' for
integers and '+.' for floats...

> 
> If instead you only allow (1), then probably union types would
> not be suitable for expressing the kinds of things that you want
> to express with them.

sure, you don't win anything.

> 
> > Is there any reason for this restriction
> > in the Haskell type system? Does this lead to losing the principal type
> > property?
> 
> If you allow (2) above, there may be serious problems for
> principal types.  For example, consider
> 
>       f x = case x of
>               Nothing -> False
>               Just _ -> True
> 
> What's the most general type for `f'?
> The type `f :: Maybe a -> Bool' is less general than
> e.g. `f :: Union { Maybe a, ... } -> Bool',
> but you certainly don't want to infer the latter type.

not necessarily. 
If you disallow undeclared union types, the only occurence of Union { Maybe a,
... } will be Maybe a, unless one really wants to extend Maybe...


cu Pixel.