Re: [Sml-implementers] Structure sharing and type abbreviations

[Derek R. D. <dr...@cs...>]

Dave Berry wrote:
>
> >2. Datatype's cannot be made transparent with seriously changing the
> >language.
> 
> By transparent, do you mean that the representation of a datatype should be
> deducible from any type that it matches?  Or. to use another example, that
> this snippet shouldn't elaborate:
>           struct
>            datatype 'a foo = Foo of 'a * 'a
>            type t = 'a * 'a
>         sig
>            type t
>             datatype 'a foo = Foo of t
>          end

To clarify: the transparent interpretation of datatypes is one in which datatype
specifications expose the implementation of a datatype as a recursive sum type. 
In the opaque interpretation (i.e. the Definition), the recursive sum type is
never exposed.  The motivation for the transparent interpretation is that, in a
type-directed compiler, it is difficult to inline datatype constructors and
destructors if the implementation of the datatype is not exposed.  In addition,
it would seem that the transparent interpretation allows more type equations to
hold, so it would appear to be more permissive than the Definition.

But in fact, there are cases where the transparent interpretation is not as
permissive as the Definition.  For instance, if you take what I think your
example above is supposed to be, and you change the definition of type 'a t to
type 'a t = 'a * 'a foo
then the structure matches the signature under the opaque interpretation (i.e.
the Definition), but not under the transparent interpretation.  As it stands,
your example appears to be fine under both the transparent and opaque
interpretations of datatypes.  An analysis of the "permissiveness gap" is given
in a TR by Crary et al. from 1998, available at the following URL:

http://www.cs.cmu.edu/~crary/papers/1998/datatype/datatype.ps.gz

> Isn't this what O'Caml implements?  If so, how do they avoid the problems
> you encountered? I'm interested to read that you've changed your mind about
> this.  Have you written up your experiences in more detail?

I'm pretty sure O'Caml also has an opaque interpretation of datatypes.  As I
said, the problems with implementing the opaque interpretation efficiently come
up in the type-directed setting, not in ordinary compilation.  We have a new way
of dealing with the opaque interpretation in TILT that clears up these
problems.  We are in the process of writing up a new TR with more compelling
examples of the "permissiveness gap" between the opaque and transparent
interpretations and with a description of our approach to implementing the
opaque interpretation in a type-directed compiler.  Stay tuned.

Derek