[PRL] local datatypes, generativity, soundness

[David Herman]

> In fact, I *believe* that when SML/NJ allows a locally-defined datatype to escape, it is non-generative. As your example shows, all instances of the datatype are equal. That preserves soundness. And it shouldn't be possible to define non-structurally equivalent datatypes by evaluating the same expression.

Yeah, I can't think of an obvious way to break soundness with non-generative local type definitions. That was kind of what brought this topic up for me.

At the same time, is it just me, or does non-generativity just seem wrong somehow? Maybe it's just because of my exposure to the Racket semantics, but generativity seems so much more natural. By analogy to lambda, for example. Then again, when I told my colleague I thought (incorrectly) that SML's local datatypes are generative, he recoiled in horror and said "that must be a bug, right?"

One more question: when we talk about SML's generative functors, we mean something a little different, don't we? I think this was part of what was confusing me. A generative functor produces fresh, incompatible datatypes *statically* at each (compile-time!) application. Whereas a generative local datatype is dynamically generative. Thinking of the latter with existentials really helps me wrap my head around this -- it's still a static type, but because it's hidden within its scope, multiple invocations of the same code are mutually incompatible.

[But then, if you have a language with dynamic linking, like Alice ML, the design space changes, because now the analog to functor application is dynamic. Which at least explains why they made different design decisions, even if I don't understand them all yet.]

Thanks again,
Dave