inferno-api-design-paper/workshop.tex

\documentclass{article}

\usepackage{mygeometry}
\usepackage{mylistings}
\usepackage{myhyperref}
\usepackage{mybibliography}

\usepackage{notations}

\title{Quantified Applicatives -- API design for type-inference 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,inferno-code} uses an
  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{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 applicative-like 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{inferno-code} is a software
library for constraint-based type inference. It exposes low-level data
structures and algorithms for efficient inference (union-find graphs
for unification, level-based 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 higher-level API (\sourcelink{src/SolverHi.mli}{SolverHi.mli})
exposing an applicative functor \lstinline{'a co} designed to write
constraint-based 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 type-inference 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 explicity-typed
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
high-level 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 Church-style 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 inference-specific 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 type-inference cases have roughly this structure: using
\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
the inferred term.

\subsection{The problem} Consider extending this code to handle not
just binary pairs, but n-ary tuples \lstinline{Tuple us}. Instead of
a statically-known 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 continuation-passing 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 empty-list 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
non-reusable 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 point-free 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
applicative-like structures called ``binding operators''. Just like we
allow user-defined ``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 user-chosen 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{composing-monads} 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 sub-term \lstinline{rc}.

  A \lstinline{co_cps} computation builds a single ever-growing 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 non-monadic
  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
quantifier-like 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 continuation-passing 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 as-is 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 modal-typing 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 quantifier-like 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
continuation-passing-style 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}