Spine-local Type Inference

TL;DR

This paper introduces spine-local type inference, a novel system for inferring omitted type annotations in System F, enhancing local inference with contextual capabilities and supporting advanced features like first-class curried applications.

Contribution

It proposes spine-local type inference, relaxing previous restrictions and enabling inference in more complex term structures, with a formal specification and practical benefits.

Findings

Supports first-class curried applications

Enables inference for previously untypable terms

Maintains predictable annotation requirements

Abstract

We present spine-local type inference, a partial type inference system for inferring omitted type annotations for System F terms based on local type inference. Local type inference relies on bidirectional inference rules to propagate type information into and out of adjacent nodes of the AST and restricts type-argument inference to occur only within a single node. Spine-local inference relaxes the restriction on type-argument inference by allowing it to occur only within an {application spine and improves upon it by using contextual type-argument inference. As our goal is to explore the design space of local type inference, we show that, relative to other variants, spine-local type inference enables desirable features such as first-class curried applications, partial type applications, and the ability to infer types for some terms not otherwise possible. Our approach enjoys usual properties of a bidirectional system of having a specification for our inference algorithm and predictable requirements for typing annotations, and in particular maintains some the advantages of local type inference such as a relatively simple implementation and a tendency to produce good-quality error messages when type inference fails.