[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