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(..))
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:

(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(..))
import Control.Monad.Writer (Writer)

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

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.