Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Tue 25 Aug 2020 14:30 - 14:45 at ICFP NY 4 - New York 4 Chair(s): Stephanie Weirich
Wed 26 Aug 2020 02:30 - 02:45 at ICFP Asia 4 - Asia 4 Chair(s): Stephanie Weirich

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.

Tue 25 Aug
Times are displayed in time zone: (GMT-04:00) Eastern Time (US & Canada) change

icfp-2020-papers
14:30 - 16:30: ICFP Program - New York 4 at ICFP NY 4
Chair(s): Stephanie WeirichUniversity of Pennsylvania

Public livestreams: YouTube, Bilibili (China)

icfp-2020-papers14:30 - 14:45
Talk
DOI Pre-print Media Attached
icfp-2020-papers14:45 - 15:00
Talk
Tristan KnothUniversity of California at San Diego, USA, Di WangCarnegie Mellon University, Adam ReynoldsUniversity of California, San Diego, Nadia PolikarpovaUniversity of California, San Diego, Jan HoffmannCarnegie Mellon University
DOI
icfp-2020-papers15:00 - 15:15
Talk
Glen MévelInria, Université Paris-Saclay, CNRS, Laboratoire de recherche en informatique, Jacques-Henri JourdanUniversersité Paris Saclay, CNRS, LRI, François PottierInria, France
DOI
icfp-2020-papers15:15 - 15:30
Talk
Matthew WeidnerCarnegie Mellon University, Christopher MeiklejohnCarnegie Mellon University, Heather MillerCarnegie Mellon University
DOI
icfp-2020-papers15:30 - 15:45
Talk
Alejandro Serrano47 Degrees, Spain, Jurriaan HageUtrecht University, Netherlands, Simon Peyton JonesMicrosoft, UK, Dimitrios VytiniotisDeepMind
DOI Pre-print
icfp-2020-papers15:45 - 16:00
Talk
Andreas AbelGothenburg University, Jean-Philippe BernardyUniversity of Gothenburg, Sweden
DOI
icfp-2020-papers16:00 - 16:15
Talk
Sebastian GrafKarlsruhe Institute of Technology, Simon Peyton JonesMicrosoft, UK, Ryan ScottGalois, Inc.
Link to publication DOI
icfp-2020-papers16:15 - 16:30
Talk
Taro SekiyamaNational Institute of Informatics, Takeshi TsukadaChiba University, Japan, Atsushi IgarashiKyoto University, Japan
DOI

Wed 26 Aug
Times are displayed in time zone: (GMT-04:00) Eastern Time (US & Canada) change

icfp-2020-papers
02:30 - 04:30: ICFP Program - Asia 4 at ICFP Asia 4
Chair(s): Stephanie WeirichUniversity of Pennsylvania

Public livestreams: YouTube, Bilibili (China)

icfp-2020-papers02:30 - 02:45
Talk
DOI Pre-print Media Attached
icfp-2020-papers02:45 - 03:00
Talk
Tristan KnothUniversity of California at San Diego, USA, Di WangCarnegie Mellon University, Adam ReynoldsUniversity of California, San Diego, Nadia PolikarpovaUniversity of California, San Diego, Jan HoffmannCarnegie Mellon University
DOI
icfp-2020-papers03:00 - 03:15
Talk
Glen MévelInria, Université Paris-Saclay, CNRS, Laboratoire de recherche en informatique, Jacques-Henri JourdanUniversersité Paris Saclay, CNRS, LRI, François PottierInria, France
DOI
icfp-2020-papers03:15 - 03:30
Talk
Matthew WeidnerCarnegie Mellon University, Christopher MeiklejohnCarnegie Mellon University, Heather MillerCarnegie Mellon University
DOI
icfp-2020-papers03:30 - 03:45
Talk
Alejandro Serrano47 Degrees, Spain, Jurriaan HageUtrecht University, Netherlands, Simon Peyton JonesMicrosoft, UK, Dimitrios VytiniotisDeepMind
DOI Pre-print
icfp-2020-papers03:45 - 04:00
Talk
Andreas AbelGothenburg University, Jean-Philippe BernardyUniversity of Gothenburg, Sweden
DOI
icfp-2020-papers04:00 - 04:15
Talk
Sebastian GrafKarlsruhe Institute of Technology, Simon Peyton JonesMicrosoft, UK, Ryan ScottGalois, Inc.
Link to publication DOI
icfp-2020-papers04:15 - 04:30
Talk
Taro SekiyamaNational Institute of Informatics, Takeshi TsukadaChiba University, Japan, Atsushi IgarashiKyoto University, Japan
DOI