4 ms·
Idris: Type safe printf [video]
- ExpiredLink 12y agoIdris?
- berbc 12y agohttp://www.idris-lang.org http://www.idris-lang.org
- socceroos 12y agoMy mind immediately went to Star Citizen...
- wz1000 12y agoReally cool, but I am assuming printf only works for values which are determined at compile time?
- chriswarbo 12y agoAFAIK the value of the formatting string needs to be known at compile time. Only the types of the rest need to be known. Actually, 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.
- ufo 12y agoWhy define Format as data Format = FInt Format | FString Format | FOther Char Format | FEnd instead of using lists? data FormatPart = FInt | FString | FOther Char type Format = List FormatPart
- walrus 12y agoSeems to work fine: https://gist.github.com/anonymous/18e4d6823de55a4d0567 https://gist.github.com/anonymous/18e4d6823de55a4d0567
- wheaties 12y agoThis was awesome and yet one more reason to learn Idris. Now I have to see if it can be done in Scala.
- paulddraper 12y agoIt can, with macros. Though Scala's stri g interpolation will get you mostly there (correct number of arguments, local format specifiers that are harder to mess up).
- wheaties 12y agoMaybe it doesn't have to be with macros.
- bronty 12y agoYou can check format strings in Java at compile-time using the Checker Framework: http://types.cs.washington.edu/checker-framework/current/checker-framework-manual.html#formatter-checker http://types.cs.washington.edu/checker-framework/current/che... The format string semantics are actually pretty tricky because printf will perform conversions in certain cases.
- latkin 12y agoVery cool, Idris looks like a really interesting language. 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).
- mmavnn 12y agoHave a type provider ;) http://blog.mavnn.co.uk/type-safe-printf-via-type-providers/ http://blog.mavnn.co.uk/type-safe-printf-via-type-providers/ And yes: syntax is not quite so nice.