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. Conferences, Workshops, Symposiums, and Seminars
  4. The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy
 
conference paper

The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy

Parreaux, Lionel  
2020
Proceedings of the ACM on Programming Languages
25th ACM SIGPLAN International Conference on Functional Programming - ICFP 2020

MLsub extends traditional Hindley-Milner type inference with subtyping while preserving compact principal types, an exciting new development. However, its specification in terms of biunification is difficult to understand, relying on the new concepts of bisubstitution and polar types, and making use of advanced notions from abstract algebra. In this paper, we show that these are in fact not essential to understanding the mechanisms at play in MLsub. We propose an alternative algorithm called Simple-sub, which can be implemented efficiently in under 500 lines of code (including parsing, simplification, and pretty-printing), looks more familiar, and is easier to understand. We present an experimental evaluation of Simple-sub against MLsub on a million randomly-generated well-scoped expressions, showing that the two systems agree. The mutable automaton-based implementation of MLsub is quite far from its algebraic specification, leaving a lot of space for errors; in fact, our evaluation uncovered several bugs in it. We sketch more straightforward soundness and completeness arguments for Simple-sub, based on a syntactic specification of the type system. This paper is meant to be light in formalism, rich in insights, and easy to consume for prospective designers of new type systems and programming languages. In particular, no abstract algebra is inflicted on readers.

  • Files
  • Details
  • Metrics
Type
conference paper
DOI
10.1145/3409006
Author(s)
Parreaux, Lionel  
Date Issued

2020

Published in
Proceedings of the ACM on Programming Languages
Volume

4

Start page

124

End page

124:29

Subjects

type inference

•

subtyping

•

principal types

URL

Associated Github repository

https://icfp20.sigplan.org/details/icfp-2020-papers/37/The-Simple-Essence-of-Algebraic-Subtyping-Functional-Pearl-
https://github.com/LPTK/simple-sub
Editorial or Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
DATA  
Event nameEvent placeEvent date
25th ACM SIGPLAN International Conference on Functional Programming - ICFP 2020

[Online event]

August 24-26, 2020

Available on Infoscience
July 11, 2020
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/169994
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