pith. sign in

arxiv: 2604.12194 · v1 · submitted 2026-04-14 · 💻 cs.LO

Simple Types for Polymorphic Functions

Barry Jay , Johannes Bader This is my paper

Pith reviewed 2026-05-10 16:19 UTC · model grok-4.3

classification 💻 cs.LO
keywords type systemscombinatory logicpolymorphismtype inferenceHindley-Milnerfunctional programmingabstract types
0
0 comments X

The pith

Combinators each get one type whose polymorphism is revealed by application, supporting more than Hindley-Milner without quantified types.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces a type system for combinatory logic in which each combinator is assigned at most one type. Polymorphism is not written with quantifiers but appears when the combinator is applied to different arguments, exposing the behaviors the single type permits. This setup types functions that go past the Hindley-Milner system while still supplying an effective inference algorithm. The types describe the concrete structure of values even when that structure is concealed by abstract types such as lists or functions. The resulting simplicity is presented as helpful for other kinds of static program analysis.

Core claim

The type system assigns each combinator a single type that exactly describes the structure of its values. Abstract types such as list types and function types can hide this structure, but application reveals the polymorphic capabilities. Without using any quantified types, the system achieves polymorphism that surpasses the Hindley-Milner type system used in functional programming, and it comes with an effective type inference algorithm.

What carries the argument

Combinatory types that assign at most one type to each combinator and expose polymorphism through application.

Load-bearing premise

That assigning at most one type to each combinator is enough to capture and infer all the polymorphic behaviors needed for practical functional programming without quantified types or other extra mechanisms.

What would settle it

A concrete polymorphic combinator or program that the type inference algorithm cannot assign a single consistent type to, even though the program type-checks in Hindley-Milner or requires behaviors that a single type cannot cover.

Figures

Figures reproduced from arXiv: 2604.12194 by Barry Jay, Johannes Bader.

