Logo image
Back
Spine-local Type Inference
Conference proceeding   Open access

Spine-local Type Inference

Christopher Jenkins and Aaron Stump
Proceedings of the 30th Symposium on implementation and application of functional languages, pp.37-48
IFL 2018
09/05/2018
DOI: 10.1145/3310232.3310233
url
https://doi.org/10.1145/3310232.3310233View
Published (Version of record) Open Access

Abstract

We present spine-local type inference, a method of partially inferring omitted type annotations for System F based on local type inference. Local type inference relies on bidirectional rules to propagate type information into and out of adjacent nodes of the AST and restricts type-argument inference to a single node. Spine-local inference relaxes this restriction, 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 better supports desirable features such as first-class curried applications and partial type applications, and it has 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 advantages of local type inference such as a relatively simple implementation and a tendency to produce good-quality error messages when type inference fails.
 bidirectional typechecking polymorphism type errors

Details

Metrics

16 Record Views
6 Times Cited - Web of Science
Logo image