[Git][monnier/typer][report/itd] -
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/bece7c8f563acd68ead00ade2bd9d6fda5cd... -- View it on GitLab: https://gitlab.com/monnier/typer/commit/bece7c8f563acd68ead00ade2bd9d6fda5cd... You're receiving this email because of your account on gitlab.com.
Afficher les réponses par date
participants (1)
-
Stefan