Idris: Type safe printf [video]
youtube.com
youtube.com
The format string semantics are actually pretty tricky because printf will perform conversions in certain cases.
F#'s standard printf-family functions are all type-safe in exactly the same way. This requires special support by the compiler, though, as F#'s type system is not as powerful. Most of the plumbing is standard, but the conversion from string literal to PrintfFormat at compile time is only possible due to hardcoded magic. You can't get exactly the same effect from plain user code, though you could certainly get something very close using a Type Provider (the syntax would just be a bit clunkier).
http://blog.mavnn.co.uk/type-safe-printf-via-type-providers/
And yes: syntax is not quite so nice.
data Format = FInt Format
| FString Format
| FOther Char Format
| FEnd
data FormatPart = FInt | FString | FOther Char
type Format = List FormatPartActually, since it's dependently typed, we don't actually need to know the value of the formatting string; we just need a proof that the formatting string will match the other values. The easiest way to do this is to know what the string is, but we could also, for example, get these values from a function, then prove that the function produces matching values.