[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.
> 
> I see. Interesting.

In fact, I *believe* that when SML/NJ allows a locally-defined datatype to escape, it is non-generative. As your example shows, all instances of the datatype are equal. That preserves soundness. And it shouldn't be possible to define non-structurally equivalent datatypes by evaluating the same expression. (Like you could if you had dependent types, say) -- e.g., the following pretty obviously fails to type check:

fun make (i) =                                                                  
   if (i>0) then                                                                
     let datatype t = Foo                                                       
     in                                                                         
         (Foo, fn Foo => ())                                                    
     end                                                                        
   else                                                                         
     let datatype t = Bar                                                       
     in                                                                         
         (Bar, fn Bar => ())                                                    
     end;                                                                       



> 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
> 
> ?

At some level, yes, it would be similar. The return type of your expression generally would get something like '?.foo' (a terrible name, really), where you can think of the ? as an existentially quantified name for the "instance" of the function that created the type. And you encounter exactly the same restrictions that the values of that type are useless unless you also pack in the return value of whatever expression creates them some operations that can work on values of the type.

 Cheers,
 R