[Haskell-cafe] Free theorems for dependent types?

[Ryan Ingram]

Free theorem's are theorems about functions that rely only on parametricity.

For example, consider any function f with the type
   forall a. a -> a

>From its type, I can tell you directly that this theorem holds:
  forall g :: A -> B, x :: A,
      f (g  x) = g (f x)

(Note that the f on the left is B -> B, the f on the right is A -> A).

The term was popularized by Philip Wadler, in his paper "Theorems for
Free!" [1].  He noticed that many of the properties of functions that
one likes to prove come "for free" from their parametric type.  For
example, it's useful to know that

reverse (map fromEnum xs) == map fromEnum (reverse xs)

But this theorem comes for free from the type of reverse!  Given any

- f :: forall a. [a] -> [a]
- g :: A -> B
- xs :: [A]
we have the free theorem
- f (map g xs) = map g (f xs).

What this is saying is that any function (forall a. [a] -> [a]) can't
do a whole lot; it can inspect the structure of the list it has been
given, and rearrange, duplicate, and/or remove some elements.  But the
output list can only contain elements from the input list, without
inspecting the elements themselves.

Therefore, if
    f [1,2,3] == [1,1,2]
then
    f "abc" == "aab"
and
    f [True, True, False] == [True, True, True]
and
    f [ [], [1], [1,2] ] == [ [], [], [1,2] ]
and so on.

Therefore mapping some pure function over the result can be done
before or after applying f; and we don't have to know *anything* about
f, aside from its type, to prove this.

  -- ryan

[1] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.9875

On Sun, May 17, 2009 at 7:51 PM, Joe Fredette <jfredett at gmail.com> wrote:
> This word has piqued my interest, I've hear it tossed around the community
> quite a bit, but never fully understood what it meant. What exactly is a
> 'free theorem'?
>
> Eugene Kirpichov wrote:
>>
>> Hello,
>>
>> Is there any research on applying free theorems / parametricity to
>> type systems more complex than System F; namely, Fomega, or calculus
>> of constructions and alike?
>>
>> This seems very promising to me for the following reason: Take the
>> free theorem for 'sort::(a->a->Bool)->[a]->[a]'. The theorem could
>> possibly be a lot more powerful if there were a way to encode in the
>> type of 'sort' that it accepts a reflexive transitive antisymmetric
>> predicate, but the only way to express that is with dependent types.
>>
>> Looks like the only thing one needs to add to System F is the
>> relational translation rule for a dependent product; but I haven't
>> tried doing it myself.
>>
>>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>