align-toparrow-leftarrow-rightbackbellblockcalendarcamerachatcheckchevron-downchevron-leftchevron-rightchevron-small-downchevron-small-leftchevron-small-rightchevron-small-upchevron-upcircle-with-crosscrosseditemptyheartfacebookfullheartglobegoogleimagesinstagramlocation-pinmagnifying-glassmailmoremuplabelShape 3 + Rectangle 1outlookpersonplusImported LayersImported LayersImported Layersshieldstartwitteryahoo

Talk on how polymorphic types give rise to free theorems

From: http://www.iai.uni-bonn.de/~jv/p76-voigtlaender.pdf

"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.

Join or login to comment.

  • Arvin M.

    Here is another cool applicatoin of free theorems. Suppose you have an algebraic data type f (* -> *) permitting a map

    fmap' :: (a -> b) -> f a -> f b

    Then it follows form the free theorem of the type of fmap', that for all g :: a -> b and h :: b -> c we have

    fmap' h . fmap' g = fmap' (h . g) . fmap' id

    Hence in order to prove that f is actually an instance of the type class Functor it is enough to verify ONLY that

    fmap' id = id

    September 27, 2013

  • Arvin M.

    Hi guys, I just figured out that it is actually true that the types List T and forall X. (T -> X -> X) -> X -> X are "isomorphic". You can prove this using a free theorem of the type on the right (see [1], 3.6)
    where you actually show that any polymorphic term

    r :: (forall X. (T -> X -> X) -> X -> X)

    must be actually of the form r_B c n = fold_T,B c n (r_(List T) cons_T nil_T)

    In other words you can think of r_B to correspond to the "List" r_(List T) cons_T nil_T

    Just wanted to share this little insight with you. :)

    Btw. there is an online "Free Theorem" generator [2] you can play with.

    Cheers
    Arvin

    [1] http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf
    [2] http://www-ps.iai.uni-bonn.de/cgi-bin/free-theorems-webui.cgi

    1 · July 26, 2013

    • Arvin M.

      I just got another small insight :) Remember I showed that the type (forall X. (X -> X) -> X -> X) is "isomorphic" to the natural numbers \N ? Well we can see this as well using the isomorphism of Lists from above: \N ~ List () ~ (forall X. ( () -> X -> X) -> X -> X) ~ (forall X. (X -> X) -> X -> X).

      July 26, 2013

  • Simon M.

    Hi guys, I'm sorry, but I cannot make it this time. Ralf Sasse will take over my role as a host. Have fun and cu next time :)

    July 25, 2013

  • Bas van D.

    Unfortunately I can't make it to this one. See you next time at ZuriHac 2013!!!

    July 22, 2013

  • Arvin M.

    Hi guys, I am really really sorry for the convenience! And Simon, Bas and Thomas thanks a lot for helping me out at short notice!
    Arvin

    June 26, 2013

    • Arvin M.

      I meant of course INconvenience :)

      June 26, 2013

  • Simon M.

    Hey guys, Arvin can unfortunately not make it. Therefore, I moved this meetup to one month later. We'll nevertheless have a meetup: Thomas Schilling, Bas van Dijk, and myself will give a hands-on introduction to stream fusion :-)

    June 26, 2013

People in this
Meetup are also in:

Sign up

Meetup members, Log in

By clicking "Sign up" or "Sign up using Facebook", you confirm that you accept our Terms of Service & Privacy Policy