Skip to content

Instantly share code, notes, and snippets.

@chrisdone
Last active May 27, 2024 13:01
Show Gist options
  • Save chrisdone/672efcd784528b7d0b7e17ad9c115292 to your computer and use it in GitHub Desktop.
Save chrisdone/672efcd784528b7d0b7e17ad9c115292 to your computer and use it in GitHub Desktop.
Type-safe dependently-typed printf in Idris
module Printf
%default total
-- Formatting AST.
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)))
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.
formatString : String -> Format
formatString s = format ( unpack s )
-- Convert a format AST into a type.
-- Example: FInt (FOther ',' (FString FEnd)) → Int -> String -> String
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
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
printf : (s : String) -> interpFormat ( formatString s )
printf s = toFunction ( formatString s ) ""
*Printf> :l Printf
Type checking ./Printf.idr
*Printf> :t printf "%d%s"
printf "%d%s" : Int -> String -> String
*Printf> :t printf "%d%s" 5
printf "%d%s" 5 : String -> String
*Printf> :t printf "%d%s" 5 "hello!"
printf "%d%s" 5 "hello!" : String
*Printf> printf "%d%s" 5 "hello!"
"5hello!" : String
*Printf> printf "%d: %s" 5 "hello!"
"5: hello!" : String
*Printf> printf "%d: %s" "woops" 6
builtin:Type mismatch between
String (Type of "woops")
and
Int (Expected type)
@paulosuzart
Copy link

Hi, I've written a blog post on top of your code. Really neat.
http://paulosuzart.github.io/blog/2017/06/18/dependent-types-and-safer-code/

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment