[TYPES] union types and overloading

[Kwangkeun Yi]

Hi Rowan,

Thanks for your information. 

Does your refinement type accept the "accept-both" function as it is?
I'm looking for, if any, simplest solution for the programmers,
where no modification (e.g. rewriting datatypes or adding annotations) is
necessary for such "accept-both" ftn to be type-checked. 
Your "f: (t1 -> t2) & (t2 -> t1)" ftn is quite nice, but I'm willing
to disallow it if the inference algorithm has to ask for a help from
the programmers. 

Best,

-Kwang

On Tue, Oct 05, 2004 at 12:22:09PM -0400, rowan at cs.cmu.edu wrote:
>
> 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
>