Hacker News new | ask | show | jobs
by star-castle 2937 days ago
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.
1 comments
lomnakkus 2937 days ago
> 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.

link
ihm 2936 days 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...
link
wk_end 2937 days 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".
link
mixedCase 2936 days 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 :)

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

link