Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Journal articles
  4. When Subtyping Constraints Liberate A Novel Type Inference Approach for First-Class Polymorphism
 
research article

When Subtyping Constraints Liberate A Novel Type Inference Approach for First-Class Polymorphism

Parreaux, Lionel
•
Boruch-Gruszecki, Aleksander Slawomir  
•
Fan, Andong
Show more
January 1, 2024
Proceedings Of The Acm On Programming Languages-Pacmpl

Type inference in the presence of first-class or "impredicative" second-order polymorphism a la System F has been an active research area for several decades, with original works dating back to the end of the 80s. Yet, until now many basic problems remain open, such as how to type check expressions like (lambda x. (x 123, x True)) id reliably. We show that a type inference approach based on multi-bounded polymorphism, a form of implicit polymorphic subtyping with multiple lower and upper bounds, can help us resolve most of these problems in a uniquely simple and regular way. We define F-{<=}, a declarative type system derived from the existing theory of implicit coercions by Cretin and Remy (LICS 2014), and we introduce SuperF, a novel algorithm to infer polymorphic multi-bounded F-{<=} types while checking user type annotations written in the syntax of System F. We use a recursion-avoiding heuristic to guarantee termination of type inference at the cost of rejecting some valid programs, which thankfully rarely triggers in practice. We show that SuperF is vastly more powerful than all first-class-polymorphic type inference systems proposed so far, significantly advancing the state of the art in type inference for general-purpose programming languages.

  • Details
  • Metrics
Type
research article
DOI
10.1145/3632890
Web of Science ID

WOS:001170729400049

Author(s)
Parreaux, Lionel
Boruch-Gruszecki, Aleksander Slawomir  
Fan, Andong
Chau, Chun Yin
Date Issued

2024-01-01

Publisher

Assoc Computing Machinery

Published in
Proceedings Of The Acm On Programming Languages-Pacmpl
Volume

8

Issue

POPL

Start page

48

Subjects

Technology

•

Type Inference

•

First-Class Polymorphism

•

Subtyping

•

Constraint Solving

Editorial or Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
LAMP1  
FunderGrant Number

Hong Kong Research Grant Council

26208821

Available on Infoscience
June 5, 2024
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/208246
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés