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.

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.

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`

.

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.

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]
```

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?

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, - the Haskell implementation,
- higher-kinded type equalities and their
`Leibniz`

es, - why
the
`=:=`

singleton trick is unsafe, - simulating GADTs with
`Leibniz`

members of data constructors.

*This article was tested with Scala 2.11.1, Scalaz 7.0.6, and Kind
Projector 0.5.2.*

Unless otherwise noted, all content is licensed under a Creative Commons Attribution 3.0 Unported License.

Back to blog