Figure 1
Figure 1. Figure 1: Subtyping Γ ⊢ S : S0 Γ ⊢ M : U → V Γ ⊢ N : U Γ ⊢ MN : V Γ ⊢ K : K0 Γ ⊢ x : T x : τ ∈ Γ and τ ≺ T Γ ⊢ t : T Γ ⊢ t : T ′ T < T′ Γ ⊢ u : U x : Cl{Γ, U}, Γ ⊢ t : T Γ ⊢ let x = u in t : T [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Type Derivation for Hybrid Terms yields the expected type of the identity SKK. The type derivation rules are given in [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Type Derivation for Combinators function, here defined by S0(U) = S1U S1U(V ) = S2UV S2T1T2(U) = T1(U)(T2(U)) K0(U) = K1U K1U(V ) = U . The rules for applying S2 and K1 reflect the reduction rules for S and K. The other rules are structural. At a glance, type application may appear to be a total function, but the recursive call in S2T1T2(U) will terminate only if the corresponding reduction does. For examp… view at source ↗
Figure 4
Figure 4. Figure 4: Type Derivation for Terms Later, this application will be reserved for producing abstract types. When term variables are admitted, then type derivation requires a context. Define a term context Γ to be a list of type assignments x : T of types T to variables x in the usual way. We may write x : T ∈ Γ if x : T is in Γ. The corresponding type derivation rules are given in [PITH_FULL_IMAGE:figures/full_fig_p… view at source ↗
Figure 5
Figure 5. Figure 5: The Summary Type System 18 [PITH_FULL_IMAGE:figures/full_fig_p018_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Type Inference Cases for Combinatory Types in OCaml [PITH_FULL_IMAGE:figures/full_fig_p019_6.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 3 minor

Summary. The paper introduces a simple type system for combinatory logic in which each combinator receives at most one simple type (with type variables but no explicit quantifiers). Polymorphism arises exclusively through the application rule. The system is claimed to support polymorphism beyond Hindley-Milner, to admit an effective type-inference algorithm, and to simplify other static analyses because of its reduced formalism.

Significance. If the central results hold, the work supplies a streamlined alternative to quantified polymorphic type systems for combinatory logic. The demonstration that the type rules, inference algorithm and examples are internally consistent, that the system is expressively equivalent to a fragment of Hindley-Milner, and that the inference procedure is terminating and produces principal types constitute concrete strengths that support the practicality of the approach.

major comments (1)
  1. Abstract and §1: the assertion that the system supports 'polymorphism beyond that of the Hindley-Milner type system' sits in tension with the later claim (and proof sketch) of equivalence to a fragment of HM; the precise sense in which the new system is 'beyond' HM should be stated explicitly, e.g., by exhibiting a combinator whose principal type in the new system cannot be expressed in HM without additional mechanisms.
minor comments (3)
  1. §2.1, notation for type variables: the paper uses both Greek letters and Latin letters for type variables without a uniform convention; a single notational choice would improve readability.
  2. Figure 1 (type rules): the application rule is presented without an accompanying prose explanation of how the substitution is computed; a short paragraph clarifying the side condition would help readers unfamiliar with combinatory logic.
  3. §4, inference algorithm: the termination argument is sketched but not given a formal lemma number; numbering the key lemmas would make cross-references easier.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the detailed and constructive report. The single major comment identifies a genuine point of potential confusion in our presentation of the relationship to Hindley-Milner, which we will resolve by tightening the wording and adding a concrete example.

read point-by-point responses

  1. Referee: Abstract and §1: the assertion that the system supports 'polymorphism beyond that of the Hindley-Milner type system' sits in tension with the later claim (and proof sketch) of equivalence to a fragment of HM; the precise sense in which the new system is 'beyond' HM should be stated explicitly, e.g., by exhibiting a combinator whose principal type in the new system cannot be expressed in HM without additional mechanisms.

    Authors: We agree that the current phrasing risks appearing contradictory and will revise both the abstract and §1. The system is expressively equivalent to a fragment of HM (as shown by the embedding and the principal-type theorem), but differs in mechanism: each combinator is given a single simple type possibly containing free type variables, and polymorphism is obtained solely by the application rule rather than by explicit universal quantifiers. This yields a strictly simpler formalism (no quantifiers, no type schemes) while still typing the same combinatory terms as the corresponding HM fragment. The sense in which the approach is 'beyond' HM is therefore that it realises the same polymorphism without quantified types or type schemes. In the revision we will add a short example (the S combinator) whose principal type in our system is a simple type with free variables; we will show that the corresponding HM type requires a quantifier and cannot be written as a simple type without additional mechanisms such as type schemes or implicit quantification. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained

full rationale

The paper presents original type rules for combinatory logic in which each combinator receives a single simple type (with type variables) and polymorphism arises solely from the application rule. These rules, the associated inference algorithm, and the claimed expressiveness results are defined directly from first principles without reducing to fitted parameters, self-referential definitions, or load-bearing self-citations. No step equates a derived result to its own input by construction, and the formalism is shown to be internally consistent on the presented terms.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Only the abstract is available; no free parameters, axioms, or invented entities are identifiable from the given text.

pith-pipeline@v0.9.0 · 5365 in / 1032 out tokens · 50304 ms · 2026-05-10T16:19:42.266923+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

21 extracted references · 21 canonical work pages

  1. [1]

    Abramsky and C.L

    S. Abramsky and C.L. Hankin, editors.Abstract Interpretation of Declarative Languages. Computers and their Applications. Ellis Horwood, 1987

    work page 1987

  2. [2]

    librosa/librosa: 0.6.3,

    Johannes Bader. Combinatory types.https://doi.org/10.5281/zenodo. 15338381

    work page doi:10.5281/zenodo

  3. [3]

    Cambridge University Press, 2013

    Hendrik Pieter Barendregt, Wil Dekkers, and Richard Statman.Lambda calculus with types. Cambridge University Press, 2013

    work page 2013

  4. [4]

    Coppo, M

    M. Coppo, M. Dezani, and B. Venneri. Principal type schemes andλ-calculus semantics. In R. Hindley and J. Seldin, editors,To H.B. Curry: essays in Combi- narory Logic, lambda calculus and Formalisms. Academic Press, 1980. 23

    work page 1980

  5. [5]

    North- Holland Amsterdam, 1972

    Haskell Brooks Curry, Robert Feys, and William Craig.Combinatory Logic. North- Holland Amsterdam, 1972

    work page 1972

  6. [6]

    InProceedings of the 9th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages(Albuquerque, New Mexico)(POPL ’82)

    Luis Damas and Robin Milner. Principal type-schemes for functional programs. InProceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’82, page 207–212, New York, NY, USA, 1982. As- sociation for Computing Machinery.https://doi.org/10.1145/582153.582176

    work page doi:10.1145/582153.582176 1982

  7. [7]

    Refinement types for ml

    Tim Freeman and Frank Pfenning. Refinement types for ml. InProceedings of the ACM SIGPLAN 1991 conference on Programming language design and imple- mentation, pages 268–277, 1991

    work page 1991

  8. [8]

    Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types

    Alain Frisch, Giuseppe Castagna, and V´ eronique Benzaken. Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types. Journal of the ACM (JACM), 55(4):1–64, 2008

    work page 2008

  9. [9]

    Girard, Y

    J-Y. Girard, Y. Lafont, and P. Taylor.Proofs and Types. Tracts in Theoretical Computer Science. Cambridge University Press, 1989

    work page 1989

  10. [10]

    A type-theoretic approach to higher-order modules with sharing

    Robert Harper and Mark Lillibridge. A type-theoretic approach to higher-order modules with sharing. InProceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’94, page 123–137, New York, NY, USA, 1994. Association for Computing Machinery.https: //doi.org/10.1145/174675.176927

    work page doi:10.1145/174675.176927 1994

  11. [11]

    Recursive programs in normal form (short paper)

    Barry Jay. Recursive programs in normal form (short paper). InProceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM ’18, pages 67–73. ACM, 2018

    work page 2018

  12. [12]

    Barry Jay.Reflective Programs in Tree Calculus. 2021. including an ap- pendix with Jose Vergara. URL:https://github.com/barry-jay-personal/ tree-calculus

    work page 2021

  13. [13]

    Combinatory types: repository of proofs in Rocq, 2025

    Barry Jay. Combinatory types: repository of proofs in Rocq, 2025. URL:https: //github.com/barry-jay-personal/combinatory-types

    work page 2025

  14. [14]

    Typed program analysis without encodings

    Barry Jay. Typed program analysis without encodings. InProceedings of the 2025 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation, PEPM ’25, page 54–65, New York, NY, USA, 2025. Association for Computing Machinery.https://doi.org/10.1145/3704253.3706138

    work page doi:10.1145/3704253.3706138 2025

  15. [15]

    R. Milner. A theory of type polymorphism in programming.Journal of Computer and Systems Sciences, 17:348–375, 1978

    work page 1978

  16. [16]

    The octagon abstract domain.Higher-order and symbolic compu- tation, 19:31–100, 2006

    Antoine Min´ e. The octagon abstract domain.Higher-order and symbolic compu- tation, 19:31–100, 2006. 24

    work page 2006

  17. [17]

    Liquid types

    Patrick M Rondon, Ming Kawaguci, and Ranjit Jhala. Liquid types. InProceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 159–169, 2008

    work page 2008

  18. [18]

    Moses Sch¨ onfinkel.¨Uber die bausteine der mathematischen logik.Mathematische Annalen, 92:305–316, 1924

    work page 1924

  19. [19]

    ACM Program

    Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, and Dimitrios Vytiniotis. A quick look at impredicativity.Proc. ACM Program. Lang., 4(ICFP), August 2020.https://doi.org/10.1145/3408971

    work page doi:10.1145/3408971 2020

  20. [20]

    Svf: interprocedural static value-flow analysis in llvm

    Yulei Sui and Jingling Xue. Svf: interprocedural static value-flow analysis in llvm. InProceedings of the 25th international conference on compiler construction, pages 265–266, 2016

    work page 2016

  21. [21]

    J B. Wells. Typability and type checking in the second-orderλ-calculus are equiv- alent and undecidable. InProceedings, Ninth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1994. 25

    work page 1994