S.M.Kahrs wrote:
let data Bar = ... in ...
If you allow this you need to be very careful about type equality. When is Bar equal to Bar? If it's inside a recursive function, does each invocation get its own Bar? (In SML the answer is yes.)
Not really. In SML the answer used to be a clear "no", that is: in the 1990 definition. However, that proved to be a matter of type-unsoundness, and Claudio Russo came up with an example that used this feature to break the type system. Having said this, this was based on the way the type system was defined in the language definition, the problem did not show up in implementations (which therefore failed to implement the language standard :-).
The problem was fixed in the 1997 language standard. But there the answer isn't "yes" either, it is more like: "whatever it is, you cannot tell", though technically it is still "no".
Mh, technically, isn't it likewise "neither"? As you say, types are only generated statically, and are erased in the dynamic semantics, so how is it a "no" more than a "yes"? As an aside (sorry if this is getting far too OT), in Alice ML we extend SML with dynamic types, and local types in fact *are* dynamically generative. This seemed to be the most natural semantics (and the only correct one in the presence of dynamic linking).
In the static semantics, a local datatype in SML is fresh. However, this freshness is a static freshness, at compile time, and every time the code is run the same "type name" (a uniqueness tag for types) will be used: there is no run time type-checking, the type name is generated once, at compile time.
Well, this is sort of true for types defined in functor bodies as well, still they are generative. The only semantical difference I see is that its local types are allowed to escape scope, and are (statically) renamed upon each application of the functor. No difference with respect to the dynamic semantics, however.
However, that type name is not allowed to leak to the outside, i.e. not only is the identifier Bar not visible outside, the type of the value returned by the let-expression must not contain the type name associated with Bar. Thus, if a let-expression with a local datatype is evaluated twice, it does not really matter whether it uses the same or a different type name because encapsulation ensures that these type names do not interfere with each other in any way.
In a nutshell: local types are not worth the trouble they cause.
I'm not quite sure how this follows from your explanation. :-) Don't you just need the same standard scoping restriction as for existential types? (Which they basically are, as we know.) Why do you consider it troublesome? - Andreas -- Andreas Rossberg, rossberg@ps.uni-sb.de