Stefan pushed to branch report/itd at Stefan / Typer

Commits: 09881d77 by Stefan Monnier at 2018-11-16T23:25:42Z -

- - - - -

1 changed file:

- paper.tex

Changes:

===================================== paper.tex ===================================== @@ -847,8 +847,8 @@ the explicit equality witnesses can be used to get the same effect. \Infer{\Jsubtype {\tau_1}{\tau_2}} {\Jsubtype {\tau_1}{\TUnion{\tau_2}{\tau_3}}}

- \Infer{\Jsubtype {\tau_1}{\tau_2}} - {\Jsubtype {\tau_1}{\TUnion{\tau_3}{\tau_2}}} + \Infer{\Jsubtype {\tau_1}{\tau_3}} + {\Jsubtype {\tau_1}{\TUnion{\tau_2}{\tau_3}}}

\Infer{\Jsubtype {\tau_1}{\tau_3} \ {\Jsubtype {\tau_2}{\tau_3}}} {\Jsubtype {\TUnion{\tau_1}{\tau_2}}{\tau_3}} @@ -1044,6 +1044,12 @@ Section~\ref{sec:erasure}. \JUdecreasing {{x}\cup\nu} {e_1}} {\JUdecreasing \nu {\Tapp{(\Tlam x \tau {e_1})}{(\Tunfold{_}{_}{e_2})}}}

