# Lambda Games

Lambda Games is a generator of free theorems for Haskell that you can run straight in your browser. If you don't know what a free theorem is, read on!

Certain programming languages, most prominently purely functional
languages like Haskell^{[1]}, satisfy a powerful property called
*parametricity*. A language with this property behaves in
many ways like a typed lambda calculus, and we can use that to
derive some fairly powerful properties of polymorphic functions.

For example, consider the type signature
`∀ a. a -> a`

.
If you take this type signature and plug it into the form at the top of this page, you'll be informed that

Let's break down what this actually says. Suppose we have a function
`f : ∀ a. a -> a`

.
That is, we have a single function `f`

which
works for *every* type `a`

we
could possibly plug into it. And, crucially, if we plug in a value of type `a`

, we're guaranteed to get out another value of the *same* type `f`

. Now, consider two distinct types `a`

and `a'`

and a function `g : a -> a'`

. Then if `a0`

is value of type `a`

, we have `g (f a0) = f (g a0)`

. Put another way, the function `f`

must *commute* with every function `g : a -> a'`

, for any types `a`

and `a'`

.

This may not seem useful yet. But remember that this works for every possible `g : a -> a'`

. Let `a`

be an arbitrary type and let `x`

be some arbitrary value of type `a`

. Then define `g : a -> a`

as the constant function which maps every input to the single value `x`

. The free theorem tells us that

For every possible `a0 : a`

. We defined `g`

to be the constant function which always maps its input to `x`

, so this tells us

That is, `f`

must map every input to itself. So there is only one^{[2]} possible function of type `f : ∀ a. a -> a`

: the identity function.

Note that this *isn't* true in many OOP languages that
provide introspection of values. For instance, we can easily write
a non-identity function with this type signature in Java.

```
```public static <T> T fakeIdentity(T value) {
if (value instanceof String) {
return "some string";
} else {
return value;
}
}

Parametricity gives you powerful capabilities to reason about your
code, simply by glancing at the type signatures. This generator's
implementation is based upon Philip Wadler's excellent 1989 paper *Theorems for free!* ^{[3]},
so if you're interested in the mathematical foundations behind
this work or a formal proof of its correctness, I strongly
recommend reading that paper.

## What's Supported?

Currently, Lambda Games supports several built-in Haskell types
and will generate free theorems written in terms of certain
functions from Haskell's `Prelude`

.

Supported features:

- List types
`[a]`

. - Tuples
`(a, b, c)`

with up to five elements. - The optional type
`Maybe a`

. - The sum type
`Either a b`

. - Several "ground" types such as
`Int`

and`Boolean`

. - Typeclasses that do not take higher-kinded types, such as
`Eq`

,`Ord`

, and`Monoid`

. - Rank N types.

Currently not supported:

- Higher-kinded typeclasses such as
`Functor`

. - Tuples of more than five elements.
- Quantified higher-kinded types.
- General mu-recursive types.

The Lambda Games generator assumes the following functions are
available. All of these come from the Haskell `base`

package.

```
```-- Prelude
fmap :: Functor f => (a -> b) -> f a -> f b
Left :: a -> Either a b
Right :: b -> Either a b
($) :: (a -> b) -> a -> b
mempty :: Monoid m => m
(<>) :: Semigroup m => m -> m -> m
(==) :: Eq a => a -> a -> Boolean
(<=) :: Ord a => a -> a -> Boolean
infixr 0 $
infixr 6 <>
infix 4 ==
infix 4 <=
-- Control.Arrow (specialized to tuples and Either)
(***) :: (a -> a') -> (b -> b') -> (a, b) -> (a', b')
first :: (a -> a') -> (a, b) -> (a', b)
second :: (b -> b') -> (a, b) -> (a, b')
(+++) :: (a -> a') -> (b -> b') -> Either a b -> Either a' b'
left :: (a -> a') -> Either a b -> Either a' b
right :: (b -> b') -> Either a b -> Either a b'
infixr 3 ***
infixr 2 +++

Additionally, Lambda Games assumes all typeclass instances are lawful. That is, an `Ord`

instances actually *does* define a total ordering, `(<>)`

is actually associative, etc. A sufficiently contrived unlawful typeclass instance will break the theorems listed here.

Lambda Games is free and open source under the GNU General Public
License. You can run the tool yourself from the command line as
well. If you have suggestions or would like to add functionality,
check out the project's GitHub page^{[4]}.

^{[1]} Assuming we don't abuse the strict evaluation function
`seq :: a -> b -> b`

,
which breaks a lot of nice properties in Haskell, including
parametricity.

^{[2]} Technically, free theorems only hold quantified
over *strict* functions,
which means I'm ignoring `⊥`

values.
If you don't know what that is (or that character doesn't even
render in your font), then you probably don't have to worry about
it.

^{[3]}https://www2.cs.sfu.ca/CourseCentral/831/burton/Notes/July14/free.pdf