I see there is a lot of enthusiasm for adding some form of type reflection to OCaml; that’s great! It is true that at LexiFi we have a tried-and-tested system in use for a long time. Let me try to give some perspective about it and answer some of the questions that came up:
-
The LexiFi patch actually consists of two parts: 1) the representation of types as an OCaml datatype; 2) a patch to the typechecker/middle end to have the compiler automatically generate type witnesses (as sketched above).
-
It is important to note that 1) is to an extent independent of 2); it comes down to giving a suitable definition of the “type of types”. I understand from past discussion that proposals in this direction would be welcome by the OCaml dev team. Accordingly, one should concentrate for the most part in 1) to make progress.
-
For historical reasons the LexiFi version of 1) (ie the type representation, see here and here) has a number of quirks. Furthermore, it makes design choices that may not be the best ones in general. For example, it only represents closed types: no type constructors or type variables can be represented, and so in particular neither can exotic types such as GADTs, first-class modules, extensible types, polymorphic variants, etc.
-
The main challenge in devising a suitable representation of types is deciding how to handle abstract types (see the paper and the slides I linked to in the other thread). At LexiFi abstract types are represented via “global names” (ie we identify an abstract type
M.tby its name"M.t"). This works reasonably well in practice, but is not a good solution in general (the notion of “name” for an abstract type is not well-defined). I suspect the answer may be something of a research problem… -
LexiFi did discuss upstreaming a version of its fork long time ago (~2011), but I suspect it wasn’t done mainly because of the theoretical shortcomings of the current implementation (eg handling of abstract types).
-
Accordingly, the LexiFi fork is not open-source: we don’t have the manpower to support it as an open-source project, we don’t want to release a version of this technology which has known limitations that make it easy to shot yourself in the foot if you don’t know what you are doing, and finally there are some commercial considerations to take into account (but my impression is that if this technology was polished enough that it could be accepted upstream, LexiFi would be happy to do so).
-
Personally, from a distance, GitHub - thierry-martinez/refl: OCaml PPX deriver for reflection looks rather interesting, but its type representation is quite complex and is not clear it can be made suitable for “practical” use.
I hope this answers some of the questions!
Cheers,
Nicolas