Andres and Wouter interview Edwin Brady, most famous for his work on the Idris programming language. We talk about how he got interested in programming with dependent types, his thoughts on dependently typed programming in Haskell, and his vision for Idris.
@jaror I never liked it; I think if you can’t be bothered to assign a name, point-free combinators are what you should be using.
I also think it gets much uglier or complicated (or both) once you have arguments (unlike getLine, but like most subroutines).
That said, I wouldn’t take it away from anyone. I think the desugaring is unsurprising and, at least in a strict language, semantics preserving.
I haven’t really spent the necessary time to think clearly through the non-strict case.