Type-safe printf, using runtime provided strings. An extension on https://gist.github.com/puffnfresh/11202637

Main.idr

module Main

%default total

data Format
  = FInt -- %d
  | FString -- %s
  | FOther Char -- [a-zA-Z0-9]

format : List Char -> List Format
format ('%'::'d'::cs) = FInt :: format cs
format ('%'::'s'::cs) = FString :: format cs
format (c::cs) = FOther c :: format cs
format [] = []

interpFormat : List Format -> Type
interpFormat (FInt :: f) = Int -> interpFormat f
interpFormat (FString :: f) = String -> interpFormat f
interpFormat (FOther _ :: f) = interpFormat f
interpFormat [] = String

formatString : String -> List Format
formatString s = format (unpack s)

toFunction : (fmt : List Format) -> String -> interpFormat fmt
toFunction (FInt :: f) a = \i => toFunction f (a ++ show i)
toFunction (FString :: f) a = \s => toFunction f (a ++ s)
toFunction (FOther c :: f) a = toFunction f (a ++ singleton c)
toFunction [] a = a

printf : (s : String) -> interpFormat (formatString s)
printf s = toFunction (formatString s) ""

runFormat : (fmt : List Format) -> interpFormat fmt -> IO ()
runFormat [] f =
  putStrLn f
runFormat (FInt :: xs) f = do
  putStr "Enter an integer: "
  s <- getLine
  runFormat xs (f (cast s))
runFormat (FString :: xs) f = do
  putStr "Enter a string: "
  s <- getLine
  runFormat xs (f s)
runFormat (FOther _ :: xs) f =
  runFormat xs f

main : IO ()
main = do
  putStr "Your printf string: "
  s <- getLine
  runFormat (formatString s) (printf s)