As mentioned already by @Levi_Roth the/one way to introduce “runtime type information” into ML is not to make values carry type information at runtime but rather make it possible to represent types themselves as values, say of a type 'a ty. Then the compiler can expose an operator val typeof: 'a -> 'a ty that builds the value representing the type of the argument. If you have this you can pretty much build everything else deriving-related on user space. That’s the easy part. The hard part is finding the right definition of 'a ty.
How would the compiler expose such a typeof operator in the first place? If a value does not carry its type, then this operator cannot exist at runtime. It is necessarily a pure compile-time construction. And thus it would only work in a monomorphic context. It is impossible to use such an operator to write a polymorphic function print: 'a -> unit.
Note that I am purposely ignoring OCaml’s objects here. Since they have associated runtime type information, the typeof operator can be defined for them. In a sense, the situation is quite similar to C++. If you invoke operator typeid on an object with some virtual methods, you get the actual dynamic type of the expression. Otherwise, you get its static type, which is pointless unless the code is templated.
You are right, I was a overly inprecise here. Indeed this “operator” should be of the form [%t: T] where T is an arbitrary type expression and which returns a value of type T ty, eg [%t: int * int] is a value of type (int * int) ty “representing” int * int.
Right, the signature of the “polymorphic” print function would not be print: 'a -> unit but print : 'a ty -> 'a -> unit. The idea is that in principle each call site is of the form print [%t: T] x where T is a type expression equivalent to the type of x, eg print [%t: int * int] (2, 3). In fact, the first argument can be essentially elided by using unification: print [%t: _] (2, 3), and the compiler can offer special support to avoid having to write it at all to begin with.
The system I described above is roughly the battle-tested one we have at LexiFi and it works really well even if it has some important limitations (can only represent closed types and its interaction with abstract types is a bit hacky). There are other possible approaches of course, but am not very familiar with them.
I could use the same argument about any abstraction or module interface. What is the implementation actually being used? Any language feature requires experience to apply it appropriately. As someone with Haskell and OCaml experience, I can say that ad-hoc overloading can make code much easier to both read and write. In Haskell, to map over anything it’s just “fmap”, to show anything it’s just “show”, or for equality it’s (==).
Modular implicits and type-classes also offer “type-derived” code. For example, one can just use (==) on lists and the correct equality is derived from the underlying types, no additional comparison arguments need to be threaded everywhere. Similarly for fmap.
Interesting! I guess that in this language extension, the compiler rejects the following code:
let f x = print [%t: _] x
because the type to be reflected is not ground? But you’d solve this by threading the type reflection:
let f a x = print a x
Now I’m curious as to how your language extension compares to a typeclass mechanism. The way you describe it, I’m under the impression that it comes (relatively) easily as a by-product of the existing typechecker (so definitely less powerful than typeclasses)?
Another way to put my question: what happens to something like:
let f (a : 'a ty) (x : 'a) = print <???> (Some x)
? Can you have the type reflection for 'a option be synthesized from the one available in context for 'a? If not, I guess you’d work around it by threading along a type reflection for 'a option, and accept that it leaks implementation details.
Note that except for the magic 'a -> 'a ty or if you want automated derivation of these values, you don’t need a language extension at all. This all happens in your rich Meta Language.
Personally I would be entirely happy to write these values by hand as needed – if only to be able to migrate my data representations easily without having to keep my previous data type definitions around.
If there was a good 'a ty in the stdlib, I would at least write them only once, and they would still work in 20 years which is worth the boring, but little, time investment. For now I have to write the same boilerplate code for the many type indexed combinators that I use (formatters, serializers, equality, comparison, random value generators, etc.) and these definitions are not open to new uses (e.g. for the day JSON will be replaced by the next half-broken but hyped serialization format).
I look forward to the day I can replace my M.pp values by M.typ values.
Overloading or deriving are complex changes, adding 'a Stdlib.Typ.t is a simple one that requires no language support with a great usability impact on the eco-system. But as @nojb mentioned the problem is finding a good definition for the type; see the discussion @Levi_Roth pointed to for a few references.
For the [%debug: expr] feature, I would recommend you all interested in deriving from types to try playing with typedppxlib this kind of thing is very easy to get started, and a half baked solution on userspace is feasible. And it works from 4.08 to 4.13 IIRC, not sure about Windows.
There is a joke example ppx_overload on how this could be done in a bad way but it’s definitely not something for production, it could be useful for production if it handled type constructors at least.
A big problem of this one is that there will be the problem of shadowing, which I don’t think it’s possible to bypass for cases with a type constructor.
As @nojb mentioned describing a good 'a ty is annoying, that’s also why making a ppx_typeof using typedppxlib is very annoying. Printing the type to a string is very easy tho.
I think OCaml has a unique place relative to several other languages, and an advantage in that it’s so explicit - while having certain simple things be implicit. I think it’s a delicate balance - and it’s easy to lose this quality of the right amount of explicitness vs implicitness.
As the thread was initiated by the sentence:
… I would like to point out typed effects as an alternative focus that I think fits OCamls explicitness-balance, and its tendency to focus on safe FP better. That exceptions suddenly would become tracked by the typesystem I think would lift OCaml to an even higher, unique, place as a language - relative to its competitors.
When I chose my primary language to begin with, I would probably have chosen Haskell if I actually wanted Haskells typeclasses, rather than the explicit style of OCaml.
My overall takeaway: see OCaml as a unique tool that deserves a unique evolution. Of course, easy things should be easy - but as others have pointed out, there are several ways to better support serialization, show etc.
I don’t write that. I argue for what feature would fit OCaml better than modular implicits, and support alternative proposals for deriving, show etc. that others have already mentioned in this thread