Live data from Hacker News

Idris: Type safe printf [video]

youtube.com

11–16 of 16 posts

Re: Idris: Type safe printf [video]

#11

This was awesome and yet one more reason to learn Idris. Now I have to see if it can be done in Scala.

It 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).

Re: Idris: Type safe printf [video]

#14

This was awesome and yet one more reason to learn Idris. Now I have to see if it can be done in Scala.

It 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).

Maybe it doesn't have to be with macros.

Re: Idris: Type safe printf [video]

#15
Very 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).

Re: Idris: Type safe printf [video]

#16
post #15

Very 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 f…

Have a type provider ;)

http://blog.mavnn.co.uk/type-safe-printf-via-type-providers/

And yes: syntax is not quite so nice.

Post reply on HN