Sometimes you’ll hear someone describe two things as being “isomorphic” to one another and I wanted to explain what that means.

You might have already guessed that “isomorphic” is a synonym for “equivalent”, and that would have been a pretty good guess. Really, the main difference between the two words is that “isomorphic” has a more precise and more general definition than “equivalent”.

In this post I will introduce a more precise definition of “isomorphic”, using Haskell code. This definition won’t be the fully general definition, but I still hope to give you some taste of how “isomorphic” can denote something more than just “equivalent”.

#### The simple version

The simplest and least general definition of “isomorphic” (in Haskell) is:

Two types,

`A`

, and`B`

, are isomorphic if there exist two functions,`forward`

and`backward`

of the following types:`forward :: A -> B backward :: B -> A`

… such that the following two equations (which I will refer to as the “isomorphism laws”) are true:

`. backward = id forward . forward = id backward`

`id`

here is the identity function from Haskell’s Prelude,
defined like this:

```
id :: a -> a
id x = x
```

… and `(.)`

is the function composition operator (also
from Haskell’s Prelude), defined like this:

```
(.) :: (b -> c) -> (a -> b) -> (a -> c)
. g) x = f (g x) (f
```

According to the above definition, the types
`Bool -> a`

and `(a, a)`

are isomorphic,
because we can define two functions:

```
forward :: (Bool -> a) -> (a, a)
= (function False, function True)
forward function
backward :: (a, a) -> (Bool -> a)
False = first
backward (first, second) True = second backward (first, second)
```

… and we can prove that those two functions satisfy the isomorphism laws using equational reasoning.

## Proof of the isomorphism laws (click to expand)

Here’s the proof of the first isomorphism law:

```
. backward
forward
-- (f . g) = \x -> f (g x)
--
-- … where:
--
-- f = forward
-- g = backward
= \x -> forward (backward x)
-- x = (first, second)
= \(first, second) -> forward (backward (first, second))
-- forward function = (function False, function True)
= \(first, second) ->
False, backward (first, second) True)
(backward (first, second)
-- backward (first, second) False = first
-- backward (first, second) True = second
= \(first, second) -> (first, second)
-- x = (first, second)
--
-- … in reverse
= \x -> x
-- id x = x
--
-- … in reverse
= \x -> id x
-- η-reduction
= id
```

… and here is the proof of the second isomorphism law:

```
. forward
backward
-- (f . g) = \x -> f (g x)
--
-- … where:
--
-- f = backward
-- g = forward
-- x = function
= \function -> backward (forward function)
-- forward function = (function False, function True)
= \function -> backward (function False, function True)
-- η-expand
= \function bool -> backward (function False, function True) bool
-- There are two possible cases:
--
-- Case #0: bool = False
-- Case #1: bool = True
-- Proof for case #0: bool = False
= \function bool -> backward (function False, function True) False
-- backward (first, second) False = first
--
-- … where:
--
-- first = function False
-- second = function True
= \function bool -> function False
-- bool = False
--
-- … in reverse
= \function bool -> function bool
-- η-reduction
= \function -> function
-- id x = x
--
-- … in reverse
= \function -> id function
-- η-reduction
= id
-- Proof for case #1: bool = True
= \function bool -> backward (function False, function True) True
-- backward (first, second) True = second
--
-- … where:
--
-- first = function False
-- second = function True
= \function bool -> function True
-- b = True
--
-- … in reverse
= \function bool -> function bool
-- η-reduction
= \function -> function
-- id x = x
--
-- … in reverse
= \function -> id function
-- η-reduction
= id
```

We’ll use the notation `A ≅ B`

as a short-hand for
“`A`

is isomorphic to `B`

”, so we can also
write:

`Bool -> a ≅ (a, a)`

Whenever we declare that two types are isomorphic we need to actually
specify what the `forward`

and `backward`

conversion functions are and prove that they satisfy isomorphism laws.
The existence of `forward`

and `backward`

functions of the correct input and output types is not enough to
establish that the two types are isomorphic.

For example, suppose we changed the definition of
`forward`

to:

```
forward :: (Bool -> a) -> (a, a)
= (function True, function False) forward function
```

Then `forward . backward`

and
`backward . forward`

would still type-check and have the
right type, but they would no longer be equal to `id`

.

