parametricity's profile picture. Theorems for Free!

Parametricity

@parametricity

Theorems for Free!

I wonder what this function does. flip :: Functor f => f (a -> b) -> a -> f b Wait, no I don't.


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.


length :: Foldable f => f a -> Int ∴ length (1, '2', "3") must return 1.


Parametricity reposted

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.


@catnaroek Fast & Loose Reasoning is Morally Correct.


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 reposted

Proof `fmap f.fmap g=fmap(f.g)` follows from `fmap id=id` and the free theorem: fpcomplete.com/user/edwardk/s… /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.


Reminder. Fast & Loose Reasoning is Morally Correct.


A csharp<A>(A a) This function returns its argument.


(~.~<.~>\\+.) :: (Profunctor p, Functor f) => (a -> f b) -> p b r -> f (p a r) This operator clearly specifies what it does in the type.


Monad f => f a -> f b -> f b Any (a) values from the effect (f a) are not used.


Correction. Applicative f => f a -> f a This function is implemented with only id, (<*) or (*>). Thanks @dino_joel


Applicative => f a -> f a This function is implemented with only id, (<*) or (*>).


IO Int -> a -> Int This function ignores both arguments.


String -> a -> a This function returns the second argument, ignoring the first.


This account does not follow anyone
Loading...

Something went wrong.


Something went wrong.