# Talk on how polymorphic types give rise to free theorems

• Jul 25, 2013 · 7:00 PM

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

• ##### 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

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

Cheers
Arvin

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

### Zürich, Switzerland

Founded Apr 20, 2011

#### People in this Meetup are also in:

• ##### Zurich Hike & Outdoor

6,817 InternationalOutdoorEnthusiasts

• ##### Pantalks - tech & non-tech talks @ Colab Zürich

1,083 Pantendees

556 Dockers

• ##### Startups Club Zurich

1,197 Join the club of Startups!

• ##### clojure.zh - Zürich Clojure User Group

200 Clojurians

• ##### Bitcoin Meetup Switzerland

1,308 Bitcoiners