K: Hi all. Could someone explain me about theorems for free, I read https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf but could not follow it. The author metions about relation parametricity, what does it mean? Thanks
F: I would say that a detailed understanding of parametricity is an intermediate topic, are you studying out of interest or because you think is necessary to continue with your FP learning?
How many possible functions
foo are 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’ll know what you need to know for everyday use I would say, no need to go to the paper at this point.
foo is the identity function.
K: What do you mean possible functions?
A: How many different functions can you implement with such signature?
K: Just two because it has to return one of the inputs.
Suppose I run
baz(List(1, 2, 3)). Can I get a list with a 4 back?
A: What kind of things can
baz do to my list? Can it, for instance, sort the list? Reverse it? Concatenate two copies? Return the first element if any or Nil?
R: Sure thing you can
A: No you can not. We are still assuming that functions must be total, not throw exceptions, and not do I/O (including reflection + methods like getClass)?
R: Sorry, you’re right, can’t get
List(4) back. But you can still have something like:
I.e. it’s not identity only. Can do anything specific to list, but not to its elements.
A: Right. You can’t sort or find the least element, but you can for instance do:
You can’t 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: A type of function.
f can only be an identity function here, because it has a signature
A => A (for any
K: Ah… So what is the conclusion about theorem 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:
Since FP languages (or FP discipline) constrains possible programs you can write, reasoning about them becomes easier. Polymorphic functions are easier to reason about because there is not much they can possibly do. Freedom to do reflection or I/O in every single function takes that reasoning away.
K: What do you mean by "For any
f: A => B, and
baz: [A] List[A] => List[A]?
A: It is straightforward to prove (using that paper) that whatever types
B you choose, whatever
f of types
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
A: If you want to be able to compare elements, that is correct.
already allows you to reorder them, but not based on the elements themselves.
R: Well, I meant some meaningful reorderin, besides reverse :smile:.
List(1, 2, 3, 4) => List(2, 1, 4, 3), swapping adjacent pairs of elements meaningful?
R: Well, meaning 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 re-ordered in the exact same way as if you pass a
List[String], because you can’t get to the
Int or the
A: Here is another interesting example of the free theorems in action:
How many possible
Eq[A, B] are there (assuming you can’t add extra
vars, pattern match on an open trait, etc)? It’s a trick question.
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
Eq represents type equality.
R: But the signature is silent about whether
A = B, So the only safe assumption is that they’re different.
M: That’s the only safe false assumption :wink:.
M: If you have an instance of
Eq[A, B], you know for sure that
A = B, because otherwise you couldn’t 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’s the point in defining it with two different type parameters, if you know for sure you can only have it with one? Sorry for stupid question.
M: There are no stupid questions.
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:
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’s sometimes not the case.
doesn’t work in ScalaFiddle (2.11?).
Y: I was eavesdropping and the concept of free theorems sounds fascinating. Thanks!
A: https://alexknvl.com/cgi-bin/free-theorems-webui.cgi - there is an automated version of the paper. When I enter
[a] -> [a] (Haskell’s syntax for
[A] List[A] => List[A]), I get
Or in Scala:
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:
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
Clearly, unless we go outside Scalazzi language subset, there are no possible implementations of
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
b and only then specifying
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.
The caller knows
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
C there could be tons of
(A, B) => C. An important distinction.
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
C, and can’t produce
C out of thin air, so to return
List[C], it must call
A: It can’t produce
B out of thin air either, so it must use elements of
lb to call p.
f can be
zipWith, or it can apply any sort of
[A] List[A] => List[A] on
lb and then
zipWith, intuitively that it is all it can do.
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: I’ll rewrite everything in Scala in a sec, that will make it much clearer I think.
Now, we know from our discussion before that to produce elements of
f must use
p, so every element of
List[C] was obtained by calling p So we can move ff inside:
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:
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:
- 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).