present Inferno

Gabriel Scherer 3 years ago
parent e5301ece17
commit f5c7d6ebb8

@ -1,6 +1,6 @@

@ -1 +1,3 @@

@ -14,6 +14,8 @@
% TODO use Software Heritage for software and code source citation
The \Inferno{} library~\citep*{inferno,inferno-code} uses an
applicative functor \lstinline{'a co} to represent constraint-based
@ -34,7 +36,9 @@
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.
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 may apply to any
applicative functors with quantifiers; it may exist in the wild or
@ -42,6 +46,91 @@
audience could be very valuable.
François Pottier's \Inferno{} 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
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 a ``witness'', of type \lstinline{'a},
that the 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:
In this document we will use the following running example, which is
adapted from a fragment of the coreML inference example.
On the right, we show the types of the combinators we use,
provided by \Inferno{}'s high-level layer:
let rec hastype (t : ML.term) (w : Infer.variable) : F.term co =
match t with
| [...]
| ML.Pair (u1, u2) ->
exists (fun v1 ->
exists (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)
val exists : (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
The function \lstinline{hastype : ML.term -> Infer.variable -> F.term co}
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; 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}.
The infix combinator \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 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{exists} 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.