Stefan pushed to branch report/itd at Stefan / Typer

Commits: 01eba948 by Stefan Monnier at 2018-11-13T21:57:43Z -

- - - - -

2 changed files:

- paper.tex - refs.bib

Changes:

===================================== paper.tex ===================================== @@ -36,11 +36,6 @@ %% \setcopyright{rightsretained} %% \copyrightyear{2018} %% If different from \acmYear

-%% Bibliography style -%% FIXME: I hate the way this bibliography looks because I find it -%% ridiculously hard to find the entry corresponding to a reference -%% like (Blume 2006) in the text. - %% \bibliographystyle{ACM-Reference-Format} %% Citation style %% Note: author/year citations are required for papers published as an @@ -57,6 +52,8 @@ \usepackage{fancybox} %For \ovalbox \usepackage{natbib} \renewcommand \cite \citep

+\DeclareUnicodeCharacter{03A0}{\ensuremath{\Pi}} +\DeclareUnicodeCharacter{03A3}{\ensuremath{\Sigma}} \DeclareUnicodeCharacter{03A9}{\ensuremath{\Omega}} \DeclareUnicodeCharacter{03B1}{\ensuremath{\alpha}} \DeclareUnicodeCharacter{03BB}{\ensuremath{\lambda}} @@ -113,8 +110,9 @@ \newcommand \Jcic[2][\Gamma] {#1 \vdash_I #2 :} \newcommand \Jstep[1] {#1 ;;\leadsto;; } %% \newcommand \Jstepr[1] {#1 \leadsto^{!*}} -\newcommand \JUstep[1] {#1 ;;\stackrel{U}{\leadsto};; } -\newcommand \JUstepr[1] {#1 \stackrel{U}{\leadsto}{!!}^*~} +\newcommand \JUstepArw {\stackrel{U}{\leadsto}} +\newcommand \JUstep[1] {#1 ;;\JUstepArw;; } +\newcommand \JUstepr[1] {#1 \JUstepArw{!!}^*~}

%% \newcommand \MetaFunction[2] {\llbracket #2 \rrbracket_{#1}} \newcommand \MetaFunction[2] {\left\llbracket #2 \right\rrbracket_{#1}} @@ -199,10 +197,6 @@ %% before \maketitle command in ACM style. %% \maketitle

-%% FIXME: I like to have the table of contents while writing, so I can get -%% a quick overview of the structure. Should be removed before submission. -%% \newpage \tableofcontents - \section{Introduction}

Typer~\cite{Monnier19a} is a functional language based on a pure type system, @@ -363,38 +357,6 @@ management. Basically, the language becomes too low-level, too close to machine language, tying the hands of the compiler too tightly for our needs.

-%% Inductive type options: -%% \begin{itemize} -%% \item Impredicative encoding: algorithmically inefficient, inability to -%% eliminate to different universe levels, inability to perform dependent -%% elimination (aka ``induction''). -%% \item Cedille's encoding: still problems with universe levels, -%% a straightforward implementation is algorithmically efficient but -%% recovering ML-style efficiency seems to require non-trivial -%% optimization efforts. -%% \item SML-style sum types: cleanly separates sums and products, but -%% dependent elimination is clumsy to specify, %% FIXME: Really? -%% and the representation tends to impose an additional indirection. -%% \item Either type: Dependent elimination is simpler to specify, -%% %% FIXME: `Either` looks very much like SML-style, so the above simplicity -%% %% may not be apparent, but indeed dependent -%% %% elimination is simpler in the sense that the "default" branch is known -%% %% to be "the other" branch, so there's really no default branch! -%% but it imposes an indirection like the SML-style, and the overhead grows -%% with the number of alternatives. -%% \item Haskell-style data types and Coq inductive types: tuples need to be -%% represented as degenerate sum types and eliminated with `case`, so record -%% selection like $x.l$ really expands to an expression of size proportional -%% to the number of fields of the record. Field extraction can't be -%% separated from case analysis. Dependent elimination is clumsy to specify -%% (especially for the default case). -%% \item Sigma type $\Sigma \id{tag}: \kw{bool} . \Tif {\id{tag}} {\tau_1} {\tau_2}$. -%% Elegant because it provides both pairs and sums at the same time. -%% Builds on booleans (or other datatypes) for the tags, so there's -%% a bootstrap (or duplication) problem; not sure how it can handle dependent -%% elimination either. -%% \end{itemize} - \subsection{Typing the default branch}

When performing case analysis in Coq and other languages of the family, the @@ -434,8 +396,6 @@ it practical to provide this feature even if it is not used very often. \textsl{(level)} & \ell &\in& \mathbb{N} \ \textsl{(ctxt)} & \Gamma,\Delta &::=& \EmptyCtx ~|~ \Gamma,x:\tau \ \textsl{(sort)} & s &::=& \Type \ell \ - %% FIXME: Already give the full syntax here! - %% FIXME: Or maybe not, since this same base language is used for CIC! \textsl{(term)} & e,\tau &::=& s ~|~ x ~|~ \Tlam x \tau e ~|~ \Tapp{e_1}{e_2} ~|~ \Tarw x {\tau_1} {\tau_2} \end{array} @@ -449,7 +409,7 @@ it practical to provide this feature even if it is not used very often. \end{array} \end{displaymath}

- %% FIXME: Let's assume that PTSes are sufficently known nowadays! + %% Let's assume that PTSes are sufficently known nowadays! %% \begin{mathpar} %% %% Context Rules %% \Infer{ }{\vdash \EmptyCtx} @@ -506,7 +466,7 @@ Because inductive types have non-trivial interactions with impredicativity, we did not include an impredicative universe at the bottom: all the calculi presented in this paper are fully predicative. -%% FIXME: The issue is much quite serious, since impredicativity +%% FIXME: The issue is quite serious, since impredicativity %% ends up introducing restrictions which prevent defining π₁ and/or π₂ %% on impredicative sums, so it's far from clear how to turn a `case` into %% a switch+projections! Same for erasability: we'll probably need to add @@ -556,8 +516,6 @@ The syntax of the complete language is the following: \textsl{(index)} & i &\in& \mathbb{N} \ \textsl{(sort)} & s &::=& \Type \ell \ \textsl{(ctxt)} & \Gamma,\Delta &::=& \EmptyCtx ~|~ \Gamma,x:\tau \ - %% FIXME: Already give the full syntax here! - %% FIXME: Or maybe not, since this same base language is used for CIC! \textsl{(term)} & e,\tau,p &::=& s ~|~ x ~|~ \Tlam x \tau e ~|~ \Tapp{e_1}{e_2} ~|~ \Tarw x {\tau_1} {\tau_2} \ \multicolumn 3 r {|~} & @@ -588,19 +546,6 @@ sufficiently orthogonal and are themselves simpler or more general. \subsection{Labeled tuples}

\begin{figure}[tb] - %% \begin{displaymath} - %% %% FIXME: `Tnth` can't be a function since it's only defined if - %% %% the index is within bounds! - %% \MAlign{ - %% %% FIXME: Mutual recursion, yuck! - %% \id{nth} : (n:\id{Nat})\to(x:\tau:\id{Types}_\ell)\to\id{Tnth}~x~n~0~\tau \ - %% \id{Tnth}~x~0~i~(\id{Tcons}_\ell~\tau~f) = \tau \ - %% \id{Tnth}~x~(s~n)~i~(\id{Tcons}_\ell~\tau~f) = \ - %% ;;;; - %% \id{Tnth}~x~n~(s~i)~(f~(\id{nth}~i~x)) - %% } - %% \end{displaymath} - \begin{mathpar} \Infer%% [T-base] { }{\Jcuc {\Tuple \EmptyCtx}{\Type 0}} @@ -1034,7 +979,7 @@ Section~\ref{sec:erasure}. \begin{mathpar} \ovalbox{\ensuremath{ \begin{array}[b]{l|l} - \JUpos e & \text{$e$ is positive in $x$} + \JUpos e ~&~ \text{$e$ is positive in $x$} \end{array} }} \vspace{-15pt} \hfill \\

@@ -1057,9 +1002,9 @@ Section~\ref{sec:erasure}. \begin{mathpar} \ovalbox{\ensuremath{ \begin{array}[b]{l|l} - \JUdecreasing{\nu}{e} & - \text{\TAlign{$i^{th}$ arg of $x_f$ always smaller than \ - $x_i$ in $e$, given that $\nu$ are smaller}} + \JUdecreasing{\nu}{e} ~&~ + \text{\TAlign{$i^{th}$ arg of $x_f$ always smaller than \ + $x_i$ in $e$, given that $\nu$ are smaller}} \end{array} }} \vspace{-15pt} \hfill \\

@@ -1068,7 +1013,7 @@ Section~\ref{sec:erasure}. \Infer{\JUdecreasing \nu \tau \ \JUdecreasing \nu e} {\JUdecreasing \nu {\Tlam x \tau e}}

- %% FIXME : add more congruence rules + %% Add more congruence rules here \else \fi

\Infer{x_f \not\in \kw{fv}(e)} @@ -1114,6 +1059,7 @@ Section~\ref{sec:erasure}. %% U = μx . (x \to x) %% f g = (unfold g) g

+\FigRecurse The final missing component of inductive types is that which gives it its name: the ability to define recursive types and to perform induction on values of those types. Both of those correspond to forms of recursive @@ -1134,7 +1080,6 @@ two syntactically separate. Concretely, the syntax is extended as follows: } \ \end{array} \end{displaymath} -\FigRecurse $\Tmu{x}{\tau}{e}$ is the fixpoint construct that can be used to define recursive types, as along as they obey the customary strict positivity constraint; $\Tmu[i]{x}{\tau}{e}$ is the fixpoint cons-truct that can be @@ -1192,8 +1137,9 @@ the two. \label{sec:erasure}

\newcommand \Erase[1] {#1{*}} -\newcommand \JEstep[1] {#1 ;;\stackrel{e}{\leadsto};; } -\newcommand \JEstepr[1] {#1 \stackrel{e}{\leadsto}{!!}^*~} +\newcommand \JEstepArw {\stackrel{e}{\leadsto}} +\newcommand \JEstep[1] {#1 ;;\JEstepArw;; } +\newcommand \JEstepr[1] {#1 \JEstepArw{!!}^*~}

The intention of our calculus is for \kw{cast}, \kw{fold}, and \kw{unfold} to have no run-time cost. In this section, we show that it is indeed the @@ -1217,12 +1163,6 @@ terms in a straightforward manner: %% \Erase{(\Tproj e i)} & \Tproj{\Erase e}i \ %% \Erase{(\TUnion{\tau_1}{\tau_2})} & \TUnion{\Erase{\tau_1}}{\Erase{\tau_2}} \ \Erase{(\TUcast{\tau_1}{\tau_2}e)} & \Erase e \ - %% FIXME: hardcodes \Erase! - %% \MAlign[c]{(\TUcase {e} {\tau_e \} {\Ttagvar}{x}{e_\Ttagvar \}{y}{e_d})*} & - %% \MAlign[c]{\TUcase[\Erase{\tau_r}] {\Erase e} {\Erase{\tau_e} \} - %% {\Ttagvar}{x}{\Erase{e_\Ttagvar} \}{y}{\Erase{e_d}}} \ - %% \Erase{(\Tmu[i]{x}{\tau}{e})} & \Tmu[i]{x}{\Erase \tau}{\Erase e} \ - %% \Erase{(\Tmu{x}{\tau}{e})} & \Tmu{x}{\Erase \tau}{\Erase e} \ \Erase{(\Tfold{\tau}{\vec p}{e})} & \Erase e \ \Erase{(\Tunfold{\tau}{\vec p}{e})} & \Erase e \ \end{array} @@ -1231,18 +1171,14 @@ The $\cdots$ stand for all the remaining constructs where the function simply recurses in the obvious way on all subterms. We do not need to introduce a new syntax for erased terms because they simply use a subset of the syntax of the non-erased terms. - -On the other hand, we do need to introduce new reduction rules. Other than -the usual congruence rules, the reduction rules of the erased calculus are -the following: +%% +On the other hand, we do need to introduce a new reduction judgment $e_1 +\JEstepArw e_2$. Other than the usual congruence rules, the reduction rules +of the erased calculus are the following: %% \begin{mathpar} \JEstep{\Tapp{(\Tlam x \tau {e_1})}{e_2}}{\Subst{e_1}{e_2}x}

- \JEstep{(\tuple \Delta {\vec e}).i}{e_i} - - \JEstep {J~_~_~_~_~_~(\id{refl}~_~_)~x}x - \begin{array}{c} \JEstep{ \TUcase {(\tuple \Delta {\vec e})} {\tau_e} @@ -1254,6 +1190,8 @@ the following: } \end{array}

+ \JEstep{(\tuple \Delta {\vec e}).i}{e_i} + \begin{array}{c} \JEstep{ \TUcase {(\tuple[l'] \Delta {\vec e})}{\tau_e} @@ -1265,9 +1203,11 @@ the following: } \end{array}

- \Infer{e_i = \tuple{_}{_}} - {\JEstep{\Tapp{(\Tmu[i]{x}{\tau}{e})}{\vec e}} - {\Tapp{(\Subst{e}{\Tmu[i]{x}{\tau}{e}}x)}{\vec e}}} + \JEstep {J~_~_~_~_~_~(\id{refl}~_~_)~x}x + + \Infer{e_i = \tuple{_}{_} \ e = \Tmu[i]{x}{\tau}{e'}} + {\JEstep{\Tapp{e}{\vec e}} + {\Tapp{(\Subst{e'}{e}{x})}{\vec e}}} \end{mathpar}

We can show that this erasure calculus is consistent with the original @@ -1279,13 +1219,13 @@ be implemented as no-ops: Assuming $ \Jcuc e \tau$, we have: \begin{itemize} \item If $\JUstepr e {e_1}$ then $\JEstepr{\Erase e}{\Erase {e_1}}$. - \item If $\JEstepr{\Erase e}{e_2}$ then there exists an $e_3$ such that + \item If ${\Erase e}\JEstepArw{e_2}$ then there exists an $e_3$ such that $\Erase{e_3} = e_2$ and $\JUstepr e {e_3}$. \end{itemize} \end{lemma} -%% \begin{proof} -%% FIXME -%% \end{proof} +\begin{proof} + FIXME +\end{proof}

\section{Equivalence} \label{sec:equivalence} @@ -1316,8 +1256,9 @@ compiled to this CIC, and the reverse as well. \newcommand \JIpos[2][x] {#1 \vdash #2;;\kw{pos}} \newcommand \JIdecreasing[3][x_f;i;x_i] {#1;#2 \vdash #3;;\kw{term}} \newcommand \BT[2] {\id{BT}\llbracket #1 \rrbracket_{#2}} -\newcommand \JIstep[1] {#1 ;;\stackrel{I}{\leadsto};; } -\newcommand \JIstepr[1] {#1 \stackrel{I}{\leadsto}{!!}^*~} +\newcommand \JIstepArw {\stackrel{I}{\leadsto}} +\newcommand \JIstep[1] {#1 ;;\JIstepArw;; } +\newcommand \JIstepr[1] {#1 \JIstepArw{!!}^*~}

\begin{figure*} %% Syntax @@ -1326,13 +1267,10 @@ compiled to this CIC, and the reverse as well. \begin{mathpar} \ovalbox{\ensuremath{ \begin{array}[b]{l|l} - \Jcic e \tau & \text{$e$ has type $\tau$ in $\Gamma$} \ - \JIstep {e}{e'} & \text{$e$ reduces to $e'$} + \Jcic e \tau ~&~ \text{$e$ has type $\tau$ in $\Gamma$} \ + \JIstep {e}{e'} ~&~ \text{$e$ reduces to $e'$} \end{array} }} \hfill - %% FIXME: This presentation doesn't allow `Con(0,Nat)` but requires - %% substituting every `Nat` with its definition. - %% Could it be that this is not needed in CUC? \Infer{e = \Tind{x}{\tau}{\vec c} \ \Jcic e \tau} {\Jcic{\Tcon{i}{e}}{\Subst{c_i}{x}{e}}} \hfill @@ -1386,8 +1324,8 @@ compiled to this CIC, and the reverse as well. \begin{mathpar} \ovalbox{\ensuremath{ \begin{array}[b]{l|l} - \JIpos e & \text{$e$ is positive in $x$} \ - \JIcon e & + \JIpos e ~&~ \text{$e$ is positive in $x$} \ + \JIcon e ~&~ \text{$e$ is the type of a constructor of $y$, positive in $x$} \end{array} @@ -1414,9 +1352,9 @@ compiled to this CIC, and the reverse as well. \begin{mathpar} \ovalbox{\ensuremath{ \begin{array}[b]{l|l} - \JIdecreasing \nu e & - \text{$i^{th}$ arg of $x_f$ always smaller than $x_i$ - in $e$, given that $\nu$ are smaller} + \JIdecreasing \nu e ~&~ + \text{\TAlign{$i^{th}$ arg of $x_f$ always smaller than \ + $x_i$ in $e$, given that $\nu$ are smaller}} \end{array} }} \vspace{-15pt} \hfill \\ %% Decreasing recursive calls @@ -1544,8 +1482,8 @@ enforce that inductive types are indeed inductive and that recursive definitions are terminating. Beside the slightly different syntax, our system differs from that of~\citet{Gimenez94} in the following aspects: \begin{itemize} -\item We omitted the obvious congruence rules for the $\leadsto$ relation and the - termination judgment; +\item We omitted the obvious congruence rules for the $\JIstepArw$ relation + and the termination judgment; \item Our rules are extended to a tower of universes; \item The typing rule of \kw{Ind} enforces predicativity; \item Giménez does not include the \kw{Ind} rule of $\JIpos e$; which allows to @@ -1725,6 +1663,7 @@ judgments into the logic: \nocite{Chapman10} %Levitation \nocite{Christiansen16} %Idris's use in elaboration \nocite{Firsov18} %Cedille +\nocite{Altenkirch10} %PiSigma, manual use of reduction rules?

\section{Conclusion}

===================================== refs.bib ===================================== @@ -42,7 +42,7 @@ Instead it has an Emacs-based interface which allows programming by gradual refinement of incomplete type-correct terms.}, - url = {http://www.cse.chalmers.se/~ulfn/papers/tphols09/ + url = {http://www.cse.chalmers.se/%5C~%7B%7Dulfn/papers/tphols09/ tutorial.pdf}, }

@@ -471,6 +471,48 @@ url = {http://doi.acm.org/10.1145/3167087%7D, }

+@inproceedings{Altenkirch10, + author = {Thorsten Altenkirch and Nils Anders Danielsson and + Andres Löh and Nicolas Oury}, + booktitle = {International Symposium on Functional and Logic + Programming}, + key = {FLOPS'10}, + pages = {40-55}, + title = {ΠΣ: Dependent Types without the Sugar}, + year = {2010}, + abstract = {The recent success of languages like Agda and Coq + demonstrates the potential of using dependent types + for programming. These systems rely on many + high-level features like datatype definitions, + pattern matching and implicit arguments to facilitate + the use of the languages. However, these features + complicate the metatheoretical study and are a + potential source of bugs. To address these issues we + introduce ΠΣ, a dependently typed core language. It + is small enough for metatheoretical study and the + type checker is small enough to be formally verified. + In this language there is only one mechanism for + recursion—used for types, functions and infinite + objects—and an explicit mechanism to control + unfolding, based on lifted types. Furthermore + structural equality is used consistently for values + and types; this is achieved by a new notion of + α-equality for recursive definitions. We show, by + translating several high-level constructions, that + ΠΣ is suitable as a core language for dependently + typed programming.}, + url = {http://www.cs.nott.ac.uk/%5C~%7B%7Dpsztxa/publ/pisigma-new.pdf%7D, +} + +@proceedings{FLOPS10, + booktitle = {International Symposium on Functional and Logic + Programming}, + key = {FLOPS'10}, + title = {International Symposium on Functional and Logic + Programming}, + year = {2010}, +} + @proceedings{ICFP06, address = {Portland, Oregon}, booktitle = {International Conference on Functional Programming},

View it on GitLab: https://gitlab.com/monnier/typer/commit/01eba94895ecb7dc67f1af3ad1cb56523b46...