In other words, when discussing isomorphic types, it’s technically
not enough that the two types are equivalent. The *way* in which
they are equivalent matters, too, if we want to be pedantic. In
practice, though, if there’s only one way to implement the two
conversion functions then people won’t bother to explicitly specify
them.

The reason why this is important is because an isomorphism also gives us an explicit way to convert between the two types. We're not just declaring that they're equivalent, but we're spelling out exactly how to transform each type into the other type, which is very useful!

#### More examples

Let’s speedrun through a few more examples of isomorphic types, which all parallel the rules of arithmetic:

```
-- 0 + a = a
Either Void a ≅ a
-- a + (b + c) = (a + b) + c
Either a (Either b c) = Either (Either a b) c
-- 1 × a = a
((), a) ≅ a
-- a × (b × c) = (a × b) × c
(a, (b, c)) ≅ ((a, b), c)
-- 0 × a = 0
Void, a) ≅ Void
(
-- a × (b + c) = (a × b) + (a × c)
Either b c) ≅ Either (a, b) (a, c)
(a,
-- a ^ 1 = a
-> a ≅ a
()
-- a ^ 0 = 1
Void -> a ≅ ()
-- (c ^ b) ^ a = (c ^ a) ^ b
-> b -> c ≅ b -> a -> c
a
-- (c ^ b) ^ a = c ^ (a × b)
-> b -> c ≅ (a, b) -> c a
```

**Exercise:** implement the `forward`

and
`backward`

functions for some of the above types and prove
the isomorphism laws for each pair of functions. It will probably be
very tedious to prove all of the above examples, so pick the ones that
interest you the most.

#### Intermediate tricks

This section will introduce some more advanced tricks for proving that two types are isomorphic.

First, let’s start with a few ground rules for working with all isomorphisms:

Reflexivity:

`a ≅ a`

Symmetry: If

`a ≅ b`

then`b ≅ a`

Transitivity: If

`a ≅ b`

and`b ≅ c`

then`a ≅ c`

Now let’s get into some Haskell-specific rules:

a

`newtype`

in Haskell is isomorphic to the underlying type if the`newtype`

constructor is public.

For example, if we were to define:

`newtype Name = Name { getName :: String }`

… then `Name`

and `String`

would be isomorphic
(`Name ≅ String`

), where:

```
forward :: Name -> String
= getName
forward
backward :: String -> Name
= Name backward
```

One such `newtype`

that shows up pretty often when
reasoning about isomorphic types is the `Identity`

type constructor from `Data.Functor.Identity`

:

`newtype Identity a = Identity { runIdentity :: a }`

… where `Identity a ≅ a`

.

To see why `Identity`

is useful, consider the following
two types:

```
newtype State s a = State { runState :: s -> (a, s) }
newtype StateT s m a = StateT { runStateT :: s -> m (a, s) }
```

The latter `newtype`

is from the `transformers`

package, which is how we layer on the “state” effect within a monad
transformer stack. If you don’t understand what that means, that’s okay;
it’s not that relevant to the point.

However, the `transformers`

package doesn’t define
`State`

as above. Instead, the `transformers`

package defines `State`

like this:

`type State s = StateT s Identity`

The latter `type`

synonym definition for
`State`

is equivalent (“isomorphic”) to the
`newtype`

definition for `State`

I provided above.
In order to prove that though I’ll need to distinguish between the two
`State`

type constructors, so I’ll use a numeric subscript to
distinguish them:

```
import Data.Functor.Identity (Identity)
newtype State₀ s a = State₀ { runState :: s -> (a, s) }
newtype StateT s m a = StateT { runStateT :: s -> m (a, s) }
type State₁ s = StateT s Identity
```

… and then we can prove that `State₀`

is isomorphic to
`State₁`

like this:

`State₀ s a ≅ s -> (a, s)`

… because the

`State₀`

`newtype`

is isomorphic to the underlying type`s -> (a, s) ≅ s -> Identity (a, s)`

… because the

`Identity`

newtype is isomorphic to the underlying type`s -> Identity (a, s) ≅ StateT s Identity a`

… because the

`StateT`

newtype is isomorphic to the underlying type`StateT s Identity a = State₁ s a`

… because of how the

`State₁`

type synonym is defined.

Therefore, by transitivity, we can conclude:

`State₀ s a ≅ State₁ s a`

Okay, now let’s introduce an **extremely useful** rule
related to isomorphic types:

If

`f`

is a`Functor`

