5 ms·

> 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

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

wk_end 8y ago
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 8y ago
  >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 8y 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_type https://en.wikipedia.org/wiki/Generalized_algebraic_data_typ... [2] https://caml.inria.fr/pub/docs/manual-ocaml/libref/CamlinternalFormatBasics.html#TYPEfmt https://caml.inria.fr/pub/docs/manual-ocaml/libref/Camlinter...
ihm 8y ago
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/module/gadts.ml https://github.com/bobzhang/ocaml-book/blob/master/lang/code...

wk_end 8y ago

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 8y ago
>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 8y 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_type https://en.wikipedia.org/wiki/Generalized_algebraic_data_typ... [2] https://caml.inria.fr/pub/docs/manual-ocaml/libref/CamlinternalFormatBasics.html#TYPEfmt https://caml.inria.fr/pub/docs/manual-ocaml/libref/Camlinter...

ihm 8y ago

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/module/gadts.ml https://github.com/bobzhang/ocaml-book/blob/master/lang/code...