Theorems for Free tells you that some abstractions satisfy some mathematical properties (for free!) under some circumstances. If you write down a function with

Theorems for Free tells you that some abstractions satisfy some mathematical properties (for free!) under some circumstances. 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.