then`forall r . (a -> r) -> f r`

is isomorphic to`f a`

.

Or in other words:

`Functor f => (forall r . (a -> r) -> f r) ≅ f a`

… and here are the two conversion functions:

```
{-# LANGUAGE RankNTypes #-}
forward :: Functor f => (forall r . (a -> r) -> f r) -> f a
= f id
forward f
backward :: Functor f => f a -> (forall r . (a -> r) -> f r)
= fmap k fa backward fa k
```

This is essentially the Yoneda lemma in
Haskell form, which is actually a bit tricky to prove. If you don’t
believe me, try proving the isomorphism laws for the above
`forward`

and `backward`

functions and see how far
you get. It’s much easier to rely on the fact that someone else already
did the hard work of proving those isomorphism laws for us.

Here’s a concrete example of the Yoneda lemma in action. Suppose that
I want to prove that there is only one implementation of the identity
function, `id`

. I can do so by proving that the type of the
identity function (`forall a . a -> a`

) is isomorphic to
the `()`

type (a type inhabited by exactly one value):

`forall a . a -> a) ≅ () (`

Here’s how you prove that by chaining together several isomorphic types:

```
forall a . a -> a)
(-- a ≅ () -> a
forall a . (() -> a) -> a)
≅ (-- a ≅ Identity a
forall a . (() -> a) -> Identity a)
≅ (-- ✨ Yoneda lemma (where f = Identity) ✨
Identity ()
≅ ≅ ()
```

… so since the `()`

type is inhabited by exactly one value
(the `()`

term) and the `()`

type is isomorphic to
the type of `id`

, then there is exactly one way to implement
`id`

(which is `id x = x`

).

Note: To be totally pedantic, there is exactly one way to implement

`id`

“up to isomorphism”. This is how we say that there might be several syntactically different ways of implementing`id`

, such as:`id x = x id y = y id = \x -> x id x = y where = x y`

… but all of those ways of implementing

`id`

are isomorphic to one another (in a slightly different sense that I have not covered), so there is essentially only one way of implementing`id.`

Similarly, we can prove that there are exactly two ways to implement
a function of type `forall a . a -> a -> a`

by showing
that such a type is isomorphic to `Bool`

(a type inhabited by
exactly two values):

```
forall a . a -> a -> a)
(-- a -> b -> c ≅ (a, b) -> c
forall a . (a, a) -> a)
≅ (-- (a, a) ≅ Bool -> a
forall a . (Bool -> a) -> a)
≅ (-- a ≅ Identity a
forall a . (Bool -> a) -> Identity a)
≅ (-- ✨ Yoneda lemma (where f = Identity) ✨
Identity Bool
≅ Bool ≅
```

… and in case you’re curious, here are the only two possible ways to implement that type (up to isomorphism):

```
{-# LANGUAGE ExplicitForAll #-}
false :: forall a . a -> a -> a
= f
false f t
true :: forall a . a -> a -> a
= t true f t
```

Here’s one last example of using the Yoneda lemma to prove that:

`forall r . (a -> r) -> r) ≅ a (`

… which you can prove like this:

```
forall r . (a -> r) -> r)
(-- Identity r ≅ r
forall r . (a -> r) -> Identity r)
≅ (-- ✨ Yoneda lemma (where f = Identity) ✨
Identity a
≅ ≅ a
```

**Exercise:** Prove that these two types are
isomorphic:

`forall r . (b -> r) -> (a -> r)) ≅ a -> b (`

## Solution (click to expand)

```
forall r . (b -> r) -> (a -> r))
(-- a -> b -> c ≅ b -> a -> c
forall r . a -> (b -> r) -> r)
≅ (-- r ≅ Identity r
forall r . a -> (b -> r) -> Identity r)
≅ (-- ✨ Yoneda lemma (where f = Identity) ✨
-> Identity b
≅ a -- Identity b ≅ b
-> b ≅ a
```

#### Isomorphism

So far we’ve only used the word “isomorphic” but there is a related word we should cover: “isomorphism”.

In Haskell, if the types `A`

and `B`

are
“isomorphic” then an “isomorphism” between them is the corresponding
pair of functions converting between them (i.e. `forward`

and
`backward`

).

The easiest way to explain this is to actually define an isomorphism type in Haskell:

```
data Isomorphism a b = Isomorphism
forward :: a -> b
{ backward :: b -> a
, }
```

