[PRL] local datatypes, generativity, soundness

[Riccardo Pucella]

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. 

For instance, your 'make' function in MLton:

fun make () =
        let datatype t = Foo
        in
            (Foo, fn Foo => ())
        end;

does not compile:

[login at tmp] mlton test.sml 
Error: test.sml 1.1.
  Type escapes the scope of its definition at test.sml 2.22.
    type: t
    in: fun make () = (let datatype t = F  ...   (Foo) => (())) end)
compilation aborted: parseAndElaborate reported errors



----- "David Herman" <dherman at ccs.neu.edu> wrote:

> 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
> _______________________________________________
> PRL mailing list
> PRL at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/prl