Type-safe printf in Idris including a practical run-time validation example -- https://zgcoder.net/ramblings/typesafe-printf.html

printf_ex.idr

%default total

Prefix : Type
Prefix = String

data Format = Number Prefix Format | Str Prefix Format | End Prefix

parse : List Char -> String -> Format
parse [] prefix_acc = End prefix_acc
parse ('%' :: 'd' :: xs) prefix_acc = Number prefix_acc (parse xs "")
parse ('%' :: 's' :: xs) prefix_acc = Str prefix_acc (parse xs "")
parse (x :: xs) prefix_acc = parse xs (prefix_acc ++ strCons x "")

parseFormat : String -> Format
parseFormat xs = parse (unpack xs) ""

PrintfType : Format -> Type
PrintfType (Number _ format) = Int -> PrintfType format
PrintfType (Str _ format) = String -> PrintfType format
PrintfType (End _) = String

printfFormat : (format : Format) -> String -> PrintfType format
printfFormat (Number prefix' format) acc =
    \num => printfFormat format (acc ++ prefix' ++ show num)
printfFormat (Str prefix' format) acc =
    \str => printfFormat format (acc ++ prefix' ++ str)
printfFormat (End prefix') acc = acc ++ prefix'

printfFormatter : (format : Format) -> PrintfType format
printfFormatter format = printfFormat format ""

printf : (str : String) -> PrintfType (parseFormat str)
printf str = printfFormatter (parseFormat str)

formatSingleNumber : String -> Maybe String
formatSingleNumber str =
    let format = parseFormat str in
    case format of
        numberFormat@(Number _ (End _)) =>
            Just (printfFormatter numberFormat 999)
        _ => Nothing

main : IO ()
main = do
    putStrLn "Translate in your language of choice:"
    putStrLn "I have %d ponies"
    translation <- getLine
    case formatSingleNumber translation of
          Nothing => putStrLn "Invalid response!"
          (Just result) => putStrLn result