polishing references to chapter 6

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.

Manuscript/future-work.tex

@@ -38,19 +38,19 @@ \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.
 To the best of my knowledge, only \citeauthor{McBride2022} has taken that question up,
 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

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}.
+that led me to it in \sidetextcite{LennonBertrand2022a}.

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}.
+présenté les difficultés qui m’y ont mené dans \sidetextcite{LennonBertrand2022a}.

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
 

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$.