+ \Infer{e_2 = \Tapp{x_e}{\vec _} \ + \JUdecreasing {\nu} {e_2} \ + x_e \in \nu \ + \JUdecreasing {{x}\cup\nu} {e_1}} + {\JUdecreasing \nu {\Tapp{(\Tlam x \tau {e_1})}{(\TJ{_}{_}{e_2})}}} + \Infer{\JUdecreasing {\nu} {\tau_e} \ \JUdecreasing {\nu} {\tau_r} \ \JUdecreasing {\nu} {e} \ @@ -1515,14 +1521,49 @@ system differs from that of~\citet{Gimenez94} in the following aspects:

\subsection{CUC to CIC}

-\newcommand \TIeither[2] {\id{Either}~#1~#2} -\newcommand \TIUnit {\id{Unit}} -\newcommand \TIunit {\id{unit}} +\newcommand \TIeither[2] {\kw{Either}~#1~#2} +\newcommand \TIUnit {\kw{Unit}} +\newcommand \TIunit {\kw{unit}} \newcommand \TIPair[3] {\Sigma #1:#2. #3} -\newcommand \TIpair[2] {\id{dcons}~#1~#2} +\newcommand \TIpair[4] {\langle#1=#2,#3:#4\rangle} \newcommand \TIproj[2] {\pi_{#1}~#2} +\newcommand \TIeq[1] {\kw{eq}~#1} +\newcommand \TIrefl {\kw{refl}~} +\newcommand \TIJ[3] {\kw{J}~#1~#2~#3}

\begin{figure} + \begin{displaymath} + \begin{array}{l@{;=;}l} + \TIUnit & \Tind{x}{\Type0}{x} \ + \TIunit & \Tcon{0}{\TIUnit} \ + \TIPair{x}{\tau_1}{\tau_2} & \Tind{y}{\Type?}{\Tarw{x}{\tau_1}{\Tsarw{\tau_2}{y}}} \ + \TIpair{x}{e_1}{e_2}{\tau_2} & \Tcon{0}{\TIPair{x}{,?}{\tau_2}}~e_1~e_2 \ + \TIeq{e_1} & \Tind{x}{,\Tsarw{?}{x}}{\Tapp{x}{e_1}} \ + \TIrefl{e_1} & \Tcon{0}{\TIeq{e_1}} \ + \TIJ{e_\equiv}{e_f}{e} & + \TIcase{\Tlam{x}{,?}{\Tlam{_}{,?}{\Tapp{e_f}{x}}}}{e_\equiv}{}{e} \ + \TIeither{\tau_1}{\tau_2} & \Tind{x}{\Type?}{\Tsarw{\tau_1}{x}, \Tsarw{\tau_1}{x}} \ + \end{array} + \end{displaymath} + \begin{displaymath} + \begin{array}{l@{;=;}l} + \Ftocic{\Jsubtype \tau \tau} & \Tlam{x}{\tau}{x} \ + \Ftocic{\Jsubtype {\TUnion{\tau_1}{\tau_2}} {\tau_3}} & + \MAlign{\Tlam{x}{\TIeither{\tau_1}{\tau_2}}{} \ + ;;\TIcase{\Tlam{_}{,?}{\tau_3}}{x}{} + {\Ftocic{\Jsubtype {\tau_1} {\tau_3}}, + \Ftocic{\Jsubtype {\tau_2} {\tau_3}}}} \ + \Ftocic{\Jsubtype {\tau_1} {\TUnion{\tau_2}{\tau_3}}} & + \Tlam{x}{\tau_1}{\Tcon{0}{\TIeither{\tau_2}{\tau_3}} + ~(\Tapp{\Ftocic{\Jsubtype {\tau_1}{\tau_2}}}{x})} + ;;;;;;;\text{if }\Jsubtype {\tau_1}{\tau_2} + \ + \Ftocic{\Jsubtype {\tau_1} {\TUnion{\tau_2}{\tau_3}}} & + \Tlam{x}{\tau_1}{\Tcon{1}{\TIeither{\tau_2}{\tau_3}} + ~(\Tapp{\Ftocic{\Jsubtype {\tau_1}{\tau_3}}}{x})} + ;;;;;;;\text{if }\Jsubtype {\tau_1}{\tau_3} + \end{array} + \end{displaymath} \begin{displaymath} \begin{array}{l@{;=;}l} \Ftocic x & x \ @@ -1531,9 +1572,12 @@ system differs from that of~\citet{Gimenez94} in the following aspects: \Ftocic {\Tarw{x}{\tau_1}{\tau_2}} & \Tarw{x}{\Ftocic {\tau_1}}{\Ftocic {\tau_2}} \medskip \ \Ftocic {\Tuple \EmptyCtx} & \TIUnit \ - \Ftocic {\Tuple {x:\tau_0,\Delta}} & \TIPair{x}{\tau_0}{\Ftocic {\Tuple \Delta}} \ + \Ftocic {\Tuple {x:\tau_0,\Delta}} & + \TIPair{x}{\Ftocic{\tau_0}}{\Ftocic {\Tuple \Delta}} \ \Ftocic {\tuple \Delta {\cdot}} & \TIunit \ - \Ftocic {\tuple \Delta {e,\vec e}} & \TIpair e {\Ftocic {\tuple \Delta {\vec e}}}\ + \Ftocic {\tuple {x:\tau_0,\Delta} {e,\vec e}} & + \TIpair{x}{\Ftocic e} + {\Ftocic {\tuple \Delta {\vec e}}}{\Ftocic {\Tuple \Delta}} \ %% Note: The translation has reduction steps that don't correspond %% to any matching state in CUC. \Ftocic {\Tproj e i} & @@ -1541,12 +1585,16 @@ system differs from that of~\citet{Gimenez94} in the following aspects: %% Combined proj and let-binding, used for termination checking! \Ftocic {\Tapp{(\Tlam x {\tau_1} {e_1})}{\Tproj {e_2} 0}} & \MAlign{ - \TIcase {\Tlam x {\tau_{e_2}} {\Subst{\tau_2}{\TIproj 1 x}{x}}} {e_2} {?} - {\Tlam x {\tau_1} {\Tlam {_} {\Ftocic{\Tuple \Delta}} {e_1}}} \ + \TIcase {\tau_r} + {\Ftocic {e_2}} {?} + {\Tlam x {\Ftocic {\tau_1}} {\Tlam {_} {\Ftocic{\Tuple \Delta}} + {\Ftocic{e_1}}}} \ ;;\text{where } \MAlign{\Jtype{e_2}{\tau_{e_2}} - \text{ and }{\tau_{e_2} = \Tuple {y:\tau_0,\Delta}} \ - \Jtype[\Gamma,x:\tau_1]{e_1}{\tau_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}} + }} \ \Ftocic {\Tapp{(\Tlam x {\tau_1} {e_1})}{\Tproj {e_2} i}} & \MAlign{ \TIcase {\Tlam _ {\tau_{e_2}} {?}} {e_2} {?} @@ -1554,24 +1602,38 @@ system differs from that of~\citet{Gimenez94} in the following aspects: ;;\text{where } \MAlign{ %% ¡¡FIXME: \tau_1 is not equal to the type of y.(i-1)!! + %% We can get a proof `P : x₀=π₁ e₂` and then use + %% `J P y` to get y' that will have the appropriate type, + %% but then \JIdecreasing will not know that y' is + %% smaller than e₂ so termination checking fails! + \FIXME{Wow!} \ 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}} \ \Jtype[\Gamma,x:\tau_1]{e_1}{\tau_2}}} \medskip \ - \Ftocic {\id{Eq}} & \id{Eq} \ - \Ftocic {\id{refl}} & \id{refl} \ - \Ftocic {J} & J + \Ftocic {\Teq{e_1}{e_2}} & \TIeq{\Ftocic{e_1}}~{\Ftocic{e_2}} \ + \Ftocic {\Trefl{e_1}} & \TIrefl{\Ftocic{e_1}} \ + \Ftocic {\TJ{e_\equiv}{e_f}{e}} & + \TIJ{\Ftocic{e_\equiv}}{\Ftocic{e_f}}{\Ftocic{e}} + %% ;;\text{where }\MAlign{ + %% \Jtype{e_\equiv}{\Teq{e_1}{e_2}} \ + %% \Jtype{e_1}{\tau_1 : \Type{\ell_1}} \ + %% \Jtype{\Tapp{e_f}{e_1}}{\Type{\ell_2}}}} \medskip \ - \Ftocic {\Tmu[i]{x}{\tau}{e}} & \Tfix{i}{x}{\tau}{e} \ + \Ftocic {\Tmu[i]{x}{\tau}{e}} & \Tfix{i}{x}{\Ftocic{\tau}}{\Ftocic{e}} \ \Ftocic {\Tmu{x}{\tau}{(\Tmlam y \tau e)}} & - \Tind{x}{\tau}{\Tmarw y \tau {e\to \Tapp x {\vec y}}} \ - \Ftocic {\Tfold \tau {\vec p} e} & \Tcon{\Ftocic {\tau}}{0}~{\vec p}~e \ + \Tind{x}{\Ftocic{\tau}} + {\Tmarw y {\Ftocic{\tau}} {\Ftocic{e}\to \Tapp x {\vec y}}} \ + \Ftocic {\Tfold \tau {\vec p} e} & + \Tcon{\Ftocic {\tau}}{0}~{\vec {\Ftocic{p}}}~{\Ftocic{e}} \ \Ftocic {\Tunfold{\tau}{\vec p} e} & - \Ftocic {\Tapp{(\Tlam x {\Tapp{\tau}{\vec p}} x)}{(\Tunfold{\tau}{\vec p} e)}} \ + \Ftocic {\Tapp{(\Tlam x {,?} x)}{(\Tunfold{\tau}{\vec p} e)}} \ \Ftocic {\Tapp{(\Tlam x \tau {e_1})}{(\Tunfold{\tau}{\vec p} e)}} & - \TIcase{?}{e}{\Tapp{\tau}{\vec p}}{\Tmlam y {\tau_y} {\Tlam x x}} \ + \MAlign{ + \FIXME{Wow!} \ + \TIcase{?}{e}{\Tapp{\tau}{\vec p}}{\Tmlam y {\tau_y} {\Tlam x x}}} \ \medskip \ \Ftocic {\TUnion{\tau_1}{\tau_2}} & \TIeither{\Ftocic {\tau_1}}{\Ftocic {\tau_2}} \ %% \Ftocic {\Jsubtype{\tau_1}{\tau_2}} & \Tsarw{\Ftocic {\tau_1}}{\Ftocic {\tau_2}} \ @@ -1654,6 +1716,8 @@ judgments into the logic: $\Tapp{\id{terminating-function}}{f}$ (FIXME: how would this work? Can we just defer to F-star instead?). \item \kw{cast} can take a proof of type $\tau_1 \subseteq \tau_2$. +\item \kw{fold}/\kw{unfold} can be replaced by a proof of equality between + the folded and unfolded type, so \kw{J} can do the folding/unfolding. \item \kw{switch}'s ordering/splitting relation can similarly be reified. \item \kw{tuple} can take a list of fields (type $\Tapp{\id{field-list}}{\ell}$) \end{itemize}

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