Idris: Type safe printf [video]

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.

Re: Idris: Type safe printf [video]

#8

Post by ufo » Sun, Dec 28, 2014, 1:55 PM UTC

Why 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

Re: Idris: Type safe printf [video]

#9

Post by walrus » Sun, Dec 28, 2014, 2:22 PM UTC

ufo wrote: post #8

Why 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

Seems to work fine: https://gist.github.com/anonymous/18e4d6823de55a4d0567

Re: Idris: Type safe printf [video]

#10

Post by wheaties » Sun, Dec 28, 2014, 3:32 PM UTC

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