← All articles

In previous posts, we have looked at the algebra of algebraic data types and most recently, we looked at reasoning about code using parametricity. Reasoning using parametricity requires a polymorphic function from which we can derive free theorems. In this post, we are going to look at the algebra of these polymorphic functions and how we can arrive at a concrete value for them.

Consider the following polymorphic function:

trait identity {
  def apply[A]: A => A
}

Earlier, we have asserted that this function is equal to 1. There is only one possible implementation of this trait. We can see this intuitively, but intuition is not always reliable. Indeed, a cynical (responsible?) programmer might become immediately suspicious of an assertion about a program that is based on intuition. How do we calculate and prove it to be 1?

Category Theory provides us with a result called the Yoneda Lemma. There are all sorts of interesting insights to the Yoneda Lemma, but we won't go into these too far. One way to look at the Yoneda Lemma is that it is the type signature for map though missing one of its arguments:

trait Yoneda[F[_], A] {
  def run[B](f: A => B): F[B]
}

One important property of the Yoneda Lemma, and one that we will be using, is that it can lower and it can lift. Specifically, we have this pair of functions:

lower: Yoneda[F, A] => F[A]
lift:  F[A] => Yoneda[F, A]

Let's implement those:

trait Yoneda[F[_], A] {
  def run[B](f: A => B): F[B]

  def lower: F[A] =
    run(identity)
}

object Yoneda {
  def lift[F[_], A](x: F[A])(implicit F: Functor[F]): Yoneda[F, A] =
    new Yoneda[F, A] {
      def run[B](f: A => B) =
        F.fmap(f)(x)
    }
}

trait Functor[F[_]] {
  def fmap[A, B](f: A => B): F[A] => F[B]
}

Using the Yoneda Lemma, we could prove some interesting results. One example of an interesting result is, given a function f[A]: List[A] => List[A], any function g and any list x, then f(x.map(g)) == f(a).map(g). This means, for example, a compiler could prove that these two expressions are equivalent and rearrange the program for optimum performance.

However, for our purposes, we want to prove: identity == 1 == Unit. We will do this by writing a pair of functions, each is a series of steps:

• identity => Unit
• Unit => identity

Before we do, let's write a lift function that is specific to the Id[A] data type. We know that the lift function works for any Functor, but we only need Id[A] for our proof. We know that Id[A] is algebraically equivalent to A:

case class Id[A](run: A) {
  def lift: Yoneda[Id, A] =
    new Yoneda[Id, A] {
      def run[B](f: A => B) =
        Id(f(Id.this.run))
    }
}

object IdentityEquals1 {
  def identity_to_1: identity => Unit = {
    sys.error("todo")
  }

  def identity_from_1: Unit => identity = {
    sys.error("todo")
  }
}

Let's get to work on the identity_to_1 function. The first step is to raise A to the power of 1 in the argument to identity:

trait identity_unit {
  def apply[A]: (Unit => A) => A
}

def identity_to_1: identity => Unit = {
  trait identity_unit {
    def apply[A]: (Unit => A) => A
  }

  val step1: identity => identity_unit =
    f =>
      new identity_unit {
        def apply[A] = g => f.apply(g(()))
      }

  sys.error("todo")
  }

Since our premise is that Unit = 1 and A1 = A, it's clear that we have not lost any information (and if we have, the reverse steps won't work!). The next step is to wrap the return value (A) in Id.

trait identity_unit_id {
  def apply[A]: (Unit => A) => Id[A]
}

def identity_to_1: identity => Unit = {
  val step1: identity => identity_unit =
    f =>
      new identity_unit {
        def apply[A] = g => f.apply(g(()))
      }

  val step2: identity_unit => identity_unit_id =
    f =>
      new identity_unit_id {
        def apply[A] = g => Id(f.apply(g))
      }

  sys.error("todo")
}

def identity_from_1: Unit => identity = {
  sys.error("todo")
}

The next step is to transform our previous step, directly to Id[Unit]. This can be done using the yoneda lemma!

def identity_to_1: identity => Unit = {
  trait identity_unit {
    def apply[A]: (Unit => A) => A
  }

  val step1: identity => identity_unit =
    f =>
      new identity_unit {
        def apply[A] = g => f.apply(g(()))
      }

  trait identity_unit_id {
    def apply[A]: (Unit => A) => Id[A]
  }

  val step2: identity_unit => identity_unit_id =
    f =>
      new identity_unit_id {
        def apply[A] = g => Id(f.apply(g))
      }

  val step3: identity_unit_id => Id[Unit] =
    f =>
      new Yoneda[Id, Unit] {
        def run[B](g: Unit => B) = f.apply(g)
      }.lower

  sys.error("todo")
}

The final step is to witness that Id[A] == A and then we can put it all together:

