4 ms·
I think the comparison between printf in Idris and Zig is a little off, since the Idris version defines an intermediate datastructure, and hence requires extra
by chriswarbo 5y ago
I think the comparison between printf in Idris and Zig is a little off, since the Idris version defines an intermediate datastructure, and hence requires extra parsing and interpreting functions for it. That's a nice approach, but the Zig version is operating directly on characters, so it's a bit apples-to-oranges.
We can get a more direct Idris implementation by inlining the parser (toFmt) into the interpreter (PrintfType). That lets us throw away `Fmt`, `toFmt`, etc. to just get:
PrintfType : (fmt : List Char) -> Type
PrintfType ('*' :: xs) = ({ty : Type} -> Show ty => (obj : ty) -> PrintfType xs)
PrintfType ( x :: xs) = PrintfType xs
PrintfType [] = String
printf : (fmt : String) -> PrintfType (unpack fmt)
printf fmt = printfAux (unpack fmt) [] where
printfAux : (fmt : List Char) -> List Char -> PrintfType fmt
printfAux ('*' :: fmt) acc = \obj => printfAux fmt (acc ++ unpack (show obj))
printfAux ( c :: fmt) acc = printfAux fmt (acc ++ [c])
printfAux [] acc = pack acc
- dvh 5y agoWould printf even exist if C had sane strings?
- foxfluff 5y agoHow is formatted printing related in any way to the internal representation of strings? printf is what you call when you want to print X in hexadecimal with at least two digits, left justified on an eight-character wide field. I don't see how the sanity of whatever string representation the programming language uses is relevant here.
- msla 5y agoSome kind of formatting function would because sometimes, you really do need to print an integer with enough leading zeroes to fit in a five-digit field.
- peterashford 5y agoprintf exists in Java. Because its so bloody useful.
- goldsteinq 5y agoExcept this version doesn’t compile. I’m not sure that it’s possible to get it to compile: type-level Idris is actually a _subset_ of Idris and pattern-matching non-ADTs is half-broken on the type level. You can also observe this problem in this simplified example: f : Char -> Type f '0' = Int f _ = Char g : (c : Char) -> (f c) g '0' = 0 g c = c