[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