[PRL] local datatypes, generativity, soundness
David Herman
dherman at ccs.neu.edu
Thu Sep 2 01:05:56 EDT 2010
> SML/NJ does not actually implement SML'97 in this respect.
>
> The 97 Standard forbids the definition of locally-defined datatypes to escape the lexical scope.
I see. Interesting.
So if they could escape, and if they were actually generative, would that basically be like an existential type? IOW, something like:
let datatype foo = Foo of (int, bool) in Foo (1, true) end
would be roughly like:
let datatype foo = Foo of (int, bool)
in
pack foo as X in Foo (1, true)
end
which would type as:
exists X . X
?
Thanks,
Dave
More information about the PRL
mailing list