Re: [Sml-implementers] Subject: Standard ML

[Stephen W. <sw...@in...>]

> It's not easy, I'm afraid. Consider the following abstype declaration:
> 
> 	abstype t = T with
> 	    val t = T
> 	    val eq = op=
> 	end
> 
> Depending on the context, type inference has to choose between two type
> schemes it can sensibly assign to eq:
> 
> 	sigma1 = ''a * ''a -> bool
> 	sigma2 = t * t -> bool
...

Thanks for all the examples.  They didn't quite convince me that it
would be too hard to implement, since it seems like similar tricks
that one uses to implement overloading would work in them (namely,
delaying a decision about the type of an instantiation until all the
uses are known).  However, the following example does convince me
that this is hard to implement.

(* Elaborates with sigma1 *)
abstype t = T with
   val t = T
   val eq = op=
end
fun f (x, y) = eq (x, y)
val _ = f (1, 2)

(* Reject *)
abstype t = T with
   val t = T
   val eq = op=
end
fun f (x, y) = eq (x, y)
val _ = f (1, 2)
val _ = eq (t, t)

These two examples show that one actually has to make decisions about
generalization before all of the uses are known.  This is worse than
overloading, which only instantiates to monotypes, not type variables.

> So I believe it is very hard to get the semantics of abstype right in a
> compiler - probably even harder than parsing fun-case. IMHO abstype in
> its current form is simply broken. That is another reason why I would
> like to see it removed from the language -- or turned into a derived
> form:
> 
> 	abstype t = conbind with dec end --->
> 		local datatype t = conbind in type t = t dec end
> 
> AFAICS, the only difference with the current definition would be that
> equality of t is transparent - but that is exactly what is required to
> avoid the current problems of non-principality and type structures not
> respecting equality. And it is a conservative change, not breaking any
> legal program (I think).

I agree, and like your solution.