A quick look at impredicativity

Alejandro Serrano; Jurriaan Hage; Simon Peyton Jones; Dimitrios Vytiniotis

doi:10.1145/3408971

A quick look at impredicativity

Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, Dimitrios Vytiniotis

Research output: Contribution to journal › Article › peer-review

14 Citations (Scopus)

63 Downloads (Pure)

Abstract

Type inference for parametric polymorphism is wildly successful, but has always suffered from an embarrassing flaw: polymorphic types are themselves not first class. We present Quick Look, a practical, implemented, and deployable design for impredicative type inference. To demonstrate our claims, we have modified GHC, a production-quality Haskell compiler, to support impredicativity. The changes required are modest, localised, and are fully compatible with GHC's myriad other type system extensions.

Original language	English
Article number	89
Journal	Proceedings of the ACM on Programming Languages
Volume	4
Issue number	ICFP
DOIs	https://doi.org/10.1145/3408971
Publication status	Published - 2 Aug 2020

Keywords

constraint-based inference
impredicative polymorphism
Type systems

Access to Document

10.1145/3408971Licence: CC BY

Download pdf
Copyright © 2020 Owner/Author
Final published version, 368 KBLicence: CC BY

Cite this

@article{6e30f1ff4f484a26a9b63acdfd2b0e96,

title = "A quick look at impredicativity",

abstract = "Type inference for parametric polymorphism is wildly successful, but has always suffered from an embarrassing flaw: polymorphic types are themselves not first class. We present Quick Look, a practical, implemented, and deployable design for impredicative type inference. To demonstrate our claims, we have modified GHC, a production-quality Haskell compiler, to support impredicativity. The changes required are modest, localised, and are fully compatible with GHC's myriad other type system extensions.",

keywords = "constraint-based inference, impredicative polymorphism, Type systems",

author = "Alejandro Serrano and Jurriaan Hage and {Peyton Jones}, Simon and Dimitrios Vytiniotis",

year = "2020",

month = aug,

day = "2",

doi = "10.1145/3408971",

language = "English",

volume = "4",

journal = "Proceedings of the ACM on Programming Languages",

issn = "2475-1421",

publisher = "Association for Computing Machinery",

number = "ICFP",

}

TY - JOUR

T1 - A quick look at impredicativity

AU - Serrano, Alejandro

AU - Hage, Jurriaan

AU - Peyton Jones, Simon

AU - Vytiniotis, Dimitrios

PY - 2020/8/2

Y1 - 2020/8/2

N2 - Type inference for parametric polymorphism is wildly successful, but has always suffered from an embarrassing flaw: polymorphic types are themselves not first class. We present Quick Look, a practical, implemented, and deployable design for impredicative type inference. To demonstrate our claims, we have modified GHC, a production-quality Haskell compiler, to support impredicativity. The changes required are modest, localised, and are fully compatible with GHC's myriad other type system extensions.

AB - Type inference for parametric polymorphism is wildly successful, but has always suffered from an embarrassing flaw: polymorphic types are themselves not first class. We present Quick Look, a practical, implemented, and deployable design for impredicative type inference. To demonstrate our claims, we have modified GHC, a production-quality Haskell compiler, to support impredicativity. The changes required are modest, localised, and are fully compatible with GHC's myriad other type system extensions.

KW - constraint-based inference

KW - impredicative polymorphism

KW - Type systems

U2 - 10.1145/3408971

DO - 10.1145/3408971

M3 - Article

SN - 2475-1421

VL - 4

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

IS - ICFP

M1 - 89

ER -

A quick look at impredicativity

Abstract

Keywords

Access to Document

Fingerprint

Cite this