fixes suggested by Olivier

This commit is contained in:
Gabriel Scherer 2020-05-30 11:16:40 +02:00
parent 21f06a8816
commit f8a213624d
1 changed files with 8 additions and 8 deletions

View File

@ -21,12 +21,12 @@
applicative functor \lstinline{'a co} to represent constraint-based
inference problems that elaborate into explicitly-typed term
representations. A central operation of the \Inferno{} API is the
\lstinline{exists} quantifier, which generates a fresh inference
variable scoped in an existential constraint. \lstinline{exists}
\lstinline{exist} quantifier, which generates a fresh inference
variable scoped in an existential constraint. \lstinline{exist}
returns the result of solving the constraint, as well as the
elaborated type inferred for the inference variable:
%
\lstinline{val exists : (variable -> 'a co) -> ('a * ty) co}
\lstinline{val exist : (variable -> 'a co) -> ('a * ty) co}
We found that programming with this interface is difficult and leads
to program that are hard to read. The difficulty is specific to
@ -128,7 +128,7 @@ combinators \lstinline{(^^), (^&)} pair constraints together. Finally,
\lstinline{<$$>} is a flipped \lstinline{map} function for constraints.
All type-inference cases have roughly this structure: using
\lstinline{exists} to create inference variables for subterms,
\lstinline{exist} to create inference variables for subterms,
combining type-checking constraints to follow our type-checking rule,
concluded by a final ``map'' that takes all the witnesses of the
constraint-solving pieces, and combines them into a final witness for
@ -209,7 +209,7 @@ There are two difficulties with the code we had to write:
complex constructs.
When we explain this code, we say that the \lstinline{Infer.ty}
result of \lstinline{exists} or the \lstinline{(F.term * F.ty) list}
result of \lstinline{exist} or the \lstinline{(F.term * F.ty) list}
result of \lstinline{traverse} is ``pushed on the stack'' -- which
is then later shuffled around by the \lstinline{(<$$>)} operator.
We would rather avoid this particular style of point-free programming.
@ -283,7 +283,7 @@ writer would require reading the solution before writing the
constraint; this is not possible if we want the final solution.
\section{Failed attempt: codensity} If we have to write in CPS style, a natural
idea is to program in the correspond CPS \emph{monad}. We can define
idea is to program in the corresponding CPS \emph{monad}. We can define
\lstinline{('a, 'i) co_cps} which does have an (indexed) monadic
structure:
\begin{lstlisting}
@ -304,7 +304,7 @@ to use in practice for the following reasons:
\item \lstinline{exist} is a naturally \emph{scoped} construction:
besides generating a free variables, it builds a raw constraint term
of the form \lstinline{CExist(x,rc)}, where the inference variable
is only bound in the sub-contraint term \lstinline{rc}.
is only bound in the constraint sub-term \lstinline{rc}.
A \lstinline{co_cps} computation builds a single ever-growing scope
(by composing continuations in scope of all quantifiers effect
@ -422,7 +422,7 @@ has to be ``unpacked'' in the final%
Unpacking is slightly surprising, and the redudancy is frustrating
(one could think of a proper modal-typing rule in the compiler that
would implicit unpack modal inputs); but note that the unpacking place
would implicitly unpack modal inputs); but note that the unpacking place
corresponds to the place, in the previous style, where the variable
would have been first named. Unpacking is a fair price to pay to
recover readable code.