Write a Blog >>
Fri 24 Jan 2020 10:51 - 11:13 at Ile de France II (IDF II) - Type Systems Chair(s): Dominique Devriese

Functional programming languages assume that type constructors are total. Yet functional programmers know better: counterexamples range from container types that make limiting assumptions about their contents (e.g., requiring computable equality or ordering functions) to type families with defining equations only over certain choices of arguments. We present a language design and formal theory of partial type constructors, capturing the domains of type constructors using qualified types. Our design is both simple and expressive: we support partial datatypes as first-class citizens (including as instances of parametric abstractions, such as the Haskell Functor and Monad classes), and show a simple type elaboration algorithm that avoids placing undue annotation burden on programmers. We show that our type system rejects ill-defined types and can be compiled to a semantic model based on System F. Finally, we have conducted an experimental analysis of a body of Haskell code, using a proof-of-concept implementation of our system; while there are cases where our system requires additional annotations, these cases are rarely encountered in practical Haskell code.

Fri 24 Jan

Displayed time zone: Saskatchewan, Central America change

10:30 - 11:35
Type SystemsResearch Papers at Ile de France II (IDF II)
Chair(s): Dominique Devriese Vrije Universiteit Brussel
10:30
21m
Talk
Kind Inference for DatatypesDistinguished Paper
Research Papers
Ningning Xie The University of Hong Kong, Richard A. Eisenberg Bryn Mawr College, USA, Bruno C. d. S. Oliveira The University of Hong Kong, Hong Kong
Link to publication DOI Media Attached
10:51
21m
Talk
Partial Type Constructors: Or, Making Ad Hoc Datatypes Less Ad Hoc
Research Papers
Mark Jones Portland State University, J. Garrett Morris University of Kansas, USA, Richard A. Eisenberg Bryn Mawr College, USA
Link to publication DOI Media Attached File Attached
11:13
21m
Talk
Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation
Research Papers
Roland Meyer TU Braunschweig, Sebastian Wolff TU Braunschweig
Link to publication DOI Media Attached File Attached