## Thursday, October 20, 2022

### What does "isomorphic" mean (in Haskell)?

What does "isomorphic" mean (in Haskell)

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:

``````forward . backward = id

backward . forward = id``````

`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)
(f . g) x = f (g x)``````

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)
forward function = (function False, function True)

backward :: (a, a) -> (Bool -> a)
backward (first, second) False = first
backward (first, second) True  = 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:

``````forward . backward

-- (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) ->
(backward (first, second) False, backward (first, second) True)

-- 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:

``````backward . forward

-- (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)
forward function = (function True, function False)``````

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)
(a, Either b c) ≅ Either (a, b) (a, c)

-- a ^ 1 = a
() -> a ≅ a

-- a ^ 0 = 1
Void -> a ≅ ()

-- (c ^ b) ^ a = (c ^ a) ^ b
a -> b -> c ≅ b -> a -> c

-- (c ^ b) ^ a = c ^ (a × b)
a -> b -> c ≅ (a, b) -> c``````

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
forward = getName

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

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
forward f = f id

backward :: Functor f => f a -> (forall r . (a -> r) -> f r)
backward fa k = fmap k fa``````

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
y = x``````

… 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
false f t = f

true :: forall a . a -> a -> a
true f t = 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) ✨
≅ a -> Identity b
-- Identity b ≅ b
≅ a -> b``````

#### 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)
exampleIsomorphism = Isomorphism{ forward = curry, backward = uncurry }``````

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)
exampleIso = iso curry uncurry``````

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)
isomorphismIsomorphism = Isomorphism{ forward, backward }
where
forward :: Isomorphism a b -> AnIso' a b
forward (Isomorphism f b) = iso f b

backward :: AnIso' a b -> Isomorphism a b
backward iso =
Isomorphism
{ forward  = view (cloneIso iso)
, backward = review (cloneIso iso)
}``````

#### 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:

``````forward . backward = id

backward . forward = id``````

… 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”:

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

f . id = 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(..))

-- 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:

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

f <=< return = 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(..))

writerIsomorphism :: Isomorphism (Kleisli (Writer (Sum Integer))) () ()
writerIsomorphism = Isomorphism{ forward, backward }
where
forward :: Kleisli (Writer (Sum Integer)) () ()
forward = Kleisli (\_ -> tell (Sum 1))

backward :: Kleisli (Writer (Sum Integer)) () ()
backward = Kleisli (\_ -> tell (Sum (-1)))``````

Like before, we still require that:

``````forward . backward = id

backward . forward = id``````

… 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:

``````forward . backward

= Kleisli (\_ -> tell (Sum 1)) . Kleisli (\_ -> tell (Sum (-1)))

= Kleisli ((\_ -> tell (Sum 1)) <=< (\_ -> tell (Sum (-1))))

= Kleisli (\_ -> tell (Sum 0))

= Kleisli return

= id``````
The proof of `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
lensIsomorphism = Isomorphism{ forward, backward }
where
forward :: Lens Bool Bool
forward = Lens{ view = not, over = \f -> not . f . not }

-- There is no rule that the two morphisms can't be the same
backward :: Lens Bool Bool
backward = forward``````

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
{ forward  = Isomorphism{ forward = (+ 1), backward = subtract 1 }
, backward = Isomorphism{ forward = subtract 1, backward = (+ 1) }
}``````

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.

1. 2. 