Free theorems.

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 defs, vals, vars, 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).