Talk on how polymorphic types give rise to free theorems

This is a past event

13 people went



"A free theorem is considered free because it can be derived solely from the type of a func- tion, with no knowledge at all of the function's actual definition. In essence, it records a constraint arising from the fact that a parametric polymorphic function must behave uniformly, i.e., must use the same algorithm to compute its result, regardless of the concrete type at which it is instantiated."

From a practical perspective, the existence of free theorems shows that polymorphic types protect us from implementation mistakes, as they force the implementation to behave uniformly over its inputs.