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... -- View it on GitLab: https://gitlab.com/monnier/typer/commit/09881d771b3308299e0253de905e1b58dff5... You're receiving this email because of your account on gitlab.com.