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/} grant
- N$^o$~\grantnum{NSERC}{298311/2012}. Any opinions, findings, and
+ Engineering Research Council of Canada}{http://nserc-crsng.gc.ca/} 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/bece7c8f563acd68ead00ade2bd9d6fda5c…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/bece7c8f563acd68ead00ade2bd9d6fda5c…
You're receiving this email because of your account on gitlab.com.
