Not exactly.
We don’t attach type information to values directly, as we don’t want to modify the runtime model of OCaml (also, this would only work with heap-allocated values, which would all become larger).
What we do instead is that when a function has a labeled, non-optional argument of type 'a ttype
(here 'a ttype
is the “type of types” with constructors corresponding to each kind of type in OCaml) and the argument is not passed explicitly, then the compiler synthetizes it at each callsite.
Concretely, if we define a function of the form
let show ~(t: 'a ttype) (x: 'a) : string =
match t with
| Int -> string_of_int x
| String -> x
| ...
And we call it with show 42
, the compiler inserts ~t:Int
as first argument. For efficiency, type witnesses (the values of type 'a ttype
) are actually computed at compilation-time whenever possible.
Makes sense?
Cheers,
Nicolas