def identity_to_1: identity => Unit = {
  val step1: identity => identity_unit =
    f =>
      new identity_unit {
        def apply[A] = g => f.apply(g(()))
      }

  val step2: identity_unit => identity_unit_id =
    f =>
      new identity_unit_id {
        def apply[A] = g => Id(f.apply(g))
      }

  val step3: identity_unit_id => Id[Unit] =
    f =>
      new Yoneda[Id, Unit] {
        def run[B](g: Unit => B) = f.apply(g)
      }.lower

  val step4: Id[Unit] => Unit =
    _.run

  step1 andThen step2 andThen step3 andThen step4
}

OK, so we have demonstrated a function: identity => Unit. We used the yoneda lemma at step 3 by lowering to Id. We now need to produce the function in the opposite direction, and you wouldn't believe it, but it's the reverse of the four steps!

We'll start at step1:

def identity_from_1: Unit => identity = {
  val step1: Unit => Id[Unit] =
    Id(_)

  sys.error("todo")
}

Step 2 involves using the lift function that we implemented on the Id data type:

def identity_from_1: Unit => identity = {
  val step1: Unit => Id[Unit] =
    Id(_)

  val step2: Id[Unit] => identity_unit_id =
    f =>
      new identity_unit_id {
        def apply[A] = f.lift.run
      }

  sys.error("todo")
}

The next step involves the equivalence between Id[A] and A:

def identity_from_1: Unit => identity = {
  val step1: Unit => Id[Unit] =
    Id(_)

  val step2: Id[Unit] => identity_unit_id =
    f =>
      new identity_unit_id {
        def apply[A] = f.lift.run
      }

  val step3: identity_unit_id => identity_unit =
    f =>
      new identity_unit {
        def apply[A] = f.apply(_).run
      }

  sys.error("todo")
}

And the final step is simplifying the expression A1 = A, then well tie it all together:

def identity_from_1: Unit => identity = {
  val step1: Unit => Id[Unit] =
    Id(_)

  val step2: Id[Unit] => identity_unit_id =
    f =>
      new identity_unit_id {
        def apply[A] = f.lift.run
      }

  val step3: identity_unit_id => identity_unit =
    f =>
      new identity_unit {
        def apply[A] = f.apply(_).run
      }

  val step4: identity_unit => identity =
    f =>
      new identity {
        def apply[A] = a => f.apply(_ => a)
      }

  step1 andThen step2 andThen step3 andThen step4
}

We have completed a proof, using the yoneda lemma, that identity = 1. There is only one possible implementation of this trait. This is a relatively trivial result, but the goal here is to show the steps to get to the result. We might do a slightly less trivial proof:

Claim: the following trait has only 2 possible implementations.

trait bool {
  def apply[A]: A => A => A
}

We start with the premise that Boolean = 2 and we write a pair of functions, using the yoneda lemma along the way, to and from. Here is the complete proof:

object BoolEquals2 {
  val bool_to_2: bool => Boolean = {
    val step1: bool => bool_uncurry =
      b =>
        new bool_uncurry {
          def apply[A] =
            aa => b.apply(aa._1)(aa._2)
        }

    val step2: bool_uncurry => bool_cont =
      b =>
        new bool_cont {
          def apply[A] =
            g =>
              b.apply(g(true), g(false))
        }

    val step3: bool_cont => bool_cont_identity =
      f =>
        new bool_cont_identity {
          def apply[A] =
            g =>
              Id(f.apply(g.apply))
        }

    val step4: bool_cont_identity => Id[Boolean] =
      f =>
        new Yoneda[Id, Boolean] {
          def run[B](g: Boolean => B) =
            f.apply(g)
        }.lower

    val step5: Id[Boolean] => Boolean =
      _.run

    step1 andThen step2 andThen step3 andThen step4 andThen step5
  }

  val bool_from_2: Boolean => bool = {
    val step1: Boolean => Id[Boolean] =
      Id(_)

    val step2: Id[Boolean] => bool_cont_identity =
      i =>
        new bool_cont_identity {
          def apply[A] =
            i.lift.run
        }

    val step3: bool_cont_identity => bool_cont =
      b =>
        new bool_cont {
          def apply[A] =
            b.apply(_).run
        }

    val step4: bool_cont => bool_uncurry =
      b =>
        new bool_uncurry {
          def apply[A] = {
            case (a1, a2) => b.apply(x => if(x) a1 else a2)
          }
        }

    val step5: bool_uncurry => bool =
      b =>
        new bool {
          def apply[A] =
            a1 => a2 => b.apply(a1, a2)
        }

    step1 andThen step2 andThen step3 andThen step4 andThen step5
  }
}

Here are some other claims that you might consider writing the equivalence, using the yoneda lemma:

• [A, B](A, B) => A == 1
• [A, B, C](B => C) => (A => B) => A => C == 1

Hopefully this gives some insight into the yoneda lemma, though there are many other interesting and practical applications for it!