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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Polymorphism with Typed Holes

  • Adam Chen,
  • Thomas Porter,
  • Cyrus Omar

摘要

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.