[jlturner]

Most functional languages have a type safe printf / sprintf (i.e. OCaml, F#, Haskell) which is similar to the effect you get in Idris: the types required to apply the function are statically analyzed from the format string.

Edit (links):

OCaml: https://caml.inria.fr/pub/docs/manual-ocaml/libref/Printf.ht...

F#: https://msdn.microsoft.com/en-us/visualfsharpdocs/conceptual...

Haskell: https://hackage.haskell.org/package/base-4.9.1.0/docs/Text-P...

[lkitching]

The Haskell version of printf does not statically analyse the format string and will raise an exception if the provided arguments are invalid e.g.

    Prelude Text.Printf> printf "%d\n" "invalid"
    *** Exception: printf: bad formatting char 'd'

The behaviour of F#'s printfn is hard-coded in the compiler and could not be written in F# iteself.

[cannam]

Aren't the Ocaml and F# examples relying on some dedicated compiler support for the format string type, though? The Idris example is interesting because its printf implementation can actually be written in Idris.

[lower]

The OCaml implementation used to be hard-coded in the type system, but has now been rewritten (in 4.02, I think) using GADTs.

https://ocaml.org/meetings/ocaml/2013/proposals/formats-as-g...

https://caml.inria.fr/mantis/view.php?id=6017

The compiler only does syntactic desugaring of format strings now.

[dllthomas]

> the types required to apply the function are statically analyzed from the format string.

Not so, in that Haskell package:

    Prelude Text.Printf> printf "%d\n" 1
    1
    Prelude Text.Printf> printf "%d\n"
    *** Exception: printf: argument list ended prematurely
    Prelude Text.Printf> printf "%d\n" 0.5
    *** Exception: printf: bad formatting char 'd'
    Prelude Text.Printf> printf "%d\n" 1 2
    1
    *** Exception: printf: formatting string ended prematurely

It could certainly be done with TH/QQ. I'm not sure, offhand, if there is already a package to that effect.

[hesselink]

There are several packages on hackage offering a type safe printf. Some use TH, some use variadic functions (defined with a type class) or other advanced type level features.

[dllthomas]

Variadic functions are used in the package under discussion, and don't get you compile time checking of the format string.

[mej10]

Sure, and I know about those. I wasn't claiming that this was only possible in Idris -- and I don't think their implementations are nearly as clean or straightforward as the one in Idris.

In Idris, the pattern used to implement this is available to anyone that knows the language. It feels a lot more natural than using a macro system or typeclasses -- it is just functions.

[mhh__]

One could also do this in D as well. it's not that impressive.