Experiments in generic programming: runtime type representation and implicit values by Gregoire Henry

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 representation, 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.

Speaker: Gregoire Henry (PPS)