Stefan pushed to branch report/itd at Stefan / Typer

Commits: 86597690 by Stefan Monnier at 2018-10-17T21:46:19Z -

- - - - -

1 changed file:

- paper.tex

Changes:

===================================== paper.tex ===================================== @@ -492,7 +492,7 @@ extensions. \label{fig:pairs} \end{figure}

- Fig.~\ref{fig:pairs} shows the usual typing rules for dependent pairs. + Figure~\ref{fig:pairs} shows the usual typing rules for dependent pairs.

\FIXME{Does this interact with impredicativity?} \FIXME{Can we use the impredicative encoding and avoid adding it to @@ -534,7 +534,7 @@ extensions. \label{fig:sums} \end{figure}

- Fig.~\ref{fig:sums} shows the usual typing rules for tagged sums. + Figure~\ref{fig:sums} shows the usual typing rules for tagged sums. }

%% \newpage @@ -686,15 +686,46 @@ that any value of arrow type has to be of the form $\lambda x:\tau.e$. \label{fig:tagged-terms} \end{figure}

- Fig.~\ref{fig:tagged-terms} shows the typing rules for tagged terms. + Figure~\ref{fig:tagged-terms} shows the typing rules for tagged terms. }

+%% \newpage +\section{Equality} + +\begin{figure} + \begin{displaymath} + \begin{array}{l@{;:;}l} + \id{Eq} & \Tarw{t}{\Type{}}{\Tarw {x,y} t {\Type{0}}}; \ + \id{refl} & \Tarw{t}{\Type{}}{\Tarw{x}{t}{\id{Eq}~t~x~x}}; \ + J & \MAlign{ + \Tarw{t}{\Type{}}{\Tarw {x,y} t {\Tarw u {\Type{}} {\Tarw + f {\Tsarw t u} {}}}} \ + \Tsarw{\id{Eq}~t~x~y}{\Tsarw{f~x}{f~y}} + ;} + \end{array} + \end{displaymath} + + \begin{mathpar} + \Jstep {J~_~_~_~_~_~(\id{refl}~_~_)~x}x + \end{mathpar} + %% With impredicativity we could define it as:\hfill\mbox{} + %% \begin{displaymath} + %% \begin{array}{l} + %% \id{Eq}~t~x~y = \Tarw u {\Type{}} {\Tarw + %% f {\Tsarw t u} {\Tsarw{f~x}{f~y}}}; \ + %% \id{refl}~t~x~=\Tlam u {\Type{}} {\Tlam f {(\Tsarw t u)} {\Tlam v {(f~x)} v}}; + %% \end{array} + %% \end{displaymath} + \caption{Equality type} + \label{fig:equality} +\end{figure} + %% \newpage \section{Unions}

