I'm reading through Type-Driven Development with Idris, and I ran into some confusing formatting while experimenting with the valToString function on page 23. Specifically, I added a function hole:
valToString : (x : Bool) -> StringOrInt x -> String
valToString x val = (?f val)
When I ask the REPL about the type of this hole, this is the printed result:
*Hello> :t f
x : Bool
val : case x of
True => Int
False => String
--------------------------------------
f : case x of True => Int False => String -> String
Holes: Main.f
The type of val is readable enough here, but how should I read the type of f? The book mentions on page 19 that whitespace is significant in Idris; would this be valid syntax if I were to use it for a type in my program?
Seems like this has nothing to do with spaces. Just bad formatting.
This
f : case x of True => Int False => String -> String
can be reformatted like this:
f : (case x of {True => Int; False => String}) -> String
When I type :t f in Idris repl this shows next thing to me:
*Hello> :t f
x : Bool
val : StringOrInt x
--------------------------------------
f : StringOrInt x -> String
Holes: Main.f
This case is just inlined version of type StringOrInt x. Though poorly formatted. Maybe older version of Idris was used when this chapter was written.
UPDATE (23.07.2017)
Unfortunately, not everyone have book :( I tried to guess type of StringOrInt but I didn't guess it precisely. I used next definition in my code:
StringOrInt : Bool -> Type
StringOrInt True = Int
StringOrInt False = String
With this definition I get output from above. While in reality StringOrInt defined in the next way:
StringOrInt : Bool -> Type
StringOrInt x = case x of
True => Int
False => String
These two definitions semantically equivalent. Difference only syntactic. But apparently this leads to different compiler output for :t f command.
I've opened corresponding issue: