Re: [Sml-implementers] Subject: Standard ML

[Dave B. <da...@ta...>]

At 18:51 08/10/2001, Andreas Rossberg wrote:
> 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).

It doesn't break any legal program, but it could break a library, and also
render books obsolete.  One use (arguably the only remaining use) of
abstype in the full language is precisely to remove the equality attribute
of a type.  If a library author has made use of this property, then removal
of the property would make that implementation unsound (even though it
would still compile).

IMO it would be preferable to settle on the existing behaviour of most
compilers.  Ideally we should replace the rule in the Definition with one
that doesn't have this flaw, but if that isn't possible then we should just
document this as a problem in the Definition and explain how compilers
should behave in practice.

I don't know if a formal specification is practical.  One approach might be
to reintroduce the notion of principal environments purely for the body of
abstypes.  But that might be too restrictive (and it could possibly break
existing code). 

Dave.