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

𝚏 : ∀ 𝚊. 𝚊 -> 𝚊 ⟹ \forall 𝚊, 𝚊’ : 𝚃𝚢𝚙𝚎 . \forall 𝚐 : 𝚊 -> 𝚊’ . \forall 𝚊𝟶 : 𝚊 . 𝚐 (𝚏 𝚊𝟶) = 𝚏 (𝚐 𝚊𝟶)

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

^[4]https://github.com/Mercerenies/lambda-games