Theorems for Free!
Parametrikistan
Joined January 2015
- Tweets57
- Following0
- Followers1.1K
- Likes0
f :: Lens a b -> a -> b -> a
This does one of two things.
∀ l x y. x /= y => f l x y x /= x
Now I know which.
@rightfold is thinking of a function with the type (a -> b) -> a -> b
The identity function specialized to functions.
Parametricity retweeted
Generalize an abstraction because removing nonessential information clarifies its independent meaning.
Re-use is accidental. @fronx
a -> (a, a, a, a)
I definitely know what this function does.
(a, a, a, a) -> a
I almost know what this function does.
f :: Monad f=>f T -> f T
The result might depend on previous effect values
g :: Applicative f=>f T -> f T
This definitely doesn't though
Parametricity retweeted
Proof `fmap f.fmap g=fmap(f.g)` follows from `fmap id=id` and the free theorem: fpcomplete.com/user/edwardk/… /cc @BartoszMilewski @parametricity
Using Data.Foldable and parametricity, one can be sure that:
foldMap f &&& foldMap g = foldMap (f &&& g)
f :: [a] -> [a]
This type tells us some, but not all, things.
∀ x. f [x] = [x]
∀ x y. f (x++y) = f y++f x
These tests tell us the rest.
f :: a -> a -> a
This function does one of two things.
test = f 1 2 == 1
Now it is disambiguated between those two.
(~.~<.~>\\+.) :: (Profunctor p, Functor f) => (a -> f b) -> p b r -> f (p a r)
This operator clearly specifies what it does in the type.
Correction.
Applicative f => f a -> f a
This function is implemented with only id, (<*) or (*>).
Thanks @dino_joel