search

stedolan / counterexamples

Counterexamples in Type Systems
http://counterexamples.org
372 stars 23 forks source link

Generative functors #4

Open elpinal opened 3 years ago

elpinal commented 3 years ago

First of all, thanks for the great work!

http://counterexamples.org/unstable-types.html

The counterexample by Russo is due to open-scope unpacking of first-class modules and applicative functors. The easiest way to fix the problem is using generative functors. That is, when unpack occurs in the body of a functor F, then it should be generative, meaning that each application of F should yield fresh abstract types. Moscow ML, Alice ML and OCaml take this approach.

If one wants to stick to applicative functors, then we must at least track dependencies of types on values. Moreover, types must be effect-free to make type equivalence reflexive. But this is not the case for existing major implementations: neither Moscow ML nor OCaml prohibits effects inside types (because of functor application!) so unpack is only allowed in generative functors.

Finally, the interaction between first-class modules and effects was briefly discussed by Harper and Lillibridge in 1994 [1], earlier than Russo.

[1] https://doi.org/10.1145/174675.176927

stedolan commented 3 years ago

Thanks for the notes, you're correct and this entry needs some work!

I think this might end up being the same issue as an applicative / generative mixup that occurred in Moscow ML (https://www.seas.upenn.edu/~sweirich/types/archive/1999-2003/msg01136.html)