5 ms·

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 app

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.html https://caml.inria.fr/pub/docs/manual-ocaml/libref/Printf.ht... F#: https://msdn.microsoft.com/en-us/visualfsharpdocs/conceptual/core.printf-module-%5Bfsharp%5D https://msdn.microsoft.com/en-us/visualfsharpdocs/conceptual... Haskell: https://hackage.haskell.org/package/base-4.9.1.0/docs/Text-Printf.html https://hackage.haskell.org/package/base-4.9.1.0/docs/Text-P...

lkitching 9y ago
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.
dllthomas 9y ago
> 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 9y ago
  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 9y ago
    Variadic functions are used in the package under discussion, and don't get you compile time checking of the format string.
cannam 9y ago
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 9y ago
  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-gadts.pdf https://ocaml.org/meetings/ocaml/2013/proposals/formats-as-g... https://caml.inria.fr/mantis/view.php?id=6017 https://caml.inria.fr/mantis/view.php?id=6017 The compiler only does syntactic desugaring of format strings now.
mhh__ 9y ago
One could also do this in D as well. it's not that impressive.
mej10 9y ago
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.

lkitching 9y ago

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.

dllthomas 9y ago

> 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 9y ago
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 9y ago
  Variadic functions are used in the package under discussion, and don't get you compile time checking of the format string.

cannam 9y ago

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 9y ago
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-gadts.pdf https://ocaml.org/meetings/ocaml/2013/proposals/formats-as-g... https://caml.inria.fr/mantis/view.php?id=6017 https://caml.inria.fr/mantis/view.php?id=6017 The compiler only does syntactic desugaring of format strings now.

mhh__ 9y ago

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

mej10 9y ago

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.