Typed printf with runtime format string

Main.idr

module Main

import Printf

%default total

||| Define the "like" relationship on two `Format`.
||| 
||| One format is "like" the other one iff the former with all non-format-specifier removed is
||| the same as the later.
data FmtLike : Format -> Format -> Type where
  LikeInt : FmtLike a b -> FmtLike (FInt a) (FInt b)
  LikeString : FmtLike a b -> FmtLike (FString a) (FString b)
  LikeOther : (c : Char) -> FmtLike a b -> FmtLike (FOther c a) b
  LikeEnd : FmtLike FEnd FEnd

||| Determine whether a `Format` is "like" another one in run-time,
||| return the proof if it is.
isLike : (a : Format) -> (b : Format) -> Maybe (FmtLike a b)
isLike (FInt     a) (FInt      b) = LikeInt <$> isLike a b
isLike (FString  a) (FString   b) = LikeString <$> isLike a b
isLike (FOther c a) b             = LikeOther c <$> isLike a b
isLike FEnd         FEnd          = Just LikeEnd
isLike _            _             = Nothing

||| Proof that if a `Format` is "like" another one, they will produce the same `printf` type.
fmtLikeHasSameArgs :
  (a : Format) -> (b : Format) -> FmtLike a b ->
  interpFormat a = interpFormat b
fmtLikeHasSameArgs (FInt     a) (FInt    b) (LikeInt     prf) = rewrite fmtLikeHasSameArgs a b prf in Refl
fmtLikeHasSameArgs (FString  a) (FString b) (LikeString  prf) = rewrite fmtLikeHasSameArgs a b prf in Refl
fmtLikeHasSameArgs (FOther c a) b           (LikeOther c prf) = rewrite fmtLikeHasSameArgs a b prf in Refl
fmtLikeHasSameArgs FEnd         FEnd        LikeEnd           = Refl

printfLike' :
  (fmt : Format) -> (fmtPat : Format) ->
  Either String (interpFormat fmtPat)
printfLike' fmt fmtPat = case fmt `isLike` fmtPat of
  Nothing  => Left "Invalid format string"
  Just prf => Right $
    rewrite sym (fmtLikeHasSameArgs fmt fmtPat prf) in
    toFunction fmt ""

||| Printf with runtime `fmt` which should be "like" `fmtPat`.
printfLike :
  (fmt : String) -> (fmtPat : String) ->
  Either String (interpFormat (formatString fmtPat))
printfLike fmt fmtPat = printfLike' (formatString fmt) (formatString fmtPat)

main : IO ()
main = do
  line <- getLine
  case printfLike line "%s%d" of
    Right p => putStrLn $ p "oxa" 42
    Left err => putStrLn err

Printf.idr

||| Typed printf
|||
||| From: https://gist.github.com/chrisdone/672efcd784528b7d0b7e17ad9c115292
module Printf

%default total

-- Formatting AST.
public export
data Format
  = FInt Format
  | FString Format
  | FOther Char Format
  | FEnd

-- Parse the format string (list of characters) into an AST.
-- Example: "%d,%s"  →   (FInt (FOther ',' (FString FEnd)))
public export
format : List Char -> Format
format ('%' :: 'd' :: cs ) = FInt ( format cs )
format ('%' :: 's' :: cs ) = FString ( format cs )
format ( c :: cs )         = FOther c ( format cs )
format []                  = FEnd

-- Convenience function to unpack a string into a list of chars, then
-- run format on it.
public export
formatString : String -> Format
formatString s = format ( unpack s )

-- Convert a format AST into a type.
-- Example: FInt (FOther ',' (FString FEnd))   →   Int -> String -> String
public export
interpFormat : Format -> Type
interpFormat (FInt f)     = Int -> interpFormat f
interpFormat (FString f)  = String -> interpFormat f
interpFormat (FOther _ f) = interpFormat f
interpFormat FEnd         = String

-- Dependently-typed part: turn a formatting AST into a well-typed
-- function accepting n arguments.
-- Example:
--      toFunction (FInt (FString FEnd))
--    →
--      \a i s => a ++ (show i) ++ s
export
toFunction : (fmt : 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 FEnd a           = a

-- Dependently-typed part: turn a formatting string into a well-typed
-- function accepting n arguments.
-- Example: printf "%d%s" → \i s => (show i) ++ s
export
printf : (s : String) -> interpFormat ( formatString s )
printf s = toFunction ( formatString s ) ""