2
User
Recs.
Recs.
3
Updates
Last
Updated
Updated
Activity
9 Options
Phil Wadler introduced us to the notion of a free theorem and we've been abusing them in Haskell ever since.
These wonderful artifacts of Hindley-Milner-style type systems help out with equational reasoning by using parametricity to tell you about what a function will not do.
For instance, there are two laws that every instance of Functor should satisfy:
- 'forall f g. fmap f . fmap g = fmap (f . g)'
- 'fmap id = id'
But, the free theorem tells us we need not bother proving the first one, but given the second it comes for 'free' just from the type signature!
fmap :: Functor f => (a -> b) -> f a -> f b
You need to be a bit careful with laziness, but this is partially covered in the original paper, and in Janis Voigtlaender's more recent paper on free theorems in the presence of seq.
Specs
Pros
Know any positive aspects of this option?
Cons
Know any negative aspects of this option?
Recommendations
Free Theorems
Recommended 11 years ago
Daniel hasn’t added their experience, pros or cons to their recommendation.
Free Theorems
Recommended 11 years ago
T-R hasn’t added their experience, pros or cons to their recommendation.