|
|
|
|
|
|
by wk_end
2931 days ago
|
|
|
(sorry for the late reply, I didn't see this) The magic that's happening in the ocaml compiler isn't dependent typing - it's a purely syntactic transformation, something like GHC turning "hello" into ['h', 'e', 'l', 'l', 'o'] into 'h':'e':'l':'l':'o':[]. ocaml notices that you have a string literal in a place where a format string is expected and swaps it out - that's all. It's magic, but it's unrelated to the type system - the type system comes in later. What does it replace it with? A value of type ('a, 'b, 'c, 'd, 'e', f) fmt. fmt is a GADT [1], fully defined within ocaml [2] - and I promise, ocaml does not have full dependent types. [1] https://en.wikipedia.org/wiki/Generalized_algebraic_data_typ... [2] https://caml.inria.fr/pub/docs/manual-ocaml/libref/Camlinter... |
|
|