Talk: Dominique Devriese, KU Leuven - Generalising Capability Safety to Effect Polymorphism - Fuctional Reasoning in an Object-Oriented World

Static effectful APIs and global state in object-oriented programming languages make it hard to modularly control effects. Object-capability (OC) languages solve this by enforcing that effects can only be triggered by components that hold a reference to the object representing the capability to do so. We study this encapsulation of effects through a formal translation to a typed functional calculus with higher-ranked polymorphism (we use a subset of Haskell for presentation). Based on an informal view of effect-polymorphism as the fundamental feature of OC languages, we translate an OC calculus to effect-polymorphic Haskell code, i.e. computations that are universally quantified over the monad in which they produce effects.

The types of our translations assert the object-capability property and we can show and exploit this using Reynolds' parametrically theorem. This text contains a simple OC calculus, the formal translation to effect-polymorphic Haskell code, proofs that effect parametrically generalizes and strengthens capability-safety, some applications and discussions. An important new insight is that current OC languages and formalization's leave one effect implicitly available: the allocation of new mutable state; adding a capability for it has important theoretical and practical advantages. In summary, we propose effect parametrically (parametrically applied to effect-polymorphic functions) as a formal property that generalizes and strengthens capability-safety. This establishes a new link between object-capability languages and the well-studied fields of functional programming and denotational semantics.

Host: Lars Birkedal