Re: [Sml-implementers] Subject: Standard ML

[Andreas R. <ros...@ps...>]

Stephen Weeks wrote:
> 
> > Note 
> > btw. that the reason why "abstype" is actually working in Alice is only
> > due to the fact that the compiler does not distinguish equality types. I
> > guess the same is true for MLton?
> 
> Right (among the hundred or so things that MLton ignores).  I will
> probably go for the overloading solution if/when I ever get around to
> writing a proper front-end.  It doesn't seem too hard.

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

But both exclude each other. Every program that requires both must be
rejected. Here are some examples covering most interesting cases:

(* (1a) Elaborates with sigma1 *)
abstype t = T with
    val t = T
    val eq = op=
end;
eq(2,3);

(* (1b) Elaborates with sigma2 *)
abstype t = T with
    val t = T
    val eq = op=
end;
eq(t,t);

(* (1c) Reject: elaborates with neither *)
abstype t = T with
    val t = T
    val eq = op=
end;
eq(2,3) andalso eq(t,t);

(* (2a) Elaborates with sigma1 *)
abstype t = T with
    val t = T
    val eq = op=
    val _ = eq(t,t)
end;
eq(2,3);

(* (2b) Elaborates with sigma2 *)
abstype t = T with
    val t = T
    val eq = op=
    val _ = eq(t,t)
end;
eq(t,t);

(* (2c) Reject *)
abstype t = T with
    val t = T
    val eq = op=
    val _ = eq(2,3)
end;
eq(t,t);

(* (3a) Elaborates with sigma1 *)
abstype t = T with
    val t = T
    val eq = op=
    val _ = eq(t,t) andalso eq(2,3)
end;
eq(2,3);

(* (3b) Reject *)
abstype t = T with
    val t = T
    val eq = op=
    val _ = eq(t,t) andalso eq(2,3)
end;
eq(t,t);

In most of these examples, when trying standard type inference, we had
to instantiate eq's type scheme before knowing which it is. In
particular, later declarations may invalidate possible typings for the
abstype body (e.g. 2a vs 2b, or 3a vs 3b). Not really obvious how this
could be implemented. And it is reminiscent of the free tyvar problem,
only worse.

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).

	- Andreas