Simple Types for Polymorphic Functions

TL;DR

This paper presents a straightforward type system for combinatory logic that captures polymorphism through application, supporting advanced type inference without quantified types, and aims to facilitate static analysis.

Contribution

It introduces a simple, effective type system for combinatory logic that extends polymorphism beyond traditional systems like Hindley-Milner, with an accompanying inference algorithm.

Findings

Supports polymorphism beyond Hindley-Milner

Provides an effective type inference algorithm

Simplifies static program analysis

Abstract

This paper introduces a simple type system for combinatory logic in which combinators have at most one type, whose polymorphism is revealed by application. The combinatory types exactly describe the structure of their values, which may be hidden by abstract types, such as list types and function types. Even without any quantified types, it supports polymorphism beyond that of the Hindley-Milner type system that underpins functional programming, and an effective type inference algorithm. Also, the simplicity of the formalism should make other static program analyses easier.