You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('') and can be up to 35 characters long.
552 lines
22 KiB
552 lines
22 KiB
\documentclass{article}




\usepackage{mygeometry}


\usepackage{mylistings}


\usepackage{myhyperref}


\usepackage{mybibliography}




\usepackage{notations}




\title{Quantified Applicatives  API design for typeinference constraints}


\author{Olivier Martinot, Gabriel Scherer} % ordre alphabétique




\begin{document}




\maketitle




% TODO use Software Heritage for software and code source citation




\begin{abstract}


The \Inferno{} library~\citep*{inferno,infernocode} uses an


applicative functor \lstinline{'a co} to represent constraintbased


inference problems that elaborate into explicitlytyped term


representations. A central operation of the \Inferno{} API is the


\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 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


applicative functors, there would be standard solutions with a monad.




We report on our API design work to solve this issue. We start by


explaining the programming difficulties and why the \Inferno{}


functor is not a monad, then a first experiment with a codensity


monad, and finally a simpler solution that avoids mixing several


functors in the same codebase. Our approach makes good use of


the ``binding operators'' recently introduced in OCaml to provide


flexible syntactic sugar for monad or applicativelike structures.




We believe that the API design pattern we propose, ``turning direct


outputs into modal inputs'', may apply to any applicative functors


with quantifiers. It may already be in use, and its discussion may


benefit other projects. Experience sharing with the ML Workshop


audience could be very valuable.


\end{abstract}




\section{Inferno}




François Pottier's \Inferno{}~\citep{infernocode} is a software


library for constraintbased type inference. It exposes lowlevel data


structures and algorithms for efficient inference (unionfind graphs


for unification, levelbased generalization), a term representation


for inference constraints


(\sourcelink{src/SolverLo.mli}{SolverLo.mli})\footnote{We give links


to source code for the interested reader, which are versioned to


point at the versions of the software at the time of writing


(git revision


\texttt{d02e4c23430df0b8cd15a99adfa41fd00086b925}). }, and


a higherlevel API (\sourcelink{src/SolverHi.mli}{SolverHi.mli})


exposing an applicative functor \lstinline{'a co} designed to write


constraintbased type inference engines in a declarative


style~\citep{inferno}.




A value of type \lstinline{'a co} pairs together an inference


constraint with a function that will be called with the solution of


the constraint to construct an \lstinline{'a} ``witness'', that


inference has suceeded. For example, a typeinference procedure for ML


programs could have type


%


\lstinline{ML.term > F.term co}: it takes an ML term and generates


a constraint that, once solved, will produce an explicitytyped


representation of the input program as a System F term. The


implementation of Inferno comes with exactly such an example inference


program, for a core fragment of ML:


\sourcelink{client/Client.ml}{Client.ml}.




In this document we will use the following running example, adapted


from a fragment of the \Inferno{} inference example. On the right, we


show the types of the combinators we use, provided by \Inferno{}'s


highlevel layer:




\begin{minipage}{0.45\linewidth}


\begin{lstlisting}


let rec hastype (t : ML.term) (w : Infer.variable) : F.term co =


match t with


 [...]


 ML.Pair (u1, u2) >


exist (fun v1 >


exist (fun v2 >


w  Infer.Prod(v1, v2) ^^


hastype u1 v1 ^&


hastype u2 v2


)) <$$> fun (ty1, (ty2, (u'1, u'2))) >


F.Pair ((u'1, ty1), (u'2, ty2))


\end{lstlisting}


\end{minipage}


\hfill


\begin{minipage}{0.55\linewidth}


\begin{lstlisting}


val exist : (Infer.variable > 'a co) > (F.ty * 'a) co


val () : Infer.variable > Infer.ty > unit co


val (^^) : unit co > 'b co > 'b co


val (^&) : 'a co > 'b co > ('a * 'b) co


val (<$$>) : 'a co > ('a > 'b) > 'b co


\end{lstlisting}


\end{minipage}




We define a function \lstinline{hastype : ML.term > Infer.variable > F.term co}


which takes an ML term \lstinline{t} and a "destination inference variable"


\lstinline{w}; the returned constraint will unify the inferred type of


\lstinline{t} with \lstinline{w}, and return the elaborated System


F term. We show the inference code for the \lstinline{Pair(u1,u2)}


construct, representing pairs in ML; for illustration purposes we use


a "very explicit" syntax for pairs in the System F side, which expects


the two terms but also their types:~%


\lstinline{F.Pair : (F.term * F.ty) * (F.term * F.ty) > F.term}.


(In practice our pair syntax does not require explicit types,


but the Churchstyle syntax for $\lambda$abstractions does.)




The infix operation \lstinline{()} inserts a unification constraint


(\lstinline{Infer.ty} is not the source representation of ML or


F types, but an inferencespecific representation of types, which the


engine knows how to traverse for unification, etc.). The infix


combinators \lstinline{(^^), (^&)} pair constraints together. Finally,


\lstinline{<$$>} is a flipped \lstinline{map} function for constraints.




All typeinference cases have roughly this structure: using


\lstinline{exist} to create inference variables for subterms,


combining typechecking constraints to follow our typechecking rule,


concluded by a final ``map'' that takes all the witnesses of the


constraintsolving pieces, and combines them into a final witness for


the inferred term.




\subsection{The problem} Consider extending this code to handle not


just binary pairs, but nary tuples \lstinline{Tuple us}. Instead of


a staticallyknown number of inference variables (2), we want to


generate one for each subterm of the list, to build the result


type. How would you program this with the proposed API?




If \lstinline{'a co} was an inference/elaboration \emph{monad}, it


would be natural to decompose the problem with a function of type


\lstinline{'a list > Infer.variable list co}, or possibly


\lstinline{mapM : ('a > 'b co) > 'a list > 'b list co}, and then


\lstinline{bind} the result to continue. We write this hypothetical


program below on the left column. But \lstinline{'a co} is \emph{not}


a monad for a good reason  we explain this in the next


section. Instead, we have to write code in continuationpassing style,


on the right column below.




\hspace{3em}


\begin{minipage}{0.5\linewidth}


\begin{lstlisting}


 ML.Tuple us >


let on_each u =


exist (fun v > v ^& hastype u v)


<$$> fun (ty, (v, u')) > (v, (u', ty))


in


mapM on_each us >>= fun vutys >


let vs, utys = List.split vutys in


w  Infer.product vs ^^


return (ML.tuple utys)


\end{lstlisting}


\end{minipage}


\hfill


\begin{minipage}{0.5\linewidth}


\begin{lstlisting}


 ML.Tuple us >


let rec traverse us (k : variable list > 'r co)


: ((F.term * F.ty) list * 'r) co


= match us with


 [] > k [] <$$> fun r > ([], r)


 u::us >


exist (fun v >


traverse us (fun vs >


hastype u v ^&


k (v :: vs)


)) <$$> fun (ty, (u', (utys, rs))) >


((u', ty) :: utys, r)


in


traverse us (fun vs >


w  Infer.product vs


) <$$> fun (utys, ()) >


F.Tuple utys


\end{lstlisting}


\end{minipage}




Note: \lstinline{traverse} is called with a single continuation; it is


possible to inline this continuation in the emptylist case, and get


a simpler, less generic function, that could not be reused


elsewhere. We wish to discuss the reusable presentation in this


document, but the API design improvements also help in the


nonreusable case.




There are two difficulties with the code we had to write:


\begin{enumerate}


\item It is much harder to figure out how to write this code than in the monadic


version, which allows a natural problem decomposition. Programmers may not know


how to generate dynamically many inference variables. If they know that


some things can be done with CPS, they may not know exactly which,


or which signatures to use for CPS functions.


\item The code, in either versions, is hard to read. In particular,


values are \emph{named} far from where they are \emph{expressed} in


the program; notice for example how \lstinline{u'} binds the witness


of \lstinline{hastype u v}, but is placed farther away in the


program. This problem gets worse when writing inference code for


more complex constructs.




When we explain this code, we say that the \lstinline{Infer.ty}


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 pointfree programming.


\end{enumerate}




Our contribution is to identify, explain this problem, and propose


a partial solution: a systematic approach to programming with


``binders'' that can be explained and documented, and a different API


that lets us name terms in a more natural, local way  at the cost of


``unpacking'' operations later on, as we will explain.




While our work is specific to Inferno (and OCaml), we believe that


this API problem arises in the more general case of an applicative


functor with quantifiers, as \lstinline{exist} in our example.




\subsection{Aside: binding operators} OCaml recently adopted a flexible


syntactic sugar for composing computations in monadic and


applicativelike structures called ``binding operators''. Just like we


allow userdefined ``infix operators'' and ``prefix operators'' in


a limited set of symbols (\lstinline{(^^)}, \lstinline{(^&)}


were examples), we allow ``binding operators'' of the form


\lstinline{let<op>} and \lstinline{and<op>}, where \lstinline{<op>} is


a userchosen sequence of symbols, with the following desugaring rules:


\begin{lstlisting}


let<op1> p1 = e1 and<op2> p2 = e2 in body


==>


(let<op1>) ((and<op2>) e1 e2) (fun (p1, p2) > body)


\end{lstlisting}


The current convention is to use \lstinline{(let* )} for monadic


binding, and \lstinline{(let+), (and+)} for applicative map and


product. For example, with suitable user definitions one can write %


\lstinline{(let* x = m in e)} for %


\lstinline{(m >>= fun x > e)}, and %


\lstinline{(let+ x = foo and+ y = bar in e)} for %


\lstinline{(pure (fun x y > e) <$> foo <$> bar)}. Other symbols are


up for grabs.




We will use binding operators for convenience, but our solution does not


rely on them in an essential way.




\subsection{Not a monad} Giving up on our page limit, let us explain


why the \lstinline{'a co} type of Inferno cannot be given the


structure of a monad.




The witness \lstinline{'a} is built with knowledge of the


\emph{global} solution to the inference constraints


generated. Consider the applicative combinator %


\lstinline{pair : 'a co > 'b co > ('a * 'b) co}; both arguments


generate a part of the constraint, but the witnesses of \lstinline{'a}


and \lstinline{'b} can only be computed once the constraints on


\emph{both} sides are solved. For example, when inferring the ML term


\lstinline{(x, x + 1)}, the type inferred for the first component of


the pair is determined by unifications coming from the constraint of


the second.




Implementing \lstinline{bind : 'a co > ('a > 'b co) > 'b co}


would require building the witness for \lstinline{'a} before the


constraint arising from \lstinline{'b co} is known; this cannot be


done if \lstinline{'a} requires the final solution.




For the abstractly inclined: internally \lstinline{'a co} is


defined as \lstinline{raw_constraint * (solution > 'a)} it is the


composition of a ``writer'' monad that generate constraints and


a ``reader'' monad consuming the solution. For the composition


$W \circ R$ of two arbitrary monads to itself be a monad, a sufficient


condition~\citep{composingmonads} is that they commute:


$(R \circ W) \to (W \circ R)$  this suffices to define


$\mathtt{join} : (W \circ R \circ W \circ R) \to W \circ R$ from the


$\mathtt{join}$ operation of $W$ and $R$. Pushing the reader below the


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 corresponding CPS \emph{monad}. We can define


\lstinline{('a, 'i) co_cps} which does have an (indexed) monadic


structure:


\begin{lstlisting}


type ('a, 'i) co_cps = { run : 'r . ('a > 'r co) > ('i * 'r) co }


val bind : ('a, 'i1) co_cps > ('a > ('b, 'i2) co_cps) > ('b, 'i1 * 'i2) co_cps


val existM : (Infer.variable, F.ty) co_cps


\end{lstlisting}




This is an indexed version of the \emph{codensity} construction: for


any functor \lstinline{'a t}, the type\\ %


\lstinline{type 'a m = 'r. ('a > 'r t) > 'r t} has a monadic


structure. This lets us write \lstinline{exist} and our


\lstinline{traverse} above in monadic style, and then rely on our


usual monadic programming habits. Unfortunately, we found this too hard


to use in practice for the following reasons:


\begin{itemize}




\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


scopes over the constraint subterm \lstinline{rc}.




A \lstinline{co_cps} computation builds a single evergrowing scope


(by composing continuations in scope of all quantifiers effect


performed so var). The scope is only ``closed'' when the computation


is ``run'' by invoking it with the identity continuation  we can


define a \lstinline{close} combinator doing this.




Note that lifting all existential constraints to a toplevel, global


scope would be incorrect, due to the interplay with polymorphism /


generalization. We need to close the scope in a more local way.




In practice we found scoped programming with \lstinline{co_cps} less


natural than the syntactic/lexical scoping of the nonmonadic


style. It makes it harder to reason about scopes, and it forces us


to write programs with hybrid usage of both \lstinline{co_cps}


(for quantifiers) and \lstinline{co} (for scope control).




\item As we have to use a mix of the two structures \lstinline{co} and


\lstinline{co_cps} in our programs, we have to duplicate all


operations to work in both of them, or to use lifting combinators


from one layer to the other. This makes program more difficult to


write and read.


\end{itemize}




\section{Our proposal: turning direct outputs into modal inputs}




We propose to define a type \lstinline{'a binder} for


quantifierlike definitions that resembles the \lstinline{co_cps}


construct, with two key differences in API design:


\begin{enumerate}


\item Instead of using a \lstinline{bind} operator whose return type


is in the \lstinline{co_cps} monad, use a composition combinator


whose return type is in the \lstinline{co} applicative. As long as


our return type remains a \lstinline{co}, we only need one set of


operations.




\item When quantifiers produce witnesses, instead of adding the


witness type \lstinline{w} to the \emph{output} type of the


continuation, have the continuation take a \emph{modal input} of


type \lstinline{w co}.




For example, we change \lstinline{exist} from the first to


the second type:


\begin{lstlisting}


val exist : (Infer.variable > 'r co) > (F.ty * 'r) co


val exist : (Infer.variable * F.ty co > 'r co) > 'r co


\end{lstlisting}


\end{enumerate}




Here \lstinline{co} acts as a modality indicating that the value will


only be available at solution time. (In particular, no constraint is


produced. We could use the writer/reader decomposition of


\lstinline{co} to take only the reader part, but that would force us


to work with two different layers again.)




More concretely, we use the following definitions:


\begin{lstlisting}


type ('a, 'r) binder = ('a > 'r co) > 'r co


val exist : (Infer.variable * F.ty co, 'r) binder


\end{lstlisting}


(Note: we would like to define \lstinline{'a binder} with a universal


quantification on \lstinline{'r}, but OCaml makes it painful due its


limited support for universal inference; in practice binders only


occur in positive positions in our APIs, so we can keep their second


parameter polymorphic in each combinator, as for \lstinline{exist}.)




This change in type only requires a simple change in the


implementation of the quantifier.




\subsection{Final API and example}


Our final API looks as follows (other combinators are unchanged from


our initial examples):


\begin{lstlisting}[columns=flexible]


type ('a, 'r) binder = ('a > 'r co) > 'r co


val exist : (Infer.variable * F.ty co, 'r) binder




val (let@) : ('a, 'r) binder > ('a > 'r co) > 'r co (* identity *)


val (let+) : 'a co > ('a > 'b) > 'b co (* map *)


val (and+) : 'a co > 'b co > ('a * 'b) co (* pair *)


\end{lstlisting}




\lstinline{('a, 'r) binder} is a type of ``general quantifiers'',


which introduce arguments of type \lstinline{'a} to build a constraint


in a delimited scope returning a \lstinline{'r co}. Only terms of this


type are written in continuationpassing style. They are used through


\lstinline{let@}, that opens a quantifier which naturally scopes until


the end of the lexical block. The binder syntax is a reference to


OCaml's infix application operator \lstinline{(@@)}: %


\lstinline{(let@ p = a in b)} is equivalent to %


\lstinline{(b @@ fun p > a)}.




As a final example, let us revisit our ``tuple'' case with this new API.


(Left: before, Right: after)




\hspace{3em}


\begin{minipage}{0.45\linewidth}


\begin{lstlisting}


 ML.Tuple us >


let rec traverse


us (k : variable list > 'r co)


: ((F.term * F.ty) list * 'r) co


= match us with


 [] >


k [] <$$> fun r > ([], r)


 u::us >


exist (fun v >


traverse us (fun vs >


hastype u v ^&


k (v :: vs)


)) <$$> fun (ty, (u', (utys, rs))) >


((u', ty) :: utys, r)


in


traverse us (fun vs >


w  Infer.product vs


) <$$> fun (utys, ()) >


F.Tuple utys


\end{lstlisting}


\end{minipage}


\hfill


\begin{minipage}{0.55\linewidth}


\begin{lstlisting}


 ML.Tuple us >


let rec traverse (us : ML.term list)


: (variable list * (F.term * F.ty) list co,


'r) binder


= fun k > match us with


 [] >


k ([], pure [])


 u::us >


let@ v, ty = exist in


let@ (vs, us') = traverse us in


k (v :: vs,


let+ u' = hastype u v


and+ ty = ty


and+ us' = us'


in (u', ty) :: us')


in


let@ (vs, utys) = traverse us in


let+ () = w  Infer.product vs


and+ utys = utys


in F.Tuple utys


\end{lstlisting}


\end{minipage}




The CPS is now guided/documented by our types: to define


a \lstinline{(foo, 'r) binder} value we use CPS, and to use these binders


we use the \lstinline{let@} operators.




Modal inputs improve code readability by giving a name to an


expression at the logical place in the code (\lstinline{ty} and


\lstinline{us'} for example). Being in the applicative, a modal input


variable \lstinline{x} cannot be used asis to build the witness, it


has to be ``unpacked'' in the final%


\lstinline{let+ .. and+ .. in <witness>} block by the odd construction


\lstinline{and+ x = x}.


%


This unpacking construction is surprising, and the redudancy is


frustrating (one could think of a proper modaltyping rule in the


compiler that 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.




\subsection{Another example} To conclude, we would like to demonstrate


the generality of this approach to a wider family of applicative


functions with ``quantifier''like combinators, by briefly showcasing


the same refactoring in a different applicative functor  an


artificial example.




Consider an applicative \lstinline{'a cloud} for ``computations in the


cloud'', where operating on a resources (here a remote file) comes


with a ``cost'' (API usage, time, money, or something else) that is


returned to the programmer when they conclude using the resource. In


this model, opening a (remote) file for reading could be exposed by


the following quantifierlike operation:




\begin{lstlisting}


val with_input : path > (in_channel > 'r cloud) > (cost * 'r) cloud


\end{lstlisting}




and now the user desires to generalize this into a function that opens


a list of paths, operates on the correspond list of input channels,


and returns the sum of all costs (we will assume that


\lstinline{type cost = int} for simplicity). They want to implement:




\begin{lstlisting}


val with_inputs : path list > (in_channel list > 'r cloud) > (cost * 'r) cloud


\end{lstlisting}




and this is tricky. Our proposal, ``turning direct outputs into modal


inputs'', suggests the following change to the primitive operation,


introducing a \lstinline{binder} type that marks the place where


continuationpassingstyle should be used:




\begin{lstlisting}


type ('a, 'r) binder = ('a > 'r cloud) > 'r cloud


val with_input : (in_channel * cost cloud, 'r) binder


\end{lstlisting}




An implementation of \lstinline{with_inputs} using the original API is on the left,


and our proposed approach is on the right.




\hspace{3em}


\begin{minipage}{0.45\linewidth}


\begin{lstlisting}


let rec with_inputs paths k =


match paths with


 [] >


let+ r = k [] in (0, r)


 p :: ps >


let+ (cost_p, (cost_ps, r)) =


let@ chan = with_input p in


let@ chans = with_inputs pts in


k (chan :: chans)


in (cost_p + cost_ps, r)


\end{lstlisting}


\end{minipage}


\hfill


\begin{minipage}{0.55\linewidth}


\begin{lstlisting}


let rec with_inputs paths =


fun k > match paths with


 [] > k ([], pure 0)


 p :: ps >


let@ chan, cost_p = with_input p in


let@ chans, cost_ps = with_input ps in


let+ res = k (p :: ps)


and+ cost_p = cost_p


and+ cost_ps = cost_ps


in (cost_p + cost_ps, res)


\end{lstlisting}


\end{minipage}




Notice, again, that the original API pushes the cost ``on the stack'',


and that the variables \lstinline{cost_p}, \lstinline{cost_ps} are


bound far from the place that logically introduces them in the left


solution. The issue is solved on the right, at the cost of explicit


unpacking of the modal inputs.




\subsection*{Acknowledgments}


We wish to thank François Pottier and our anonymous reviewers for their feedback.




\bibliography{biblio}


\end{document}
