Things that Idris improves things over Haskell

Re:Things that Idris improves things over Haskell by dllthomas on Friday June 16, 2017 @11:21AM (#14569761)

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

[ Parent | on HN ]

Re:Things that Idris improves things over Haskell by hesselink on Friday June 16, 2017 @11:45AM (#14569959)

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.

[ Parent | on HN ]

Re:Things that Idris improves things over Haskell by dllthomas on Friday June 16, 2017 @12:09PM (#14570153)

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

[ Parent | on HN ]