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, [EMAIL PROTECTED]
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
