ICFP 2022
Sun 11 - Fri 16 September 2022 Ljubljana, Slovenia
Fri 16 Sep 2022 11:30 - 12:00 at Kosovel - Compiler and Extensions Chair(s): Marco Vassena

Type constructors in functional programming languages are total: a Haskell programmer can equally readily construct lists of any element type. In practice, however, not all applications of type constructors are equally sensible: collections may only make sense for orderable elements, or embedded DSLs might only make sense for serializable return types. Jones et al. proposed a theory of \emph{partial type constructors}, which guarantees that type applications are sensible, and extends higher-order abstractions to apply equally well to partial and total type constructors. This paper evaluates the practicality of partial type constructors, in terms of both language design and implementation. We extend GHC, the most widely used Haskell compiler, with partial type constructors, and use our extended compiler on a significant sample of Haskell code, including the compiler itself, widely-used Hackage packages, and existing examples of partiality in type constructors. We show that introducing partial type constructors has a minimal impact on most code, but raises important questions in language and library design.

Fri 16 Sep

Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change

11:00 - 12:30
Compiler and ExtensionsHaskell at Kosovel
Chair(s): Marco Vassena Utrecht University
11:00
30m
Talk
Investigating Magic Numbers: Improving the Inlining Heuristic in the Glasgow Haskell Compiler
Haskell
Celeste Hollenbeck University of Edinburgh, Michael F. P. O'Boyle University of Edinburgh, Michel Steuwer University of Edinburgh
11:30
30m
Talk
Partial Type Constructors in Practice
Haskell
Apoorv Ingle University of Iowa, Alex Hubers The University of Iowa, J. Garrett Morris The University of Iowa
12:00
30m
Talk
Reasonable Agda is Correct Haskell: Writing Verified Haskell using agda2hs
Haskell
Jesper Cockx TU Delft, Lucas Escot TU Delft, Orestis Melkonian University of Edinburgh, James Chapman Input Output, Ulf Norell Gothenburg University
Pre-print File Attached