Three comments on the anti-frame rule
François Pottier · 2009
This informal note presents three comments about the antiframe rule, which respectively regard: its interaction with polymorphism; its interaction with the higher-order frame axiom; and a problematic lack of modularity. Interaction between anti-frame and polymorphism It is well-known that a careless combination of parametric polymorphism and weak references is unsound. (A weak reference is one that can be read and written without restrictions, as in ML.) The standard way to work around this problem is to rely on the value restriction [7] that is, to restrict the ∀-introduction rule to values (as opposed to arbitrary terms). Charguéraud and Pottier [3] pointed out that, on the other hand, there is no adverse interaction between polymorphism and strong references. (A strong reference is one that can be read and written only by presenting a linear capability.) As a result, in a typeand-capability