I would have loved to see an example at the end where the format string comes from user input. I’ll try to find the answer myself as I’m quite baffled right now as how would Idris be able to calculate a type from a string that isn’t known at compile time…
Except for that, nice video! Thanks for creating it.
The thing I found unsatisfactory was when there were no arguments, that was not a compile error. But extremely cool.
I haven’t used Idris at all so this is just an assumption on my part. But I think the reason why it didn’t error on the case where there were no arguments is because of currying. printf "%d" by itself just returns a function that takes an Int and returns a String so you can do things like:
intPrinter :: Int -> String
intPrinter = printf "%d"
In a complete program, the compiler would complain if you tried to use the intPrinter function as a String value (thus forcing you to provide an argument). Again, this is just an assumption on my part; maybe Brian can correct me if I’m wrong.
It would be an error to do the following:
h : String
h = printf "Hello ℅s"
But the Idris REPL has no problems printing functions, unlike the Haskell REPL.
I read your question initially and thought, “Clearly that’s simple to solve, you just calculate the function on the fly as you do and then pass it the relevant arguments an–” then I realized you can’t know how many arguments to take without added work. I don’t know Idris, but I suspect the problem can be written:
main = do
formatStr <- getStr
printf formatStr "some" "args" "here" 1 2 3
The question being, ‘What happens when the format string has some number of placeholders not equal to 6’. Certainly we could count and verify the number of needed placeholders, but I suspect this code would either compile just fine and crash on bad input, or hollar that it couldn’t figure out the type of (printf formatStr) and fail to compile (hopefully the latter).
I suspect to get it to compile you would need to annotate the type as you do in haskell, and then you’d probably need to add a run-time check to make sure things failed nicely.
Idris won’t compile the above - proving that the input string has the correct interpolation holes would be pretty tricky, especially in the way this printf is formulated.
If you want the printf value to be determined at runtime, I’d probably just go the Haskell way but add a validation type. Not a lot of value in proving correct arguments to a value when you don’t know anything about the possible value (conversely, you gain value from having more constraints on the possible input value).