Auteur : Gregoire Henry (PPS)

Titre : Experiments in generic programming: runtime type representation and implicit values

Abstract :

We present two ongoing related experiments in generic programming with
OCaml. In the first experiment, inspired from the implicit values of
Scala, the language is extended with primitives to enrich a locally
scoped environment of implicit values -- mapping types to values -- and a
construcion for synthesising a value of a given type from the
environment of implicit values. We have used this extension to
implement light-weight, semi-implicit type classes.

The second experiment is based on explicit runtime-type representa-
tion, described by a GADT, that can be analysed in a type-safe manner
to implement polytypic functions, defined by cases on the structure of
the types of their arguments.

Both experiments share a common set of non-intrusive extensions of
the OCaml compiler; in particular, the modication in the type checker
are simple, limited, and identical in both cases. This is because implicits
can be implemented modularly as an additional phase in the compilation
chain that comes right after type-checking.