Haskell printf arguments as array

Question

I want to call Text.Printf function printf with array but I can't find a way. Here are two not working versions (actually same idea).

import Text.Printf

printfa :: (PrintfArg a) => String -> [a] -> String
printfa format args = step (printf format) args
  where
    step :: (PrintfType r, PrintfArg a) => r -> [a] -> r
    step res (x:[]) = res x
    step res (x:xs) = step (res x) xs

printfa' :: (PrintfArg a) => String -> [a] -> String
printfa' format args = foldr (\arg p -> p arg) (printf format) args

main = putStrLn $ printfa "%s %s" ["Hello", "World"]

GHC errors are:

printfa.hs:8:23:
    Couldn't match type `r' with `a1 -> r'
      `r' is a rigid type variable bound by
          the type signature for
            step :: (PrintfType r, PrintfArg a1) => r -> [a1] -> r
          at printfa.hs:8:5
    The function `res' is applied to one argument,
    but its type `r' has none
    In the expression: res x
    In an equation for `step': step res (x : []) = res x

printfa.hs:12:41:
    The function `p' is applied to one argument,
    but its type `String' has none
    In the expression: p arg
    In the first argument of `foldr', namely `(\ arg p -> p arg)'
    In the expression: foldr (\ arg p -> p arg) (printf format) args

(Why: I'm writing DSL and want to provide printf function.)

Answer 1

First, realize that PrintfArg a => [a] is not a heterogenous list. That is, even though Int and String are both instances of PrintfArg, [ 1 :: Int, "foo" ] is not a valid construct.

So if you did define a function :: PrintfArg a => String -> [a] -> String, that all the args would be constrained to be of the same type.

To get around this, you can use existential quantification.

{-# LANGUAGE ExistentialQuantification #-}
import Text.Printf

data PrintfArgT = forall a. PrintfArg a => P a

printfa :: PrintfType t => String -> [ PrintfArgT ] -> t
printfa format = printfa' format . reverse
  where printfa' :: PrintfType t => String -> [ PrintfArgT ] -> t
        printfa' format [] = printf format
        printfa' format (P a:as) = printfa' format as a

main = do
  printfa "hello world\n" []
  printfa "%s %s\n" [ P "two", P "strings"]
  printfa "%d %d %d\n" (map P $ [1 :: Int, 2, 3])
  printfa "%d %s\n" [ P (1 :: Int), P "is the loneliest number" ]

The reason your first solution didn't work is because you passed res to step as an argument.

When you have foo :: Constraint a => a -> t you guarantee that foo will work on all instances of Constraint. And though there exists an instance of PrintfType which can take an argument, not all instances can. Thus your compiler error.

In contrast, when you have foo :: Constraint a => t -> a, you guarantee that foo will return any desired instance of Constraint. Again, the caller gets to choose which instance. This is why my code works - when printfa' recurses, it requires the recursive call to return a value from the (PrintfArg a, PrintfType t) => a -> t instance.

For your second try, the compiler complains because foldr requires that the accumulated value be of the same type between iterations. GHC notices that the accumulated value must be a function type (PrintfArg a, PrintfType t) => a -> t, because you apply it in the iterated function. But you return the applied value, which it can figure out is of type t. This means that t equals a -> t, which GHC doesn't like, because it doesn't allow infinite types. So it complains.

If you want to use a fold, you can, you just have to mask the accumulator type using Rank2Types or RankNTypes to keep the type constant between iterations.

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE RankNTypes #-}
import Text.Printf

data PrintfArgT = forall a. PrintfArg a => P a
data PrintfTypeT = T { unT :: forall r. PrintfType r => r }

printfa :: PrintfType t => String -> [ PrintfArgT ] -> t
printfa format = unT . foldl (\(T r) (P a) -> T $ r a ) (T $ printf format)

Answer 2

I'm not sure this is a minimal solution, but if you know the length of your vectors statically you can use type-indexed Vectors and type indexed Fun types.

{-# LANGUAGE GADTs, TypeFamilies #-}

import Text.Printf

data Z
data S n

data Vec n a where
  Nil  :: Vec Z a
  Cons :: a -> Vec n a -> Vec (S n) a

type family Fn n b a
type instance Fn Z b a = a
type instance Fn (S n) b a = b -> Fn n b a

-- in order to tell the compiler that we want to consider a function as a `Fn`
newtype Fun n b a = Fun (Fn n b a)

run :: Fun n b a -> Vec n b -> a
run (Fun f) v = case v of
  Nil         -> f
  Cons b more -> run (Fun $ f b) more

z :: Vec (S (S Z)) String
z = Cons "foo" (Cons "bar" Nil)

then you can do run (Fun $ printf "%s %s") z.