\newcommand \TUnion[1] {#1~\cup~} \newcommand \TUnionSmart[1] {#1~\cup'~} -\newcommand \TUweaken[1] {\id{Sub.weaken}~#1~} +\newcommand \TUweaken[1] {\id{S.weaken}~#1~} \newcommand \TUcase[6] {\kw{switch}~#1~|~#2~#3~P_{#3}~\Rightarrow #4~|~#5~P_{#5}~\Rightarrow #6}

\newcommand \JSplit[3] {#2 \Longleftarrow #1~/\Ttagvar \Longrightarrow #3} @@ -754,27 +785,30 @@ initial environment: %% \multicolumn 1 l {_{\subseteq}_ \hfill :} & _\cup_ & \Type{\ell_1}\to\Type{\ell_2}\to\Type{\Tmax{\ell_1}{\ell_2}} \ _{\subseteq}_ & \Type{\ell_1}\to\Type{\ell_2}\to\Type{\Tmax{\ell_1}{\ell_2}} \medskip \ - \id{Sub.refl};\tau & \Jsubtype \tau \tau \ - \id{Sub.left};\tau_3 & + \id{S.refl};\tau & \Jsubtype \tau \tau \ + \id{S.left};\tau_3 & \Jsubtype{\tau_1}{\tau_2} \to \Jsubtype{\tau_1}{\TUnion{\tau_2}{\tau_3}} \ - \id{Sub.right};\tau_3 & + \id{S.right};\tau_3 & \Jsubtype{\tau_1}{\tau_2} \to \Jsubtype{\tau_1}{\TUnion{\tau_3}{\tau_2}} \ - \id{Sub.both} & + \id{S.both} & \Jsubtype{\tau_1}{\tau_3} \to \Jsubtype{\tau_2}{\tau_3} \to \Jsubtype{\TUnion{\tau_1}{\tau_2}}{\tau_3} \ - \id{Sub.weaken} & \Jsubtype{\tau_1}{\tau_2} \to \tau_1 \to \tau_2 \ + \id{S.trans} & + \Jsubtype{\tau_1}{\tau_2} \to \Jsubtype{\tau_2}{\tau_3} \to + \Jsubtype{\tau_1}{\tau_3} \ + \TUweaken{} & \Jsubtype{\tau_1}{\tau_2} \to \tau_1 \to \tau_2 \ %% \end{array} \end{displaymath} These declarations define the new union $\cup$ type as well as a new subtype -type $\subseteq$. Then come four constructors that allow constructing proofs of -subtyping between union types, and finally the \id{Sub.weaken} operation +type $\subseteq$. Then come constructors that allow constructing proofs of +subtyping between union types, and finally the \id{S.weaken} operation which should be read as a form of casting from a subtype to a supertype.

Note that we are cheating a bit here: not only those declarations use a shorthand notation eliding some arguments that can be inferred, but they rely on some form of universe polymorphism, so they should be read -a declaration schemas, which need to be freshly instantiated for each use. +as declaration schemas, which need to be freshly instantiated for each use.

After casting our subtypes to their supertype, we need some way to recover the lost information. For that we introduce the following new syntax: @@ -794,9 +828,59 @@ of data. Our \kw{switch} statement tests a single label before falling through to a default branch, but it can be trivially chained in order to select between several possible labels, of course.

+Reduction rules of the languages are +extended with the obvious congruence rules as well as the following +primitive reductions: +\begin{figure*} + \begin{displaymath} + \begin{array}{r@{;;\leadsto;;}l} + \id{S.weaken}~P_1~(\id{S.weaken}~P_2~e) & + \id{S.weaken}~(\id{S.trans}~P_2~P_1)~e \ + %% \multicolumn 2 l {\TUcase {(\tuple \Delta {\vec e})} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d}} \ + %% & + %% \Subst{e_\Ttagvar}{\id{refl},\tuple \Delta {\vec e}}{P_x,x} \ + %% \multicolumn 2 l {\TUcase {(\tuple[l'] \Delta {\vec e})} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d}} \ + %% & + %% \Subst{e_d}{\id{refl},\tuple[l'] \Delta {\vec e}}{P_y,y} \ + %% \multicolumn 2 l {\TUcase {(\TUweaken P {(\tuple \Delta {\vec e})})} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d}} \ + %% & + %% \Subst{e_\Ttagvar}{\id{refl},\tuple \Delta {\vec e}}{P_x,x} \ + %% \multicolumn 2 l {\TUcase {(\tuple[l'] \Delta {\vec e})} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d}} \ + %% & + %% \Subst{e_d}{\id{refl},\tuple[l'] \Delta {\vec e}}{P_y,y} \ + %% FIXME: Get rid of those first two! + \TUcase {(\tuple \Delta {\vec e})} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} & + \Subst{e_\Ttagvar}{\id{refl},\tuple \Delta {\vec e}}{P_x,x} \ + \TUcase {(\tuple[l'] \Delta {\vec e})} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} & + \Subst{e_d}{\id{refl},\tuple[l'] \Delta {\vec e}}{P_y,y} \ + \TUcase {(\TUweaken P {(\tuple \Delta {\vec e})})} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} & + \Subst{e_\Ttagvar}{\id{refl},\tuple \Delta {\vec e}}{P_x,x} \ + \TUcase {(\TUweaken P {(\tuple[l'] \Delta {\vec e})})} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} & + \Subst{e_d}{\id{refl},\tuple[l'] \Delta {\vec e}}{P_y,y} \ + \end{array} + \end{displaymath} +\end{figure*} + +\begin{displaymath} + \begin{array}{l@{;;\leadsto;;}l} + \id{S.trans}~\id{S.refl}~P & P \ + \id{S.trans}~P~\id{S.refl} & P \ + \id{S.trans}~P_1~(\id{S.left}~\tau~P_2) & + \id{S.left}~\tau~(\id{S.trans}~P_1~P_2) \ + \id{S.trans}~P_1~(\id{S.right}~\tau~P_2) & + \id{S.right}~\tau~(\id{S.trans}~P_1~P_2) \ + \id{S.trans}~(\id{S.left}~\tau~P_1)~(\id{S.both}~P_2~P_3) & + \id{S.trans}~P_1~P_2 \ + \id{S.trans}~(\id{S.right}~\tau~P_1)~(\id{S.both}~P_2~P_3) & + \id{S.trans}~P_1~P_3 \ + \id{S.trans}~(\id{S.both}~P_1~P_2)~P_3 & + \id{S.both}~(\id{S.trans}~P_1~P_3)~(\id{S.trans}~P_2~P_3) \ + \end{array} +\end{displaymath} + %% FIXME: reduction rules? Especially for the `weaken` thingy!

-Fig.~\ref{fig:unions} shows our typing rules for unions. Our unions are +Figure~\ref{fig:unions} shows the typing rules for unions. Our unions are unusual in that the subterms that make up the type cannot be arbitrary types, to make sure we can apply \kw{case} to them.

@@ -851,37 +935,6 @@ types, to make sure we can apply \kw{case} to them. \label{fig:recurse} \end{figure}

-\newpage -\section{Equality} - -\begin{figure} - \begin{displaymath} - \begin{array}{l@{;:;}l} - \id{Eq} & \Tarw{t}{\Type{}}{\Tarw {x,y} t {\Type{0}}}; \ - \id{refl} & \Tarw{t}{\Type{}}{\Tarw{x}{t}{\id{Eq}~t~x~x}}; \ - J & \MAlign{ - \Tarw{t}{\Type{}}{\Tarw {x,y} t {\Tarw u {\Type{}} {\Tarw - f {\Tsarw t u} {}}}} \ - \Tsarw{\id{Eq}~t~x~y}{\Tsarw{f~x}{f~y}} - ;} - \end{array} - \end{displaymath} - - \begin{mathpar} - \Jstep {J~_~_~_~_~_~(\id{refl}~_~_)~x}x - \end{mathpar} - %% With impredicativity we could define it as:\hfill\mbox{} - %% \begin{displaymath} - %% \begin{array}{l} - %% \id{Eq}~t~x~y = \Tarw u {\Type{}} {\Tarw - %% f {\Tsarw t u} {\Tsarw{f~x}{f~y}}}; \ - %% \id{refl}~t~x~=\Tlam u {\Type{}} {\Tlam f {(\Tsarw t u)} {\Tlam v {(f~x)} v}}; - %% \end{array} - %% \end{displaymath} - \caption{Equality type} - \label{fig:equality} -\end{figure} - \section{Erasure}

The intention of our calculus is for \kw{weaken} to have no run time cost. @@ -1207,7 +1260,7 @@ $\Ftocic \bot = \bot$. \Ftocuc {\Tarw{x}{\tau_1}{\tau_2}} & \Tarw{x}{\Ftocuc {\tau_1}}{\Ftocuc {\tau_2}} \ \Ftocuc {\TUnion{\tau_1}{\tau_2}} & \TIeither{\Ftocuc {\tau_1}}{\Ftocuc {\tau_2}} \ \Ftocuc {\Jsubtype{\tau_1}{\tau_2}} & \Tsarw{\Ftocuc {\tau_1}}{\Ftocuc {\tau_2}} \ - %% \Ftocuc {\id{Sub.refl}{e}} & \ + %% \Ftocuc {\id{S.refl}{e}} & \ \Ftocuc {\TUweaken{P}{e}} & \Tapp{\Ftocuc {P}}{\Ftocuc {e}} \ \Ftocuc {\id{Tup.Types}~\ell} & \Type~\ell \ \Ftocuc {\id{Tup.Tnil}} & \id{True} \

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