Sciweavers

POPL
2016
ACM

System f-omega with equirecursive types for datatype-generic programming

7 years 11 months ago
System f-omega with equirecursive types for datatype-generic programming
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 higherorder 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 equivale...
Yufei Cai, Paolo G. Giarrusso, Klaus Ostermann
Added 09 Apr 2016
Updated 09 Apr 2016
Type Journal
Year 2016
Where POPL
Authors Yufei Cai, Paolo G. Giarrusso, Klaus Ostermann
Comments (0)