Polymorphism with Typed Holes
摘要
Live programming environments aim to provide rapid and continuous feedback to developers, but this can be challenging when a program is incomplete. Hazel is a live programming environment that aims to solve this problem by using expression and type holes to stand for missing terms or mark erroneous terms. Hazel is based on the Hazelnut Live calculus presented in prior work. This paper starts by presenting Polymorphic Hazelnut Live, an extension of Hazelnut Live to support explicit System F-style polymorphism. We show, with mechanized proofs in Agda, that this extended system satisfies the key metatheoretic properties necessary for live programming with typed holes. We compare the type system of Polymorphic Hazelnut Live to other systems that combine gradual typing (i.e. the theory of type holes) with polymorphism, discussing subtleties related to parametricity and the gradual guarantee. Finally, we present a method to integrate a form of implicit type application into the Hazel architecture. We propose a system in which the programmer may omit explicit type applications, and the editor (rather than downstream tools like a typechecker or compiler) implicitly inserts and fills them, allowing the user to see and override these implicit type applications as needed.