From d31bdcd379de3e523c8e5c9ebfc80f4d19184b7f Mon Sep 17 00:00:00 2001 From: Meven Date: Mon, 30 May 2022 17:27:42 +0200 Subject: [PATCH] polishing references to chapter 6 --- Manuscript/bidir-intro.tex | 2 +- Manuscript/future-work.tex | 19 ++++++++++++------- Manuscript/intro-en.tex | 2 +- Manuscript/intro-fr.tex | 2 +- Manuscript/main.tex | 2 +- Manuscript/typed-untyped-algo.tex | 17 ++++++++++------- 6 files changed, 26 insertions(+), 18 deletions(-) diff --git a/Manuscript/bidir-intro.tex b/Manuscript/bidir-intro.tex index a505263..69e9f43 100644 --- a/Manuscript/bidir-intro.tex +++ b/Manuscript/bidir-intro.tex @@ -90,7 +90,7 @@ With those set clear, we go on with their adaptation to \kl{PCUIC}, and the subtle issues that arose in that context, in \cref{chap:bidir-pcuic}. Finally, \cref{chap:bidir-conv} describes early investigations into giving a -bidirectional treatment not only of typing, but also of conversion. +bidirectional treatment not only of typing, but also of \kl{conversion}. % This equivalence has been formalised on top of MetaCoq \cite{Sozeau2020}\footnote{A version frozen as described in this article is available in the following git branch: \url{https://github.com/MevenBertrand/metacoq/tree/itp-artefact}.} % We next turn back to less technical considerations, as we believe that the bidirectional structure is of general theoretical interest. \Cref{sec:beyond} thus describes the value of basing type systems on the bidirectional system directly rather than on the equivalent undirected one. Finally \cref{sec:related} investigates related work, and in particular tries and identify the implicit presence of constrained inference in various earlier articles, showing how making it explicit clarifies those. \ No newline at end of file diff --git a/Manuscript/future-work.tex b/Manuscript/future-work.tex index 5bca1d9..500078c 100644 --- a/Manuscript/future-work.tex +++ b/Manuscript/future-work.tex @@ -38,7 +38,7 @@ \section{Bidirectional Typing for Dependent Types} the case of Church-style syntax is quite different. In the case of normal forms, the proof ideas presented in this thesis should be easily adapted. But if we wish to go beyond normal forms, we must consider the use of annotations in terms, -as is done in \eg \sidetextcite{McBride2022} \sidetextcite{Gratzer2019} or +as is done in \eg \sidetextcite{McBride2022}, \sidetextcite{Gratzer2019} or \sidetextcite{Dunfield2021}. However, due to the dependently-typed setting, we have to investigate how these annotations play out with conversion and/or reduction. @@ -46,11 +46,11 @@ \section{Bidirectional Typing for Dependent Types} but does not arrive – yet – at a definitive solution, so there is matter left for further research. -Another thread to pull is the relation with Generalized Type Systems, as presented in -\sidetextcite{Bauer2020,Bauer2022}. Here as in McBride’s discipline we find +Another thread to pull is the relation with Generalized Type Systems +\sidecite{Bauer2020,Bauer2022}. Here, as in McBride’s discipline, we find well-formation invariants to be preserved, and carefully structured rules that should respect them. Re-casting -the bidirectional ideas in such a setting could allow for a better understanding both of the +the bidirectional concepts in such a setting could allow for a better understanding both of the ideas at work in bidirectional typing, yielding a proper formal account of McBride’s discipline together with a general proof that it ensures @@ -62,7 +62,10 @@ \section{Bidirectional Typing for Dependent Types} to question how we can marry conversion and bidirectionalism. Here again there are ingredients in the air: \sidetextcite{Abel2017} show a notion of conversion geared towards proving decidability of typing, but which is clearly bidirectional, and could serve as a basis to give a general -notion of bidirectional conversion. +notion of bidirectional conversion. This subject is only scratched in \cref{chap:bidir-conv}, but +I believe that the ideas presented there can be scaled to a system such as \kl{PCUIC}, and +be an interesting building block in order to specify extensionality rules as used in \kl{Coq}’s +kernel. \section{\kl{MetaCoq}’s Future} @@ -97,9 +100,11 @@ \section{\kl{MetaCoq}’s Future} around that untyped notion of conversion, and could not be so easily adapted to a typed conversion. This makes the integration of η laws challenging. The case of strict propositions is less well-known, being much more recent, but poses similar challenges. +A possibile direction would be to move the whole development over to typed conversion, +using the ideas introduced in \cref{chap:bidir-conv}. The second lacking feature are modules and functors. -While these are less pervasive than η laws, they are still important in a number of developments. +While these are less pervasive than η laws, they are still present in a number of developments. Here again the difficulty is not simply to show that an implementation is faithful to a given semantic, but to precisely pin down said semantic. This is tricky in the case of modules, which have interactions with global environments, contrarily to records – their first-class counterpart. @@ -113,7 +118,7 @@ \section{\kl{MetaCoq}’s Future} and show that it fulfils the conditions we abstractly ask for in the current development. More ambitious, the complex guard condition implemented in \kl{Coq} was designed \sidecite{Gimenez1995} in order to allow a translation back to eliminators. -This gives a much stronger validity criterion for the guard, and would not be a simple project. +This gives a much stronger validity criterion for the guard, but would not be an easy project. But as for modules, reaching that goal would make the guard much more trustworthy than it currently is. Moreover, it could open the door to extending it, with the formalization diff --git a/Manuscript/intro-en.tex b/Manuscript/intro-en.tex index 02938f1..afc5d81 100644 --- a/Manuscript/intro-en.tex +++ b/Manuscript/intro-en.tex @@ -634,4 +634,4 @@ \subsection{Technical contributions} Finally, \cref{chap:bidir-conv} corresponds to a project I initiated in order to extend \kl{MetaCoq} to integrate extensionality η rules to conversion, but which did not reach the stage of publication yet. Yet, I presented the difficulties -raised in \sidetextcite{LennonBertrand2022a}. \ No newline at end of file +that led me to it in \sidetextcite{LennonBertrand2022a}. \ No newline at end of file diff --git a/Manuscript/intro-fr.tex b/Manuscript/intro-fr.tex index f3db59f..3535971 100644 --- a/Manuscript/intro-fr.tex +++ b/Manuscript/intro-fr.tex @@ -707,4 +707,4 @@ \subsection{Contributions techniques et publications} Enfin le \cref{chap:bidir-conv} correspond à un projet que j’ai entamé dans le but d’étendre \kl{MetaCoq} pour intégrer des règles η d’extensionalité à la conversion, mais qui n’a pas encore atteint le stade de la publication. J’ai en revanche -présenté les difficultés soulevées dans \sidetextcite{LennonBertrand2022a}. \ No newline at end of file +présenté les difficultés qui m’y ont mené dans \sidetextcite{LennonBertrand2022a}. \ No newline at end of file diff --git a/Manuscript/main.tex b/Manuscript/main.tex index b93a031..86caa81 100644 --- a/Manuscript/main.tex +++ b/Manuscript/main.tex @@ -36,7 +36,7 @@ \usepackage{styles/macros} \usepackage{styles/alectryon-minted} -\includeonly{typed-untyped-algo} +% \includeonly{typed-untyped-algo} \graphicspath{{./figures/}} % Paths where images are looked for diff --git a/Manuscript/typed-untyped-algo.tex b/Manuscript/typed-untyped-algo.tex index 41d91a8..717f172 100644 --- a/Manuscript/typed-untyped-algo.tex +++ b/Manuscript/typed-untyped-algo.tex @@ -56,7 +56,7 @@ \chapter{Bidirectional Conversion} finally, \cref{sec:unty-conv-equiv} presents the equivalence between this bidirectional conversion and the untyped one. -All of the chapter is rather new, and its material has not yet been submitted to peer-reviewing. +The content of this chapter is rather new, and its material has not yet been submitted to peer-reviewing. As such, it should be regarded as a first attempt at making interesting ideas visible, rather than a finished and polished exposition. @@ -119,7 +119,7 @@ \subsection{Conversion checks, neutral comparison infers} \AP The important intuition about this relation is that it actually decomposes conversion in two components. On one side, \intro{generic conversion}, that we will continue writing% -\sidenote{We use the color \typedcolor{blue} for the typed relations, and the $\typedcolor{\vdash_{\symup{t}}}$ +\sidenote{We use the colour \typedcolor{blue} for the typed relations, and the $\typedcolor{\vdash_{\symup{t}}}$ symbol to distinguish typing judgments defined using the typed relations.} $\intro* \bconvop$, which takes a type as \kl{input} – \ie it \emph{checks}. On the other side, @@ -301,15 +301,15 @@ \subsection{Conversion checks, neutral comparison infers} \section{Untyped Presentation} \label{sec:unty-conv} -In the presentation of \cref{sec:bidir-conv}, types are carried around, +\AP In the presentation of \cref{sec:bidir-conv}, types are carried around, but almost never used. Indeed, only \ruleref{rule:bd-fun-conv} really needs the type information to be applied. However, there is an alternative approach, used by the kernels of \kl{Coq} and \kl{Agda}, which avoids looking at types altogether by replacing the type-directed \ruleref{rule:bd-fun-conv} with term-directed ones. As types are not maintained, there is also no point in maintaining the context either. -Thus, this alternative \kl{conversion} simply relates two terms: $\buconv{\gamma}{t}{t'}$.% -\sidenote{We use the color \untypedcolor{purple} for untyped relations, and the +Thus, this alternative \kl{conversion} simply relates two terms: $intro* \buconv{\gamma}{t}{t'}$.% +\sidenote{We use the colour \untypedcolor{purple} for untyped relations, and the $\untypedcolor{\vdash_{\symup{u}}}$ symbol for typing judgments defined using those relations.} Let us now spell out the rules for this alternative, untyped presentation. @@ -331,6 +331,7 @@ \section{Untyped Presentation} \label{fig:gene-ucum} \end{figure} +\AP \phantomintro{\bucumhop} The first rules of \cref{fig:gene-ucum} are similar to those for the typed variants: cumulativity can be used in checking, and terms are compared by first reducing them to weak-head normal form, and if they are neutrals the special \kl{neutral comparison} is called. @@ -355,6 +356,7 @@ \section{Untyped Presentation} \label{fig:bd-cong-univ} \end{figure} +\AP \phantomintro{\uconvhop}\phantomintro{\ucumhop} The rules for the comparison of types are given in \cref{fig:bd-cong-univ}, and are again close to those for the typed variant: there is a congruence rule for Π-types, and universes are convertible when their levels are in the right relation. @@ -373,6 +375,7 @@ \section{Untyped Presentation} \label{fig:neu-ucomp} \end{figure} +\AP \phantomintro{\nuconvop} In the case of \kl{neutral comparison}, the rules (\cref{fig:neu-ucomp}) are even simpler than in the typed case, because there is no need for a special rule to reduce the type. Thus, there are only two rules, one for application and one base case for variables. @@ -435,7 +438,7 @@ \subsection{Modes for the relations} With the modes set down, the following definitions of \kl{inputs} and \kl{outputs} well-formation are rather natural. The only maybe surprising point is that we express all those conditions in the typed variant. This way, we need only consider the meta-theory of -one system – the one based on typed relations –, and can carry over all these properties to +one system – the one based on typed relations~–, and can carry over all these properties to the other system after we have proven their equivalence. \begin{definition}[Inputs well-formation – typed relations] @@ -710,7 +713,7 @@ \section{Equivalence of the presentations} In case $w$ is a λ-abstraction, say $\l x : A.\ t$ and $w'$ is a neutral $n'$, then $v'$ must be equal to $n'\ x$. Then we have $f\ x \hred w\ x \hored t \hred v$, and thus $\buconv{|\Gamma|,x}{t}{n'\ x}$ since $\uconvh{|\Gamma|,x}{v}{n'\ x}$. - Therefore \ruleref{rule:bd-abs-neu} applies to conclude. The reasoning in the symmetric case where $w'$ is an abstraction + Therefore, \ruleref{rule:bd-abs-neu} applies to conclude. The reasoning in the symmetric case where $w'$ is an abstraction and $w$ is neutral is similar. In the last case, both $w$ and $w'$ are neutrals, say $n$ and $n'$. Then $v$ and $v'$ are respectively $n\ x$ and $n'\ x$.