Type functions at run-time in Idris

Question

I've going over Type-driven development, and there is a section on a well-typed printf, where the type is calculated from the first argument which is a format string:

printf : (fmt : String) -> PrintfType (toFormat (unpack fmt))

toFormat creates a format representation out of a List Char and PrintfType creates a function type out of such a format representation. The full code is here: https://github.com/edwinb/TypeDD-Samples/blob/master/Chapter6/Printf.idr

I understand what's going on with code like printf "%c %c" 'a' 'b'--the type of printf "%c %c is calculated to be Char -> Char -> String.

What I don't understand is what happens when the first argument is unknown at run-time. I understand why in general such code should not compile: the format string, and the resulting type, cannot be known at compile-time if they are entered by a user at run-time, but I don't know the actual technical reasoning behind this intuition.

For example:

main : IO ()
main = do fmt <- getLine
          c1 <- getChar
          c2 <- getChar
          printf fmt c1 c2

Results in the following error message:

When checking an application of function Prelude.Monad.>>=:
        printf fmt does not have a function type (PrintfType (toFormat (unpack fmt)))

I guess I'm trying to understand this error message. Does Idris treat functions like this as a special case?

Answer 1

The type of printf fmt : PrintfType (toFormat (unpack fmt)) cannot be further evaluated, because fmt : String is not known at compile-time. So for Idris this is not a function – it's A instead of A -> B. That's what the error message is saying.

For your case, you have to check at run-time if PrintfType (toFormat (unpack fmt)) is String -> String.

As an example, here are two functions that take a format and maybe return a proof that it's the right format:

endFmt : (fmt : Format) -> Maybe (PrintfType fmt = String)
endFmt End = Just Refl
endFmt (Lit str fmt) = endFmt fmt
endFmt fmt = Nothing

strFmt : (fmt : Format) -> Maybe ((PrintfType fmt) = (String -> String))
strFmt (Str fmt) = case endFmt fmt of
  Just ok => rewrite ok in Just Refl
  Nothing => Nothing
strFmt (Lit str fmt) = strFmt fmt
strFmt fmt = Nothing

We then can call strFmt with toFormat (unpack fmt) and have to handle both Maybe cases. Because Idris has problems applying the proof, we help with replace.

main : IO ()
main = do fmt <- getLine
          str <- getLine
          case strFmt (toFormat (unpack fmt)) of
            Just ok => let printer = replace ok {P=id} (printf fmt) in
              putStrLn $ printer str
              -- in a better world you would only need
              -- putStrLn $ printf fmt str
            Nothing => putStrLn "Wrong format"

With this we can run:

:exec main
foo %s bar  -- fmt
and         -- str
foo and bar -- printf fmt str