For example:

```
exampleIsomorphism :: Isomorphism ((a, b) -> c) (a -> b -> c)
= Isomorphism{ forward = curry, backward = uncurry } exampleIsomorphism
```

However, this is not the only way we can encode an isomorphism in
Haskell. For example, the `lens`

package has an
`Iso`

type which can also represent an isomorphism:

```
import Control.Lens (Iso', iso)
exampleIso :: Iso' ((a, b) -> c) (a -> b -> c)
= iso curry uncurry exampleIso
```

These two types are equivalent. In fact, you might even say they are … isomorphic 👀.

```
{-# LANGUAGE NamedFieldPuns #-}
import Control.Lens (AnIso', Iso', cloneIso, iso, review, view)
data Isomorphism a b = Isomorphism
forward :: a -> b
{ backward :: b -> a
,
}
-- | We have to use `AnIso'` here instead of `Iso'` for reasons I won't go into
isomorphismIsomorphism :: Isomorphism (Isomorphism a b) (AnIso' a b)
= Isomorphism{ forward, backward }
isomorphismIsomorphism where
forward :: Isomorphism a b -> AnIso' a b
Isomorphism f b) = iso f b
forward (
backward :: AnIso' a b -> Isomorphism a b
=
backward iso Isomorphism
= view (cloneIso iso)
{ forward = review (cloneIso iso)
, backward }
```

#### Generalized isomorphisms

I mentioned earlier that the isomorphism definition we began with was not the fully general definition. In this section we’ll slightly generalize the definition, while still sticking to something ergonomic to express within Haskell:

Two types,

`A`

, and`B`

, are isomorphic if there exist two morphisms,`forward`

and`backward`

of the following types:`forward :: cat A B backward :: cat B A`

… such that

`cat`

is an instance of the`Category`

type class and the following two equations (which I will refer to as the “isomorphism laws”) are true:`. backward = id forward . forward = id backward`

… where

`(.)`

and`id`

are the methods of the`Category`

type class and not necessarily the`(.)`

and`id`

from the Prelude.

This definition is based on the `Category`

type class from the `Control.Category`

module, which is defined like this:

```
class Category cat where
-- | the identity morphism
id :: cat a a
-- | morphism composition
(.) :: cat b c -> cat a b -> cat a c
```

… and all instance of the `Category`

class must satisfy
the following three “category laws”:

```
. g) . h = f . (g . h)
(f
. id = f
f
id . f = f
```

In other words, you can think of the `Category`

class as
generalizing our notion of functions to become “morphisms” so that we
replace values of type `a -> b`

(functions) with values of
type `cat a b`

(“morphisms”). When we generalize our notion
of functions to morphisms then we can similarly generalize our notion of
isomorphisms.

Of course, Haskell functions are one instance of this
`Category`

class:

```
instance Category (->) where
id = Prelude.id
.) = (Prelude..) (
```

… so if we take our more general definition of isomorphisms and
replace `cat`

with `(->)`

then we get back the
less general definition of isomorphisms that we started with.

However, things other than functions can be instances of this
`Category`

class, too. For example, “monadic” functions of
type `Monad m => a -> m b`

can implement
`Category`

, too, if we wrap them in a newtype:

```
import Control.Category (Category(..))
import Control.Monad ((<=<))
-- Note: This type and instance already exists in the `Control.Arrow` module
newtype Kleisli m a b = Kleisli{ runKleisli :: a -> m b }
instance Monad m => Category (Kleisli m) where
id = Kleisli return
Kleisli f . Kleisli g = Kleisli (f <=< g)
```

… and that satisfies the category laws because:

```
<=< g) <=< h = f <=< (g <=< h)
(f
<=< return = f
f
return <=< f = f
```

Fun fact: The above category laws for the

`Kleisli`

type constructor are isomorphic to the monad laws (in a different sense of the world "isomorphic" that I have not covered).

Once we begin to use `Category`

instances other than
functions we can begin to explore more interesting types of “morphisms”
and “isomorphisms”. However, in order to do so we need to generalize our
`Isomorphism`

type like this:

```
data Isomorphism cat a b = Isomorphism
forward :: cat a b
{ backward :: cat b a
, }
```

… so that we can store morphisms that are not necessarily functions.

With that generalized `Isomorphism`

type in hand we can
now create a sample `Isomorphism`

