Union Types for Haskell!?

[Bernd Holzmüller]

> Ashley Yakeley wrote:
> 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'?
> ...
> There are two different kinds of 'general' here. Informally, you want the 
> type most general in the type-substitution sense, but probably most 
> specific in the subtype sense.

I think that's the point. It seems that for union types a different
approach for type inference might be used to avoid the problems Fergus
Henderson and others noted. The following typing rule could serve as a
basis for further discussion:

(1) Union types are used in type inference only if necessary to
    successfully type the expression.

In other words, the type checker should try to use the most general type
using parametric polymorphism, but at the same time the *smallest*
possible type regarding the use of union types. That is, there is
usually more than one most general type in case union types are used
with type inference, but there is only one most specific type amongst
those type expressions using union types (which is still equally or more
general than the most general type in a type system without union
types). The following picture illustrates this idea graphically:

   t1 t2 t3    possible types that correctly type e, using union types
     \ | /
      \|/
       t       most specific type of all types for e using union types
       |       (is equally or more general than t0)
       |
  e :: t0      Haskell 98 (principal) type for e (not using union types)

Example 1:
 
> Fergus Henderson wrote:
>
>         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.

Applying the above rule (1) would just give the expected result: f has
type Maybe a -> Bool because from the body of the function there is no
necessity of using a more general type using union types.

Example 2:

>         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]

The type of list must be inferred as Maybe a -> { [b], Integer } because
otherwise the expression would not be typeable. However, the type of the
case body for "case list of ..." should be inferred as [a] -> Maybe a
(which is the most specific and here as well the most general type when
not considering union types) which could not be legally applied to the
list argument, which is of type { [a], Integer }, because it is too
general: it cannot match type [a] for all elements of the union. Thus,
the function is not correctly typed (I assume the quite obvious matching
rules with union types as follows: t1 matches Union t2 t3 if t1 matches
t2 or t1 matches t3 and Union t2 t3 matches t1 if both t2 and t3 match
t1).

> Ashley Yakeley wrote:
>
>  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.

Againg: applying (1) yields B1 :: B (which is the most specific type not
using unions) and *not* B1 :: A.

It seems that the typing rule given by (1) is a compromise of the
proposed explicit style for the use of union types and the flexibility
and accuracy achieved by type inference. 

--
Bernd Holzmüller