This commit is contained in:
Gabriel Scherer 2020-05-29 10:23:09 +02:00
parent d265153007
commit e5301ece17
2 changed files with 62 additions and 0 deletions

View File

@ -0,0 +1,15 @@
@inproceedings{inferno,
author = {François Pottier},
title = {{Hindley-Milner} elaboration in applicative style},
booktitle = {ICFP},
month = sep,
year = 2014,
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-elaboration.pdf},
soft = {https://gitlab.inria.fr/fpottier/inferno},
}
@misc{inferno-code,
author = {François Pottier},
title = {the {Inferno} library: \url{https://gitlab.inria.fr/fpottier/inferno}},
year = 2014,
}

View File

@ -0,0 +1,47 @@
\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
\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 combinator of the \Inferno{} API is the
\lstinline{exists} quantifier, which generates a fresh inference
variable scoped in an existential constraint. \lstinline{exists}
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}
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.
We believe that the API design pattern we propose may apply to any
applicative functors with quantifiers; it may exist in the wild or
benefit other projects. Experience sharing with the ML Workshop
audience could be very valuable.
\end{abstract}
\bibliography{biblio}
\end{document}