Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Sun 18 Aug 2019 14:30 - 14:50 at Aurora Borealis - Invited Talk and Metatheory Chair(s): Jeremy Gibbons

Algebraic data types and inductive types like those of the Calculus of Inductive Constructions (CIC) are the bread and butter of statically typed functional programming languages. They conveniently combine in a single package product types, sum types, recursive types, and indexed types. But this also makes them somewhat heavyweight: for example, tuples have to be defined as ``degenerate'' single constructor inductive types, and extraction of a single field becomes a laborious full case-analysis on the object. We consider this to be unsatisfactory. In this article, we develop an alternative presentation of CIC’s inductive types where the various elements are provided separately, such that inductive types are built on top of tuples and sums rather than the other way around. The resulting language is lower-level yet we show it to be equivalent to a predicative version of the Calculus of Inductive Constructions. An additional benefit is that it can conveniently give a precise type to the default branch of \kw{case} statements.

Sun 18 Aug

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:40 - 14:50
Invited Talk and MetatheoryTyDe at Aurora Borealis
Chair(s): Jeremy Gibbons Department of Computer Science, University of Oxford
Cubes, Cats, Effects
Inductive types deconstructed
Stefan Monnier Université de Montréal
Link to publication