[PRL] local datatypes, generativity, soundness

[Vasileios Koutavas]

A related paper is "Non-Parametric Parametricity" by Georg Neis, Derek Dreyer, and Andreas Rossberg.

http://www.mpi-sws.org/~dreyer/papers/npp/jfp.pdf

They study the use of generative types to achieve type abstraction in the presence of intentional type analysis (e.g. typecast). This is generally believed to be sound, although it has not been formally proven.

Best,
--Vassilis



On 2 Sep 2010, at 18:50, David Herman wrote:

> Thanks for the reference. For anyone interested, the paper is here:
> 
>    http://www.cs.kent.ac.uk/pubs/1993/569/
> 
> with addenda from several years later here:
> 
>    http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.2523
> 
> and Andreas Rossberg has a similar tech report on flaws in the Revised Definition:
> 
>    http://www.mpi-sws.org/~rossberg/papers/Rossberg%20-%20Defects%20in%20the%20Revised%20Definition%20of%20Standard%20ML%20%5B2007-01-22%20Update%5D.pdf
> 
> Thanks,
> Dave
> 
> On Sep 2, 2010, at 9:42 AM, Matthias Felleisen wrote:
> 
>> 
>> There is a tech rpt out of Edinburgh on 101 safety flaws in SML (v1). The generative datatype and escaping local types is one big chapter in there. 
>> 
>> There is also Bob's chapter and papers on applicative vs generative functors, which explain why the latter are (usually) the right solution. Dreyer has some objections to generative functors all the time. I don't think that static functor generativity differs from the one for datatype. 
>> 
>> Riccardo has explained most of the rest. 
>> 
>> -- Matthias
>> 
>> 
>> 
>> 
>> 
>> On Sep 2, 2010, at 9:12 AM, David Herman wrote:
>> 
>>>> 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.
>>> 
>>> Yeah, I can't think of an obvious way to break soundness with non-generative local type definitions. That was kind of what brought this topic up for me.
>>> 
>>> At the same time, is it just me, or does non-generativity just seem wrong somehow? Maybe it's just because of my exposure to the Racket semantics, but generativity seems so much more natural. By analogy to lambda, for example. Then again, when I told my colleague I thought (incorrectly) that SML's local datatypes are generative, he recoiled in horror and said "that must be a bug, right?"
>>> 
>>> One more question: when we talk about SML's generative functors, we mean something a little different, don't we? I think this was part of what was confusing me. A generative functor produces fresh, incompatible datatypes *statically* at each (compile-time!) application. Whereas a generative local datatype is dynamically generative. Thinking of the latter with existentials really helps me wrap my head around this -- it's still a static type, but because it's hidden within its scope, multiple invocations of the same code are mutually incompatible.
>>> 
>>> [But then, if you have a language with dynamic linking, like Alice ML, the design space changes, because now the analog to functor application is dynamic. Which at least explains why they made different design decisions, even if I don't understand them all yet.]
>>> 
>>> Thanks again,
>>> Dave
>>> 
>>> 
>>> _______________________________________________
>>> PRL mailing list
>>> PRL at lists.ccs.neu.edu
>>> https://lists.ccs.neu.edu/bin/listinfo/prl
>> 
> 
> 
> _______________________________________________
> PRL mailing list
> PRL at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/prl