Binding Application in Idris
I’ve recently implemented binding application as a language feature in Idris. This feature allows writing types such as Dependent pairs in a more ergonomic way without relying on special compiler magic. Or rather, the compiler magic is made available to everyone. This post is a collection of uses for this feature. This feature is not publicly available yet, but I intend to make it available in the near future. What is it? Binding syntax and binding-application is an idea I had a couple of yea