Ohad Kammar: A denotational semantics for Hindley-Milner polymorphism

A denotational semantics for Hindley-Milner polymorphism

Abstract: Hindley-Milner let-polymorphism in the presence of computational effects, notably local state mixed with type recursion, requires restriction to achieve type soundness. Existing solutions either restrict generalisation over type variables, excluding opportunities for sound polymorphism, or use types that expose the effectful nature of the implementation. Our goal is to analyse the problem and existing solutions denotationally, with the hope that such models will provide new insights.

We present an intrinsically-typed (Church-style) zeroth-order calculus of let-polymorphism. We define a fibrational denotational semantics to the pure calculus, drawing on ideas from models of the polymorphic lambda calculus, modifying Seeley's PL categories to use Ulmer's relative adjunctions. We extend the pure semantics to include higher-order functions and effects. The resulting calculus does not require a value restriction. We conclude by speculating how to use this model to analyse the existing value restrictions and other solutions.

Joint work with Sean Moss.