Typability and Type Inference in Atomic Polymorphism

TL;DR

This paper investigates typability and type inference in Curry style variants of a restricted polymorphic system, demonstrating decidability and providing an algorithm for type inference with non-redundancy constraints.

Contribution

It shows that typability is decidable in Curry style variants of system Fat and introduces an algorithm for type inference handling non-redundancy constraints.

Findings

Typability is decidable in Curry style variants of system Fat.

An algorithm for type inference with non-redundancy constraints is proposed.

Type inhabitation remains undecidable in the full system F, but is decidable in the studied fragment.

Abstract

It is well-known that typability, type inhabitation and type inference are undecidable in the Girard-Reynolds polymorphic system F. It has recently been proven that type inhabitation remains undecidable even in the predicative fragment of system F in which all universal instantiations have an atomic witness (system Fat). In this paper we analyze typability and type inference in Curry style variants of system Fat and show that typability is decidable and that there is an algorithm for type inference which is capable of dealing with non-redundancy constraints.