Stefan pushed to branch report/itd at Stefan / Typer
Commits: aa3d24dc by Stefan Monnier at 2018-10-05T14:47:12Z -
- - - - -
1 changed file:
- paper.tex
Changes:
===================================== paper.tex ===================================== @@ -130,20 +130,20 @@ \begin{abstract} 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 combine in a single package - product types, sum types, and recursive types. But this also makes them - somewhat heavyweight: for example, tuples have to be defined as + functional programming languages. They conveniently combine in a single + package product types, sum types, and recursive 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. This can - be inconvenient when used as intermediate language in a compiler, as is - the case in Typer. In this article, we develop an alternative + a single field becomes a laborious full case-analysis on the object. + This can be inconvenient when used as intermediate language in a compiler, + as is the case in Typer. 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 in that each primitive maps to fewer assembly instructions, - yet we show it to be equivalent to the Calculus of Inductive - Constructions. A nice side-benefit is that every branch of \kw{case} - statements gets precise type information, including the default branch. + 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 also conveniently give a precise type to the default branch of + \kw{case} statements. \end{abstract}
%% 2012 ACM Computing Classification System (CSS) concepts @@ -642,6 +642,7 @@ which is sound and complete. \Infer{\JIcon e \ \JIpos \tau}{\JIcon {\Tsarw \tau e}}
%% Actual typing rules + %% FIXME: This lets all inductive types live in Type0!! \Infer{\Jtyper{\tau}{\Type{\ell}} \ \forall i \ \Jtyper[\Gamma,x:\tau]{c_i}{\Type{\ell_i}} \
View it on GitLab: https://gitlab.com/monnier/typer/commit/aa3d24dc53b19dcee6eace2bdc8308f2f57f...