Triplequote are sponsoring Typelevel, click here to learn how you can help them help us (and speed up your builds into the bargain)

## A function from type equality to Leibniz

The Scala standard library provides evidence of two types being equal at the data level: a value of type `(A =:= B)` witnesses that `A` and `B` are the same type. Accordingly, it provides an implicit conversion from `A` to `B`. So you can write `Int`-summing functions on your generic foldable types.

``````final case class XList[A](xs: List[A]) {
def sum(implicit ev: A =:= Int): Int =
xs.foldLeft(0)(_ + _)
}
``````

That works because `ev` is inserted as an implicit conversion over that lambda’s second parameter.

## Fragility

That’s not really what we want, though. In particular, flipping `A` and `Int` in the `ev` type declaration will break it:

``````….scala:5: overloaded method value + with alternatives:
(x: Int)Int <and>
(x: Char)Int <and>
(x: Short)Int <and>
(x: Byte)Int
cannot be applied to (A)
xs.foldLeft(0)(_ + _)
^
``````

That doesn’t make sense, though. Type equality is symmetric: Scala knows it goes both ways, so why is this finicky?

Additionally, we apply the conversion for each `Int`. It is a logical implication that, if `A` is `B`, then `List[A]` must be `List[B]` as well. But we can’t get that cheap, single conversion without a cast.

## Substitution

Scalaz instead provides `Leibniz`, a more perfect type equality. A simplified version follows, which we will use for the remainder.

``````sealed abstract class Leib[A, B] {
def subst[F[_]](fa: F[A]): F[B]
}
``````

This reads “`Leib[A, B]` can replace `A` with `B` in any type function”. That “any” is pretty important: it gives us both the theorem that we want, and a tremendous consequent power that gives us most of what we can get in Scala from value-level type equality, by choosing the right `F` type parameter to `subst`.

## What could it be?

Following the Scalazzi rules, where no `null`, type testing or casting, or `AnyRef`-defined functions are permitted, what might go in the body of that function? Even if you know what `A` is, as a `Leib` implementer, it’s hidden behind the unknown `F`. Even if you know that `B` is a supertype of `A`, you don’t know that `F` is covariant, by scalac or otherwise. Even if you know that `A` is `Int` and `B` is `Double`, what are you going to do with that information?

So there’s only one thing this `Leib` could be, because you do have an `F` of something.

``````implicit def refl[A]: Leib[A, A] = new Leib[A, A] {
override def subst[F[_]](fa: F[A]): F[A] = fa
}
``````

Every type is equal to itself. Every well-formed `Leib` instance starts out this way, in this function.

## Recovery

So, it’s great that we know the implication of the `subst` method’s generality. But that’s not good enough; we had that with `=:=` already. We want to write well-typed operations that represent all the implications of the `Leib` type equality as new `Leib`s representing those type equalities.

First, let’s solve the original problem, using infix type application to show the similarity to `=:=`:

``````def sum2(implicit ev: A Leib Int): Int =
ev.subst[List](xs).foldLeft(0)(_ + _)
``````

There is no more implicit conversion, the result of `subst` is the same object as the argument, and `[List]` would be inferred, but I have merely specified it for clarity in this example.

This doesn’t compose, though. What if, having `subst`ed `Int` into that `List` type, I now want to `subst` `List[A]` for `List[Int]` in some type function? Specifically, what about a `Leib` that represents that type equality? To handle that, we can `subst` into `Leib` itself!

``````def lift[F[_], A, B](ab: Leib[A, B]): Leib[F[A], F[B]] =
ab.subst[Lambda[X => Leib[F[A], F[X]]]](Leib.refl[F[A]])
``````

Again, the final `[F[A]]` could be inferred.

As an exercise, define the `symm` and `compose` operations, which represent that `Leib` is symmetric and transitive as well. Hints: the `symm` body is the same except for the type parameters given, and `compose` doesn’t use `refl`.

``````def symm[A, B](ab: Leib[A, B]): Leib[B, A]
def compose[A, B, C](ab: Leib[A, B], bc: Leib[B, C]): Leib[A, C]
``````

## Leib power

In Scalaz, `Leibniz` is already defined, and used in a few places. Though their `subst` definitions are completely incompatible at the scalac level, they have a weird equivalence due to the awesome power of `subst`.

``````import scalaz.Leibniz, Leibniz.===

def toScalaz[A, B](ab: A Leib B): A === B =
ab.subst[A === ?](Leibniz.refl)

def toLeib[A, B](ab: A === B): A Leib B =
ab.subst[A Leib ?](Leib.refl)
``````

…where `?` is to type-lambdas as `_` is to Scala lambdas, thanks to the Kind Projector plugin.

And so it would be with any pair of `Leibniz` representations with such `subst` methods that you might define. Unfortunately, `=:=` cannot participate in this universe of isomorphisms; it lacks the `subst` method that serves as the `Leibniz` certificate of authenticity. You can get a `=:=` from a `Leibniz`, but not vice versa.

Why would you want that weak sauce anyway?

## Looking up

These are just the basics. Above:

• The weakness of Scala’s own `=:=`,
• the sole primitive `Leibniz` operator `subst`,
• how to logically derive other type equalities,
• the isomorphism between each `Leibniz` representation and all others.

In the next part, we’ll look at:

• Why it matters that `subst` always executes to use a type equality,
• higher-kinded type equalities and their `Leibniz`es,
• why the `=:=` singleton trick is unsafe,
• simulating GADTs with `Leibniz` members of data constructors.