Write a Blog >>
Wed 20 Jan 2016 11:20 - 11:45 at Grand Bay South - Track 2: Types and Foundations Chair(s): Robert Atkey

Traversing an algebraic datatype by hand requires boilerplate code which duplicates the structure of the datatype. Datatype-generic programming (DGP) aims to eliminate such boilerplate code by decomposing algebraic datatypes into type constructor applications from which generic traversals can be synthesized. However, different traversals require different decompositions, which yield isomorphic but unequal types. This hinders the interoperability of different DGP techniques.

In this paper, we propose Fωμ, an extension of the higher-order polymorphic lambda calculus Fω with records, variants, and equirecursive types. We prove the soundness of the type system, and show that type checking for first-order recursive types is decidable with a practical type checking algorithm. In our soundness proof we define type equality by interpreting types as infinitary λ-terms (in particular, Berarducci-trees). To decide type equality we β-normalize types, and then use an extension of equivalence checking for usual equirecursive types.

Thanks to equirecursive types, new decompositions for a datatype can be added modularly and still interoperate with each other, allowing multiple DGP techniques to work together. We sketch how generic traversals can be synthesized, and apply these components to some examples.

Since the set of datatype decomposition becomes extensible, System Fωμ enables using DGP techniques incrementally, instead of planning for them upfront or doing invasive refactorings.

Wed 20 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:10
Track 2: Types and FoundationsResearch Papers at Grand Bay South
Chair(s): Robert Atkey University of Strathclyde
10:30
25m
Talk
Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega
Research Papers
Matt Brown UCLA, Jens Palsberg University of California, Los Angeles
Media Attached File Attached
10:55
25m
Talk
Type Theory in Type Theory using Quotient Inductive Types
Research Papers
Thorsten Altenkirch University of Nottingham, Ambrus Kaposi University of Nottingham
Media Attached File Attached
11:20
25m
Talk
System Fω with Equirecursive Types for Datatype-generic Programming
Research Papers
Yufei Cai University of Tübingen, Germany, Paolo G. Giarrusso University of Tübingen, Germany, Klaus Ostermann University of Tübingen, Germany
Media Attached
11:45
25m
Talk
A Theory of Effects and Resources: Adjunction Models and Polarised Calculi
Research Papers
Pierre-Louis Curien Univ. Paris Diderot and INRIA Paris-Rocquencourt, Marcelo Fiore Computer Laboratory, University of Cambridge, Guillaume Munch-Maccagnoni Computer Laboratory, University of Cambridge