[lomnakkus]

> OCaml has a type-safe printf and isn't purely functional.

Isn't that a non-extensible built-in that's handled "magically" by the compiler? (Apologies if that's wrong, it's been a few years since I've used O'Caml.)

In Idris it's possible to write a type-safe printf entirely in library code -- no magic.

[ihm]

You can almost do this in OCaml using GADTs. The only trouble is you won't get nice "string syntax" for your format specifier. The idea can be seen here: https://github.com/bobzhang/ocaml-book/blob/master/lang/code...

[wk_end]

IIRC the only magic is in parsing the format string to a structured representation of it; but that format object is a normal ocaml value and the actual typechecking happens without any "magic".

[mixedCase]

>the only magic is in parsing the format string to a structured representation of it

That's the "magic" being discussed, where the value determines the type of something, hence, dependent typing :)

[wk_end]

(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...