inferno-api-design-paper/slides.tex

\documentclass{beamer}

\usetheme{CambridgeUS}

\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}

\usepackage{mylistings-slide}
  
\title[API design for type-inference constraints]{Quantified Applicatives \\
  API design for type-inference constraints}

\author{\textbf{Olivier Martinot}, Gabriel Scherer}
\institute[]{PARTOUT team / Inria Saclay}

\begin{document}

\frame{\titlepage}

\begin{frame}{Summary of the work}
\begin{itemize}
\item Inferno exposes an applicative functor with quantifier-like functions
\item We found a difficulty to write certain programs.
\item We present a change of API that solves it

      (turn direct outputs into modal inputs)
\item This applies to any applicative functors with "quantifiers with outputs"

  \lstinline{('i -> 'c t) -> ('o * 'c) t}
\end{itemize}
\end{frame}

\begin{frame}[fragile]{Introduction to Inferno}
\begin{itemize}
\item Library developped by François Pottier
\item Constraint-based type inference
\item \lstinline{'a co} $ = $ a constraint $ + $ a function that will
      be called with its solution
\item Applicative functor with quantifiers
\end{itemize}

\pause

\begin{block}{Remark}
\lstinline{'a co} is not a monad.

\lstinline{bind : 'a co -> ('a -> 'b co) -> 'b co}
requires the \lstinline{'a} before we have the \lstinline{'b co} constraint :
impossible if \lstinline{'a} requires the complete solution.
\end{block}

\begin{block}{Example}
\lstinline{(x, x + 1)} \hfill\textcolor{gray}
          {unifications coming from the second constraint}
\end{block}

\end{frame}

\begin{frame}[fragile]{Code example (with exist)}

\begin{lstlisting}
let<op1> p1 = e1 and<op2> p2 = e2 in body
                  ==>
(let<op1>) ((and<op2>) e1 e2) (fun (p1, p2) -> body)
\end{lstlisting}

\pause

\begin{lstlisting}
val exist : (Infer.variable -> 'a co) -> (F.ty * 'a) co
val (---) : Infer.variable -> Infer.ty -> unit co

val (let@) : (('a -> 'c co) -> 'c co)
               -> ('a -> 'c co) -> 'c co
val (let+) : 'a co -> ('a -> 'b) -> 'b co
val (and+) : 'a co -> 'b co -> ('a * 'b) co
\end{lstlisting}

\end{frame}

\begin{frame}[fragile]{Code example (with exist)}  
\begin{small}

\begin{lstlisting}
let rec hastype
  (t : ML.term) (w : Infer.variable)
  : F.term co
  = match t with
  | [...]
  | ML.Pair (u1, u2) ->
    let+ (ty1, (ty2, (u1', u2'))) =
      let@ v1 = /* \alert<2>{exist}*/ in
      let@ v2 = /* \alert<3>{exist}*/ in
      let+ () = w /*\alert<4>{------}*/ Infer.Prod(v1,v2)
      and+ u1' = hastype u1 v1
      and+ u2' = hastype u2 v2
      in (u1', u2')
    in F.Pair ((u1', ty1), (u2', ty2))
\end{lstlisting}

\begin{lstlisting}
/*
\only<2,3>{val \alert{exist} : (Infer.variable -> 'a co) -> (F.ty *\ 'a) co}
\only<4>{val \alert{(------)} : Infer.variable -> Infer.ty -> unit co}
*/
\end{lstlisting}

\end{small}
\end{frame}

\begin{frame}[fragile]{The problem}
Generate a arbitrary number of inference variables ?\\
If \lstinline{'a co} was a monad :
\begin{lstlisting}
| ML.Tuple us ->
  let on_each u =
    let@ v = exist in
    let+ v = v
    and+ u' = hastype u v
    in (v, (u', ty))
  in
  mapM on_each us >>= fun vutys ->
  let vs, utys = List.split vutys in
  let+ () = w --- Infer.product vs in
  return (ML.tuple utys)
\end{lstlisting}
\begin{block}{}
\lstinline{'a co} is not a monad, so we are forced to write in continuation
passing style
\end{block}


\end{frame}

\begin{frame}[fragile]{Example with another applicative}

\begin{itemize}
\item An applicative \lstinline{'a cloud} for ``computations in the cloud''
\item Operating on a resource (here a remote file) comes with a ``cost''

\begin{lstlisting}[basicstyle=\footnotesize\ttfamily]
val with_input : path ->
  (in_channel -> 'c cloud) -> (cost * 'c) cloud
\end{lstlisting}
\end{itemize}

\pause\vfill

How to implement the following?
\begin{lstlisting}[basicstyle=\footnotesize\ttfamily]
val with_inputs : path list ->
  (in_channel list -> 'c cloud) -> (cost * 'c) cloud
\end{lstlisting}
Same issue as the non-static number of \texttt{exist}.
\end{frame}

\begin{frame}[fragile]{CPS solution}
\begin{lstlisting}[basicstyle=\footnotesize\ttfamily]
| ML.Tuple us ->
  let rec traverse us (k : variable list -> 'c co)
    : ((F.term * F.ty) list * 'c) co
    = match us with
    | [] -> let+ c = k [] in ([], c)
    | u::us ->
      let+ (ty, (u', (utys, r))) =
        let@ v = exist in
        let+ (utys, (u' r)) = traverse us (fun vs ->
          let+ u' = hastype u v
          and+ r = k (v :: vs)
          in (u', r))
        in (u', (utys, r))
      in ((u', ty) :: utys, r)
  in
  let+ (utys, ()) = traverse us (fun vs ->
    w --- Infer.product vs)
  in F.Tuple utys
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]{Our proposal: direct outputs => modal inputs}

Instead of quantifiers with a direct \emph{output}:
\begin{lstlisting}
val old_quantifier : (input -> 'c) -> (/*\alert{output}*/ * 'c) co
\end{lstlisting}

have the continuation take a \emph{modal input} \lstinline{output co}:
\begin{lstlisting}
val new_quantifier : (input * /*\alert{output co}*/ -> 'c) -> 'c co
\end{lstlisting}

\pause\vfill

For \lstinline{exist}:
\begin{lstlisting}
val old_exist : (Infer.variable -> 'c co) -> (/*\alert{F.ty}*/ * 'c) co
val new_exist : (Infer.variable * /*\alert{F.ty co}*/ -> 'c co) -> 'c co
\end{lstlisting}

\pause\vfill

For \lstinline{with_input}:
\begin{lstlisting}
val old_with_input : path ->
  (in_channel -> 'c cloud) -> (cost * 'c cloud)
val new_with_input : path ->
  (in_channel * cost cloud -> 'c cloud) -> 'c cloud
\end{lstlisting}

\end{frame}

\begin{frame}[fragile]{New API}

\begin{lstlisting}[basicstyle=\footnotesize\ttfamily]
type ('a, 'c) binder = ('a -> 'c co) -> 'c co
val exist : (Infer.variable * F.ty co, 'r) binder

val (let@) : ('a, 'c) binder -> ('a -> 'c co) -> 'c co  (* identity *)
val (let+) : 'a co -> ('a -> 'b) -> 'b co               (* map *)
val (and+) : 'a co -> 'b co -> ('a * 'b) co             (* pair *)
\end{lstlisting}

\end{frame}

\begin{frame}[fragile]{New code example}

\hspace{-1em}
\begin{minipage}{0.5\linewidth}
\begin{lstlisting}[basicstyle=\tiny\ttfamily]
| ML.Tuple us ->
  let rec traverse us (k : variable list -> 'c co)
    : ((F.term * F.ty) list * 'c) co
    = match us with
    | [] -> let+ c = k [] in ([], c)
    | u::us ->
      let+ (ty, (u', (utys, r))) =
        let@ v = exist in
        let+ (utys, (u' r)) = traverse us (fun vs ->
          let+ u' = hastype u v
          and+ r = k (v :: vs)
          in (u', r))
        in (u', (utys, r))
      in ((u', ty) :: utys, r)
  in
  let+ (utys, ()) = traverse us (fun vs ->
    w --- Infer.product vs)
  in F.Tuple utys
\end{lstlisting}
\end{minipage}
\hfill
\begin{minipage}{0.5\linewidth}
\begin{lstlisting}[basicstyle=\tiny\ttfamily]
| 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}
\end{frame}

\begin{frame}{Conclusion}
\begin{itemize}
\item Turning outputs into modal inputs improve readability
\item This programming trick applies to other code relying on
  applicative functors with quantifiers
\end{itemize}
\begin{block}{}
  Thank you for your attention !
\end{block}
\end{frame}

\end{document}