Things that Idris improves things over Haskell

Re:Things that Idris improves things over Haskell by lobster_johnson on Friday June 16, 2017 @12:57PM (#14570556)

Re typesafe printf, I assume the compiler can produce efficient code, since the pattern matching occurs at compile time?

Also, if you have an arbitrary string that isn't a constant that can be analyzed statically — for example, a string read from a config file — how do you prove to the compiler that it's a valid format-code string?

[ Parent | on HN ]

Re:Things that Idris improves things over Haskell by jfoutz on Friday June 16, 2017 @01:25PM (#14570871)

the compiler knows the failure modes. if the file doesn't exist, the printf isn't reachable. if the file isn't at least X bytes long, the printf isnt' reachable if bytes 10-20 can't be parsed as a number the printf isn't reachable.

it's just showing if you get through these 50 checks, by the time you get to printf the bytes will have been converted to what you need, or the program will have already errored out.

[ Parent | on HN ]

Re:Things that Idris improves things over Haskell by eutectic on Friday June 16, 2017 @03:33PM (#14571983)

Any string is a valid format string.

[ Parent | on HN ]

Re:Things that Idris improves things over Haskell by lobster_johnson on Friday June 16, 2017 @03:48PM (#14572105)

I mean the combination of format string + values.

Anyway, is that really true? "%-1s" should probably give you an error, for example.

[ Parent | on HN ]