Extra attributes on post: XmlAttr(name=original_url, value=String(value=https://gitter.im/typelevel/cats?at=592401562b926f8a67834090))

**K**: Hi all. Could someone explain to me theorems for free? I read paper but could not follow it. The author mentions relation parametricity. What does it mean? Thanks.

**F**: A detailed understanding of parametricity is an intermediate topic. Are you studying out of interest or because you think it is necessary to continue your FP learning?

**A**:

```
def foo[A](a: A): A
```

How many possible functions `foo`

is there assuming that `foo`

must be total, not throw exceptions, and not do I/O (including reflection + methods like getClass)?

**K**: **F**, Do I have to understand in detail for FP?

**F**: The approach **A** is taking is what we primarily use it for in everyday programs. Go with his explanation, and you will know what you need to know for everyday use — no need to go to the paper at this point.

**K**: `foo`

is the identity function.

**A**: Right.

```
def bar[A, B](a: A, b: B): A
```

Same question.

**K**: What do you mean by possible functions?

**A**: How many different functions can you implement with such a signature?

**K**: Just two because it has to return one of the inputs.

**A**: Yes.

```
def baz[A](a: List[A]): List[A]
```

Suppose I run `baz(List(1, 2, 3))`

. Can I get a list with a 4 back?

**K**: No.

**R**: Sure thing you can.

**A**: No, you can not.

**R**: Sorry, you are right. I cannot get `List(4)`

back. However, you can still have something like:

```
def baz[A](a: List[A]): List[A] = Nil
```

I.e., it is not identity only. It can do anything specific to the list but not to its elements.

**A**: Right. You cannot sort or find the least element, but you can, for instance, do the following:

```
def baz[A](a: List[A]): List[A] = a ++ a
def baz[A](a: List[A]): List[A] = a.reverse
def baz[A](a: List[A]): List[A] = a match {
case Nil => Nil
case x :: xs => List(x)
}
```

You cannot even `map`

in a meaningful way because the only function you have is `id: A => A`

.

**K**: What does `A => A`

mean? A function?

**A**: It is the function's type.

**A**:

```
def baz[A](a: List[A]): List[A] = a.map(f)
```

`f`

can only be an identity function here because it has a signature `A => A`

(for any `A`

).

**K**: Ah... So what is the conclusion about Theorems For Free?

**A**: Theorems For Free paper shows a way to derive all such "laws" for polymorphic functions. There are more advanced things you can say, for instance:

```
// For any a: List[A],
// f: A => B, and
// baz: [A] List[A] => List[A]
baz(a).map(f) == baz(a.map(f))
```

Since FP languages (or FP discipline) constrain possible programs you can write, reasoning about them becomes straightforward. Polymorphic functions are easier to reason about because there is not much they can do. The freedom to do reflection or I/O in every function takes that reasoning away.

**K**: What do you mean by "For any `a: List[A]`

, `f: A => B`

, and `baz: [A] List[A] => List[A]`

?

**A**: It is straightforward to prove (using that paper) that whatever types `A`

and `B`

you choose, whatever `a`

, `f`

of types `List[A]`

, `A => B`

you come up with, `baz(a).map(f) == baz(a.map(f))`

will be true. `baz`

can not observe any properties of the elements of `a`

, so it can't modify them, only reorder / trim / reverse.

**K**: So if I would like the reorder the list in `baz`

, how would the signature look like?

**R**: I guess

```
def baz[A: Ord](a: List[A]): List[A]
```

**A**: If you want to be able to compare elements, that is correct.

```
def baz[A](l: List[A]): List[A]
```

already allows you to reorder them, but not based on the elements themselves.

**R**: Well, I meant some meaningful reordering besides reversing the list smile.

**A**: Is `List(1, 2, 3, 4) => List(2, 1, 4, 3)`

, swapping adjacent pairs of elements meaningful?

**R**: Well, meaningfullness is a fuzzy concept.

**M**: You can also write a `def reorder[A](a: List[A]): List[A]`

, but the way you reorder them will be fixed, that is to say, if you pass a `List[Int]`

, it will be reordered in the same way as if you pass a `List[String]`

, because you cannot get to the `Int`

or the `String`

.

**A**: Here is another interesting example of the free theorems in action:

```
trait Eq[A, B] {
def subst[F[_]](fa: F[A]): F[B]
}
```

How many possible `Eq[A, B]`

are there (assuming you cannot add extra `def`

s, `val`

s, `var`

s, pattern match on an open trait, etc)? It is a trick question.

**R**: Zero?

**A**: It depends on whether `A`

is the same as `B`

. There is exactly one `Eq[A, A]`

for any `A`

, and exactly zero `Eq[A, B]`

for different `A`

and `B`

. So `Eq`

represents type equality.

**R**: But the signature is silent about whether `A = B`

, So the only safe assumption is that they are different.

**M**: That's the only safe false assumption wink.

**A**:

```
def refl[A]: Eq[A, A] = new Eq[A, A] {
def subst[F[_]](fa: F[A]): F[A]
}
```

**M**: If you have an instance of `Eq[A, B]`

, you know that `A = B`

, because otherwise, you could not have one, right?

**A**: Yes. This amazing data-type is so powerful, that in Idris you can use it to prove theorems, same way you can with built-in `=`

. And you can use `Eq`

to implement dynamic typing in functional languages.

**R**: But what is the point in defining it with two different type parameters if you know for sure you can only have it with one? Sorry for the stupid question.

**M**: There are no stupid questions.

**A**:

```
def foo[A, B](eq: Eq[A, B], a: A): b: B
```

Because you can have two different types in one context that are equal in another. The caller of `foo`

knows that `A = B`

, but inside `foo`

, they look like different types. Here is another more realistic example:

```
sealed abstract class F[A, B] {
def isFoo: Option[Eq[A, B]]
}
final case class Foo[A]() extends F[A, A] {
def isFoo: Option[Eq[A, A]] = Some(refl[A])
}
```

**A**:
You can usually just pattern match `case Foo() =>`

to recover `A = B`

, and it will just work. However, GADTs in Scala are utterly broken, so it is sometimes not the case.

```
sealed abstract class F[A, B]
final case class Foo[A]() extends F[A, A]
def f[A, B](fab: F[A, B], a: A): B = fab match {
case Foo() => a
}
```

doesn't work in ScalaFiddle (2.11?).

**Y**: I was eavesdropping and the concept of free theorems sounds fascinating. Thanks!

**A**: There is an automated version of the paper. When I enter `[a] -> [a]`

(Haskell's syntax for `[A] List[A] => List[A]`

), I get

```
map g (f x) = f (map g x)
```

Or in Scala:

```
f(x).map(g) == f(x.map(g))
```

**A**: For `f: [A] A -> A`

it produces `forall g: A => A . g(f(x)) = f(g(x))`

, which means that `f`

is an identity. Notice that `g`

above is not necessarily polymorphic in `A`

, which is precisely why the law implies that `f`

is an identity.

Now let's look at:

```
def f[A]: A = ???
```

`f`

must return a value of type `A`

for any type `A`

, is it possible to fill in the `???`

to make that work? What if I run `f[MySecretType]`

:

```
final class MySecretType private ()
val x: MySecretType = f[MySecretType]
```

Clearly, unless we go outside Scalazzi language subset, there are no possible implementations of `f`

.

Let's look at `a -> b -> c`

, or in Scala's notation `[A, B, C](a: A, b: B): C`

. How many functions of this type are there? Consider partially applying it to it's arguments `a`

and `b`

and only then specifying `C`

:

```
val f : [A, B](a, b)[C]: C
```

This function returns `[C] C`

, which as we already know, has no possible instances.

**Y**: Could you help me out with the analysis of `(a -> b -> c) -> [a] -> [b] -> [c]`

?

**A**: Let's first rewrite it in Scala.

```
def f[A, B, C](f: (A, B) => C, la: List[A], lb: List[B]): List[C]
```

The caller knows `A`

, `B`

, `C`

, so they can supply an `f`

. compare it to the above discussion: There is no polymorphic `[A, B, C] (A, B) => C`

, but for concrete `A`

, `B`

, and `C`

there could be tons of `(A, B) => C`

. An important distinction.

**Y**: Right.

**A**: Here is the free theorem for `f :: (a -> b -> c) -> [a] -> [b] -> [c]`

, `def f[A, B, C](p: (A, B) => C, la: List[A], lb: List[B]): List[C]`

according to the generator:

```
forall t1,t2 in TYPES, g :: t1 -> t2.
forall t3,t4 in TYPES, h :: t3 -> t4.
forall t5,t6 in TYPES, f1 :: t5 -> t6.
forall p :: t1 -> t3 -> t5.
forall q :: t2 -> t4 -> t6.
(forall x :: t1. forall y :: t3. f1 (p x y) = q (g x) (h y))
==> (forall z :: [t1].
forall v :: [t3]. map f1 (f p z v) = f q (map g z) (map h v))
```

**Y**: Yeah kind of blown away.

**A**: Well, first we can intuit that `f`

can't look inside `A`

, `B`

, and `C`

, and can't produce `C`

out of thin air, so to return `List[C]`

, it must call `p`

.

**Y**: Yes.

**A**: It can't produce `A`

or `B`

out of thin air either, so it must use elements of `la`

and `lb`

to call p.

**Y**: Sure.

**A**: `f`

can be `zipWith`

, or it can apply any sort of `[A] List[A] => List[A]`

on `la`

and `lb`

and then `zipWith`

, intuitively that it is all it can do.

**Y**: `zipWith`

is definitely what I intended. But I am curious how `zipWith`

relates to the theorem.

**A**: The theorem says that if `gh (p x y) = q (g x) (h y))`

, then `map gh (f p la lb) = f q (map g la) (map h lb))`

So it basically says that if you first map two lists, it's the same as mapping the result.

**K**: What does forall stands for?

**A**: When it says `forall t :: TYPES`

it means roughly the same as `[T]`

in Scala, if it is `forall a :: t`

where `t`

is a type, then it means "whatever the value of `a`

".

**A**: I'll rewrite everything in Scala in a sec, that will make it much clearer I think.

```
if gh(p(x, y)) = q(g(x), h(y)) then
f(p, la, lb).map(gh) = f(q, la.map(g), lb.map(h))
```

Now, we know from our discussion before that to produce elements of `List[C]`

, `f`

must use `p`

, so every element of `List[C]`

was obtained by calling p
So we can move ff inside:

```
if (gh compose p)(x, y) = q(g(x), h(y)) then
f(gh compose p, la, lb) = f(q, la.map(g), lb.map(h))
```

I think this is pretty clear.

**Y**: I think I'm not fully there yet... What is the literary meaning you want to pull out?

**A**: Let's simplify a bit further, define `p'`

to be `gh compose p`

:

```
if p'(x, y) = q(g(x), h(y)) then
f(p', la, lb) = f(q, la.map(g), lb.map(h))
```

See how it makes sense?

**Y**: Ahah. Yes, this is amazing.

**Y**: Haven't read through the paper yet, so I'm only giving wild guesses. My guess is that a theorem derived from the type of a function is a key indicator of the properties of the function? So it would seem natural to think that a function's type already speaks much about the semantics of a function!

**A**: If you are disciplined with your code, then yes. On JVM you can break all sorts of rules.

**Y**: Right... I've always had an intuition that a function's type already speaks much about what it does, and that's why I've been looking into languages like Scala in the first place. I guess Free Theorems is a solid foundation for my religious beliefs.

**A**: One of the reasons FP people advocate so strongly for:

- no
`null`

- real parametricity
- tail-call elimination
- no I/O unless in a monad
- no exceptions
- no partial functions

is because all of these (or lack thereof) break this reasoning in one way or another.

**P**: +1 The idea is just to build a bubble of determinism in a world of randomness and unpredictability, in which you can reason sanely... It doesn't prevent IO or mutations but it does it at the boundaries of the bubble, not inside.

**Y**: Definitely. **A**, thanks for the info. Really helped broaden my insights.

**R**: Thanks **A**.

**A**: Paul Philips has rightly noticed that the three principles of INGSOC apply nicely to FP. The last two for sure:

- War Is Peace
- Freedom Is Slavery - side-effects (freedom) enslave.
- Ignorance Is Strength - ignorance (parametricity) gives you strength (free theorems).