The verbosity is not in the function definition, its in the match expression needed at _every single call site_. In Idris, the definition would be similar length or longer, but call sites would not need a match expression.