[PRL] local datatypes, generativity, soundness
David Herman
dherman at ccs.neu.edu
Wed Sep 1 23:27:43 EDT 2010
SML/NJ has some notes about local datatype definitions in SML:
http://www.smlnj.org/doc/Conversion/types.html#LocalDT
that suggest that these were the source of some soundness bugs in the past. The whole idea of generative static types is a little brain-twisting -- in Racket, I can easily understand a code snippet like:
(define (make)
(define-struct foo ())
(values (make-foo) foo?))
(define-values (foo1 foo1?) (make))
(define-values (foo2 foo2?) (make))
(foo1? foo2) ;; #f
(foo2? foo1) ;; #f
But I'm not sure what to make of this similar code in SML:
fun make () =
let datatype t = Foo
in
(Foo, fn Foo => ())
end;
val (x, f) = make ();
val (y, g) = make ();
val _ = f y; (* succeeds! *)
val _ = g x; (* succeeds! *)
I *thought* local datatypes were supposed to be generative, even though I don't fully understand what that means. But I wouldn't have expected this code to succeed. Can anyone either shed some light or point to some literature on the topic?
Many thanks!
Dave
More information about the PRL
mailing list