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

In recent years, languages like Haskell have seen a dramatic surge of new features that significantly extends the expressive power of their type systems. With these features, the challenge of kind inference for datatype declarations has presented itself and become a worthy research problem on its own.

This paper studies kind inference for datatypes. Inspired by previous research on type-inference, we offer declarative specifications for what datatype declarations should be accepted, both for Haskell98 and for a more advanced system we call PolyKinds, based on the extensions in modern Haskell, including a limited form of dependent types. We believe these formulations to be novel and without precedent, even for Haskell98. These specifications are complemented with implementable algorithmic versions. We study soundness, completeness and the existence of principal kinds in these systems, proving the properties where they hold. This work can serve as a guide both to language designers who wish to formalize their datatype declarations and also to implementors keen to have principled inference of principal types.

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