Blogs (28) >>
ICFP 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom
Wed 6 Sep 2017 16:40 - 17:03 at L1 - Inference and Analysis Chair(s): Mark Jones

We present an approach to support partiality in type-level computation without compromising expressiveness or type safety. Existing frameworks for type-level computation either require totality or implicitly assume it. For example, type families in Haskell provide a powerful, modular means of defining type-level computation. However, their current design implicitly assumes that type families are total, introducing nonsensical types and significantly complicating the metatheory of type families and their extensions. We propose an alternative design, using qualified types to pair type-level computations with predicates that capture their domains. Our approach naturally captures the intuitive partiality of type families, simplifying their metatheory. As evidence, we present the first complete proof of consistency for a language with closed type families.

Wed 6 Sep

Displayed time zone: Belfast change

16:40 - 17:50
Inference and AnalysisResearch Papers at L1
Chair(s): Mark Jones Portland State University
16:40
23m
Talk
Constrained Type Families
Research Papers
J. Garrett Morris University of Kansas, USA, Richard A. Eisenberg Bryn Mawr College, USA
DOI
17:03
23m
Talk
Automating Sized-Type Inference for Complexity Analysis
Research Papers
Martin Avanzini University of Innsbruck, Austria, Ugo Dal Lago University of Bologna, Italy / Inria, France
DOI
17:26
23m
Talk
Inferring Scope through Syntactic Sugar
Research Papers
Justin Pombrio Brown University, USA, Shriram Krishnamurthi Brown University, USA, Mitchell Wand Northeastern University, USA
DOI