in a `Kleisli`

`Category`

:

```
import Data.Monoid (Sum(..))
import Control.Monad.Writer (Writer)
writerIsomorphism :: Isomorphism (Kleisli (Writer (Sum Integer))) () ()
= Isomorphism{ forward, backward }
writerIsomorphism where
forward :: Kleisli (Writer (Sum Integer)) () ()
= Kleisli (\_ -> tell (Sum 1))
forward
backward :: Kleisli (Writer (Sum Integer)) () ()
= Kleisli (\_ -> tell (Sum (-1))) backward
```

Like before, we still require that:

```
. backward = id
forward
. forward = id backward
```

… but in this case the `(.)`

and `id`

in these
two isomorphism laws will be the ones for our `Kleisli`

type
instead of the ones for functions.

## Proof of isomorphism laws (click to expand)

I’ll skip over several steps for this proof to highlight the relevant parts:

```
. backward
forward
= Kleisli (\_ -> tell (Sum 1)) . Kleisli (\_ -> tell (Sum (-1)))
= Kleisli ((\_ -> tell (Sum 1)) <=< (\_ -> tell (Sum (-1))))
= Kleisli (\_ -> tell (Sum 0))
= Kleisli return
= id
```

`backward . forward = id`

is essentially the
same thing, except flipped.
Note our `Isomorphism`

effectively says that the type
`()`

is isomorphic to the type `()`

within this
`Kleisli (Writer (Sum Integer))`

`Category`

, which
is not a very interesting conclusion. Rather, for this
`Isomorphism`

the (slightly more) interesting bit is in the
“morphisms” (the `forward`

and `backward`

definitions), which are inverses of one another.

Here is one last example of a non-trivial `Category`

instance with an example isomorphism:

```
import Prelude hiding ((.), id)
-- Note: This is not how the lens package works, but it's still a useful example
data Lens a b = Lens{ view :: a -> b, over :: (b -> b) -> (a -> a) }
instance Category Lens where
id = Lens{ view = id, over = id }
Lens{ view = viewL, over = overL } . Lens{ view = viewR, over = overR } =
Lens{ view = viewL . viewR, over = overR . overL }
lensIsomorphism :: Isomorphism Lens Bool Bool
= Isomorphism{ forward, backward }
lensIsomorphism where
forward :: Lens Bool Bool
= Lens{ view = not, over = \f -> not . f . not }
forward
-- There is no rule that the two morphisms can't be the same
backward :: Lens Bool Bool
= forward backward
```

Again, it’s not very interesting to say that `Bool`

is
isomorphic to `Bool`

, but it is more to note that the
`forward`

lens is essentially its own inverse.

There’s one last category I want to quickly mention, which is …
`Isomorphism`

!

Yes, the `Isomorphism`

type we introduced is itself an
instance of the `Category`

class:

```
instance Category cat => Category (Isomorphism cat) where
Isomorphism forwardL backwardL . Isomorphism forwardR backwardR =
Isomorphism (forwardL . forwardR) (backwardR . backwardL)
id = Isomorphism id id
```

You might even say that an “isomorphism” is a “morphism” in the above
`Category`

. An “iso”-“morphism”, if you will (where “iso”
means “same”).

Furthermore, we can create an example `Isomorphism`

in
this `Category`

of `Isomorphism`

s:

```
nestedIsomorphism :: Isomorphism (Isomorphism (->)) Integer Integer
=
nestedIsomorphism Isomorphism
= Isomorphism{ forward = (+ 1), backward = subtract 1 }
{ forward = Isomorphism{ forward = subtract 1, backward = (+ 1) }
, backward }
```

Okay, perhaps that’s going a bit too far, but I just wanted to end this post with a cute example of how you can keep chaining these ideas together in new ways.

#### Conclusion

In my experience, the more you train your ability to reason formally about isomorphisms the more you broaden your ability to recognize disparate things as equivalent and draw interesting connections between them.

For example, fluency with many common isomorphisms is a useful skill for API design because often there might be a way to take an API which is not very ergonomic and refactor it into an equivalent (isomorphic) API which is more ergonomic to use.

Ironically, `forward function = (function False, function True)` has a bug that makes the proof fail. I suggest extracting code and proofs automatically for blog posts, e.g., via Agda or the like, to ensure proofs are checked.

ReplyDeleteAn exquisite post -- cheers!

ReplyDelete