printf-safe- Type safe interface for Text.Printf

Copyright(C) 2016 Csongor Kiss
MaintainerCsongor Kiss <>
Safe HaskellSafe




A type-safe interface for Text.Printf that ensures at compile-time that the number and type of arguments passed to printf matches the format specifier.

Thus, the specifier is lifted to the type-level and can be composed manually using the (%) type-level function, or with the (%) term-level function.

Note that while the term-level composition retains type-safety, it does not provide a way to define string literals within the format string, those must be passed on as an argument to printf in that case.

Specifiers composed at the type-level can be bound to terms using the Template' proxy (as they are not of kind *), and those terms can then be further composed with each other.


Safe printf

printf Source


:: (FoldToString (FormatList a), PrintfType (PrintfType a)) 
=> proxy a

Witness the Format list. The proxy is usually a Template'.

-> PrintfType a

The constructed type for printf

The printf frontend.

a is of kind [Format]. It is first turned into a list of format specifiers (the literals are kept in place), then the format string is constructed from it.


printf (Template :: Template ("hex: " % 'Hex % " binary: " % 'Binary)) 500 500

generates a format string "hex: %x binary: %b", and calls the internal printf with the format string and the provided arguments.

Format template

type family Template a :: * Source

Type family that produces a proxy (Template') from any compatible template candidate.

This way, we can have produce templates from single types, as in

Template :: Template Int

which acts as a `%d' specifier, or

Template :: Template ('Hex % Int)

which is a "%x %d" format string. (see composition below).


Template (a :: [Format]) = Template' a 
Template (a :: Format) = Template' `[a]` 
Template (a :: FormatSpec) = Template' `[ToFormat a]` 
Template (a :: *) = Template' `[ToFormat a]` 
Template (a :: Symbol) = Template' `[ToFormat a]` 

data Template' f Source

Fixed-kinded proxy for storing a list of Formats for printf



Formatting options

data FormatSpec Source

Format specifiers that are not directly tied to a type. For example, Hex (%x) belongs here, but Int (%d) doesn't. These constructors are used ticked, promoting FormatSpec to its own kind.



%x (requires an Int)


%b (requires an Int)


%o (requires an Int)


%e (requires a Double)

Format template composition


type family e % ls :: [Format] infixr 5 Source

Acts like a cons function for Format lists, first turning the the new head element into a Format. (since it can be a string literal (kind Symbol), for example, or a Haskell type (kind *)).

Because the Template type family is poly-kinded, it supports both lists and singular format specifiers. Composition produces lists.

format :: Template (Int % "in base 16 is: " % 'Hex)
format = Template

printf format 50 50


e % (ls :: [Format]) = ToFormat e : ls 
e % ls = ToFormat e : `[ToFormat ls]` 


(%) :: Template' a -> Template' b -> Template (a :++ b) infixr 5 Source

Composes two templates.

Given two terms representing templates, simply appends them to produce a new term representing the composition.

format :: Template (Int % " in base " % Int % " is: ")
format = Template

hex :: Template 'Hex
hex = Template

printf (format % hex) 30 16 30

which yields the same result as calling printf as such:

Text.Printf.printf "%d in base %d is: %x" 30 16 30

(<%>) :: Template' a -> Template' b -> Template (a :++ (Lit " " : b)) Source

Same as (%), but inserts a space in between the two formats.

Term-level combinators

hex :: Template Hex Source

Term-level representation of a 'Hex (hexadecimal) specifier for composition.


printf hex 35

oct :: Template Oct Source

Term-level representation of an 'Oct (octal) specifier for composition.

binary :: Template Binary Source

Term-level representation of a 'Binary specifier for composition.

sci :: Template Sci Source

Term-level representation of an 'Sci (scientific) specifier for composition.

string :: Template String Source

Term-level representation of a String specifier for composition.

This will not generate string literals in the format string (as that's only possible at the type-level), but insert a `%s' specifier and modify the type of printf accordingly, so it is useful when the string is not known at compile time.


printf string "example"

This means this is the same as calling

Text.Printf.printf "%s" "example"