[TYPES] union types and overloading

[Johan Nordlander]

Hi Kwang,

You might be interested in taking a look at the subtyping system of 
O'Haskell (http://www.cs.chalmers.se/~nordland/ohaskell/).  This system 
provides nominal subtyping via type extension for datatypes as well as 
records, together with a type inference algorithm that trades 
simplicity over completeness (i.e., it actually solves all inferred 
subtyping constraints before let-generalization, even when this leads 
to loss of information).

Your example translates rather directly into O'Haskell syntax as 
follows:

data T1 = A Int | B T1
data T2 = C | D T2

data Both > T1, T2

accept_both (A n) = n
accept_both (B x) = 0
accept_both C     = 0
accept_both (D y) = 0

The inferred type for accept_both is Both -> Int.  By subtyping this 
can be coerced to T1 -> Int as well as T2 -> Int.

Note that the declaration of type Both is necessary in this system.  
Note also that the argument to constructor B is still of type T1, even 
when B is considered a constructor of type Both.

All the best,
Johan


> Hi there,
>
> I would like to extend our ML compiler's type system so that it allow
> functions to be defined over the sum of multiple datatypes. (union 
> types?)
>
> E.g.,
>
> type t1 = A of int | B of t1
> type t2 = C | D of t2
>
> (* accept-both : t1+t2 -> int *)
> fun accept-both (A n) = n
>   | accept-both (B x) = 0
>   | accept-both C = 0
>   | accept-both (D y) = 0
>
> Could you point me to some papers that I have to check out to avoid
> reinvention or to expect possible obstacles?
>
> Thank you,
>
> -Kwang
>
> --
> Kwangkeun Yi		http://ropas.snu.ac.kr/~kwang
>