Hacker News Reader

Comment by star-castle | Hacker News Reader

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

ATS is essentially 'C with dependent types'. And optionally some other languages with dependent types. You can think of its dependent type checking and theorem-proving as 'pre-compilation', since there's no runtime overhead to it (and since you can separate it out into its own compilation step, including swapping out alternative solvers). ATS's relationship with C is good enough that you can take an arbitrary C program and start tightening its screws by injecting a bit of ATS into it.

View on HN

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

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

>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 :)

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

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

Reply on news.ycombinator.com