Stefan pushed to branch report/itd at Stefan / Typer

Commits: bece7c8f by Stefan Monnier at 2019-03-27T23:57:03Z -

- - - - -

1 changed file:

- paper.tex

Changes:

===================================== paper.tex ===================================== @@ -1238,6 +1238,8 @@ be implemented as no-ops: \section{Equivalence} \label{sec:equivalence}

+\FIXME{No such compilation, neither one way nor the other!} + %% FIXME: We have a problem with inductive types's universe level: CUC %% does not let the user define Bool elsewhere than Type₀, whereas %% the CIC presented does. @@ -1247,7 +1249,7 @@ be implemented as no-ops:

Now that we have defined a calculus which provides us with the intended run-time cost, we show that this calculus is sound and complete with respect -to a more classic presentation of inductive types. We will first present +to a more classical presentation of inductive types. We will first present a variant of the base calculus extended with inductive types in the style of~\citet{Gimenez94}, and then show that any expression of our CUC can be compiled to this CIC, and the reverse as well. @@ -1606,7 +1608,7 @@ system differs from that of~\citet{Gimenez94} in the following aspects: \MAlign{\Jtype{e_2}{\tau_{e_2}} \text{ and }{\tau_{e_2} = \Tuple {x:\tau_1,\Delta}} \ \Jtype[\Gamma,x:\tau_1]{e_1}{\tau_2} \ - \tau_r = \Tlam x {\Ftocic {\tau_{e_2}}} {\Subst{\Ftocic {\tau_2}}{\TIproj 1 x}{x}} + \tau_r = \Tlam y {\Ftocic {\tau_{e_2}}} {\Subst{\Ftocic {\tau_2}}{\TIproj 1 y}{x}} }} \ \Ftocic {\Tapp{(\Tlam x {\tau_1} {e_1})}{\Tproj {e_2} i}} & \MAlign{ @@ -1615,14 +1617,20 @@ system differs from that of~\citet{Gimenez94} in the following aspects: {(\TIrefl{(\TIproj 1 {e_2})})} \ ;;\text{where } \MAlign{ - \FIXME{Wow!} \ - b = {\Tlam {x_0} {\tau_0} {\Tlam {y} {\Ftocic{\Tuple \Delta}} - {\textsl{body}}}} \ - \textsl{body} = \Tlam{x_\equiv}{\Teq{x_0}{\TIproj 1 {e_2}}}{?} \ - e' = \Ftocic{\Tapp{(\Tlam x {\tau_1} {e_1})} - {\Tproj {y} {(i - 1)}}} \ \Jtype{e_2}{\tau_{e_2}} \text{ and }{\tau_{e_2} = \Tuple {x_0:\tau_0,\Delta}} \ + %% Here we have a major problem: + %% The type of `x` is supposed to be that of πi, but instead + %% `Case` only gives us a type which we can convert to πi + %% with the convoy-pattern, but this makes the value go + %% through `J` which in turns makes it "not smaller" any more! + \FIXME{Wow!} \ + b = {\Tlam {x_0} {\tau_0} {\Tlam {x_t} {\Ftocic{\Tuple \Delta}} + {\textsl{body}}}} \ + \textsl{body} = \Tlam{x_\equiv}{(\Teq{x_0}{\TIproj 1 {e_2}})}{e'} \ + x_t' = \TIJ{x_\equiv}{(\Tlam{x_0}{\tau_0}{\Ftocic{\Tuple \Delta}})}{x_t} \ + e' = (\Tlam{x_t}{}{\Ftocic{\Tapp{(\Tlam x {\tau_1} {e_1})} + {\Tproj {x_t} {(i - 1)}}}})~x_t' \ \Jtype[\Gamma,x:\tau_1]{e_1}{\tau_2} \ \tau_r = \Tlam {x_e} {,?} {\Tarw{_} {\Teq{\TIproj 1 {x_e}}{\TIproj 1 {e_2}}} @@ -1740,12 +1748,13 @@ judgments into the logic:

\section{Related works}

-\nocite{Gimenez94} -\nocite{Blume06,Castagna16} %Union types and extensible sums -\nocite{Chapman10} %Levitation -\nocite{Christiansen16} %Idris's use in elaboration -\nocite{Firsov18} %Cedille -\nocite{Altenkirch10} %PiSigma, manual use of reduction rules? +\\cite{Gimenez94} +\\cite{Blume06,Castagna16} Union types and extensible sums +\\cite{Chapman10} Levitation +\\cite{Christiansen16} Idris's use in elaboration +\\cite{Firsov18} Cedille +\\cite{Altenkirch10} PiSigma, manual use of reduction rules? +\\cite{Trellys}

\section{Conclusion}

@@ -1754,8 +1763,9 @@ judgments into the logic: \newcommand \grantnum[2] {#2} \begin{acks} This work was supported by the \grantsponsor{NSERC}{Natural Sciences and - Engineering Research Council of Canada}{http://nserc-crsng.gc.ca/%7D grant - N$^o$~\grantnum{NSERC}{298311/2012}. Any opinions, findings, and + Engineering Research Council of Canada}{http://nserc-crsng.gc.ca/%7D grants + N$^o$~\grantnum{NSERC}{298311/2012} and \grantnum{NSERC}{RGPIN-2018-06225}. + Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the NSERC. \end{acks}

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