111

Haskell's type safety is second to none only to dependently-typed languages. But there is some deep magic going on with Text.Printf that seems rather type-wonky.

> printf "%d\n" 3
3
> printf "%s %f %d" "foo" 3.3 3
foo 3.3 3

What is the deep magic behind this? How can the Text.Printf.printf function take variadic arguments like this?

What is the general technique used to allow for variadic arguments in Haskell, and how does it work?

(Side note: some type safety is apparently lost when using this technique.)

> :t printf "%d\n" "foo"
printf "%d\n" "foo" :: (PrintfType ([Char] -> t)) => t
undur_gongor
  • 15,657
  • 5
  • 63
  • 75
Dan Burton
  • 53,238
  • 27
  • 117
  • 198
  • 16
    You can only get a type safe printf using dependent types. – augustss Oct 19 '11 at 21:06
  • 10
    Lennart's quite right. Haskell's type safety is second to languages with even more dependent types than Haskell. Of course, you can make a printf-like thing type safe if you choose a more informative type than String for the format. – pigworker Oct 19 '11 at 21:29
  • 3
    see oleg for multiple variants of printf: http://okmij.org/ftp/typed-formatting/FPrintScan.html#DSL-In – sclv Oct 20 '11 at 15:16
  • Here is some Scala code that uses a _similar_ technique: http://scala-programming-language.1934581.n4.nabble.com/Simple-enough-to-describe-td2535027.html#a2535194. – missingfaktor Apr 21 '12 at 16:53
  • 1
    @augustss You can only get a type-safe printf using dependent types OR TEMPLATE HASKELL! ;-) – MathematicalOrchid Jan 05 '13 at 21:18
  • 3
    @MathematicalOrchid Template Haskell doesn't count. :) – augustss Jan 05 '13 at 22:08
  • 1
    Here's another take on printf without dependent types, on the MLton wiki about printf in Standard ML: http://mlton.org/Printf – okonomichiyaki Jun 03 '14 at 20:02

1 Answers1

137

The trick is to use type classes. In the case of printf, the key is the PrintfType type class. It does not expose any methods, but the important part is in the types anyway.

class PrintfType r
printf :: PrintfType r => String -> r

So printf has an overloaded return type. In the trivial case, we have no extra arguments, so we need to be able to instantiate r to IO (). For this, we have the instance

instance PrintfType (IO ())

Next, in order to support a variable number of arguments, we need to use recursion at the instance level. In particular we need an instance so that if r is a PrintfType, a function type x -> r is also a PrintfType.

-- instance PrintfType r => PrintfType (x -> r)

Of course, we only want to support arguments which can actually be formatted. That's where the second type class PrintfArg comes in. So the actual instance is

instance (PrintfArg x, PrintfType r) => PrintfType (x -> r)

Here's a simplified version which takes any number of arguments in the Show class and just prints them:

{-# LANGUAGE FlexibleInstances #-}

foo :: FooType a => a
foo = bar (return ())

class FooType a where
    bar :: IO () -> a

instance FooType (IO ()) where
    bar = id

instance (Show x, FooType r) => FooType (x -> r) where
    bar s x = bar (s >> print x)

Here, bar takes an IO action which is built up recursively until there are no more arguments, at which point we simply execute it.

*Main> foo 3 :: IO ()
3
*Main> foo 3 "hello" :: IO ()
3
"hello"
*Main> foo 3 "hello" True :: IO ()
3
"hello"
True

QuickCheck also uses the same technique, where the Testable class has an instance for the base case Bool, and a recursive one for functions which take arguments in the Arbitrary class.

class Testable a
instance Testable Bool
instance (Arbitrary x, Testable r) => Testable (x -> r)
hammar
  • 138,522
  • 17
  • 304
  • 385
  • Great answer. I just wanted to point out that haskell is figuring out the type of Foo based on the arguments applied. To understand this, you might want to specify the type of Foo explicity as follows: λ> (foo :: (Show x, Show y) => x -> y -> IO ()) 3 "hello" – redfish64 Aug 13 '18 at 11:46
  • 1
    While I understand how the variable length argument part is implemented, I still don't understand how the compiler rejects `printf "%d" True`. This is very mystical to me, as it seems that the runtime(?) value `"%d"` gets deciphered at compile time to require an `Int`. This is absolutely baffling to me . . . especially since the source code doesn't use things like `DataKinds` or `TemplateHaskell` (I checked the source code, but didn't comprehend it.) – Thomas Eding Mar 23 '19 at 15:13
  • 2
    @ThomasEding The reason the compiler rejects `printf "%d" True` is because there's no `Bool` instance of `PrintfArg`. If you pass an argument of the wrong type that _does_ have an instance of `PrintfArg`, it does compile and throws an exception at runtime. Ex: `printf "%d" "hi"` – Travis May 10 '19 at 14:42