parent
f0def3cb4c
commit
b88bb546e5
@ -0,0 +1,30 @@
|
||||
The [Inferno](https://gitlab.inria.fr/fpottier/inferno) library uses an
|
||||
applicative functor `'a co` to represent constraint-based
|
||||
inference problems that elaborate into explicitly-typed term
|
||||
representations. A central operation of the Inferno API is the
|
||||
`exist` quantifier, which generates a fresh inference
|
||||
variable scoped in an existential constraint. `exist`
|
||||
returns the result of solving the constraint, as well as the
|
||||
elaborated type inferred for the inference variable:
|
||||
|
||||
```
|
||||
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.
|
Loading…
Reference in new issue