[TYPES] union types and overloading

[rowan at cs.cmu.edu]

Kwangkeun Yi writes:
 > 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? 

I'd add to this discussion that your example could be slightly
reformulated to use an intersection type:

  accept-both : (t1 -> int) & (t2 -> int)

Alternatively, you can easily replace the definitions of t1 and t2 by
a single type.

 type t = A of int | B of t | C | D of t

But, then you have less precise static checking in those parts of the
code that are specific to t1 or t2.  One way to avoid this loss of
static checking is to use type refinements.  With the implementation
of type refinements for datatypes that I built for my thesis work, you
could write the equivalent of above code in SML using stylized
comments to specify refinements:

 datatype t = A of int | B of t
            | C | D of t

 (*[ datasort t1 = A of int | B of t1
     datasort t2 = C | D of t2 ]*)

 (*[ val accept_both :>  (t1 -> int) 
                       & (t2 -> int) ]*)
 fun accept_both (A n) = n
   | accept_both (B x) = 0
   | accept_both C = 0
   | accept_both (D y) = 0

(We could also specify accept_both :> t -> int.)

Such refinements are particularly aimed at the situation where we have
more expressive specifications like:

   (*[  val f :> (t1 -> t2) & (t2 -> t1)  ]*)
   fun f (A n) = C
     | f (B x) = D (f x)
     | f C = A 0
     | f (D y) = B (f y)

But, I think they do provide one approach for dealing with the
situation that you described.

See the following paper for more details:
    http://www.cs.cmu.edu/~fp/papers/icfp00.pdf

(Or, for many more details, see my dissertation, which will be
complete soon.  And, I'm also planning a public release of the
implementation.)

Cheers

- Rowan