Parametricity

@parametricity

Theorems for Free!

Parametrikistan
homepages.inf.ed.ac.uk/wadler/topics/…
Joined January 2015
0 Photos and videos Photos and videos

Tweets

You blocked @parametricity

Are you sure you want to view these Tweets? Viewing Tweets won't unblock @parametricity

  1. 21 Apr 2017

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

    2 replies 10 retweets 28 likes
    Undo
  2. 17 Apr 2017

    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.

    1 reply 2 retweets 3 likes
    Undo
  3. 14 Oct 2015

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

    2 replies 8 retweets 13 likes
    Undo
  4. Retweeted
    10 Jul 2015
    Replying to

    a -> (a -> a) -> a I've narrowed this down to countably many possibilities.

    6 retweets 11 likes
    Undo
  5. Retweeted
    11 Jul 2015

    Generalize an abstraction because removing nonessential information clarifies its independent meaning. Re-use is accidental.

    2 replies 103 retweets 140 likes
    Undo
  6. 9 Jul 2015

    a -> (a, a, a, a) I definitely know what this function does. (a, a, a, a) -> a I almost know what this function does.

    6 replies 51 retweets 73 likes
    Undo
  7. 26 Feb 2015

    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

    3 replies 5 retweets 10 likes
    Undo
  8. Retweeted
    15 Feb 2015

    Proof `fmap f.fmap g=fmap(f.g)` follows from `fmap id=id` and the free theorem: /cc

    5 replies 18 retweets 29 likes
    Undo
  9. 10 Feb 2015

    Using Data.Foldable and parametricity, one can be sure that: foldMap f &&& foldMap g = foldMap (f &&& g)

    4 retweets 3 likes
    Undo
  10. 2 Feb 2015

    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.

    4 replies 35 retweets 29 likes
    Undo
  11. 28 Jan 2015

    f :: a -> a -> a This function does one of two things. test = f 1 2 == 1 Now it is disambiguated between those two.

    1 reply 10 retweets 7 likes
    Undo
  12. 24 Jan 2015

    Reminder. Fast & Loose Reasoning is Morally Correct.

    1 reply 9 retweets 6 likes
    Undo
  13. 24 Jan 2015

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

    6 replies
    Undo
  14. 22 Jan 2015

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

    6 replies 67 retweets 74 likes
    Undo
  15. 22 Jan 2015

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

    2 likes
    Undo
  16. 22 Jan 2015
    Replying to

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

    1 retweet 2 likes
    Undo
  17. 22 Jan 2015

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

    1 reply 1 like
    Undo
  18. 21 Jan 2015

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

    1 reply 5 retweets 5 likes
    Undo
  19. 21 Jan 2015

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

    1 like
    Undo
  20. 21 Jan 2015

    const :: a -> b -> a This function returns the first argument, ignoring the second.

    3 retweets 1 like
    Undo

@parametricity hasn't Tweeted yet.

Loading seems to be taking a while.

Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.

    You may also like

    ·