>There’s a well-known saying: "All abstractions leak." It’s true. No matter how good the abstraction, eventually, you’ll run into situations where you need to understand the underlying implementation details This is false. One can read up on Theorem's for Free by Wadler to see that not all abstractions are leaky.
If you write down a function with signature
{T : Type} -> T -> T
then it must be the identity function, if you do not use "malicious" extensions of the type system.But what is the performance of the identity function?
Here is an identity function:
lambda T, lambda t, if (2 + 2 = 4) then t else t
In other words: I can hide pretty much arbitrary computation in my identity function.Users of my identity functuon will notice that it is wicked slow (in reality, I let my identity function compute Busy Beaver 5, before doing nothing). Their complaints are evidence of leaky abstraction.
Now you might have a smart optimizing compiler that knows about Thm4Free... But that's another story.