There have been many tutorials recently motivating lenses from a practical point of view. In this post I want to try to motivate lenses from a more mathematical point of view. Actually, I want to provide motivation for three types from the lens library; `Iso`s, `Lens`es, and `Prism`s.

These roughly correspond to three concepts from category theory; isomorphisms, products, and coproducts. Even before we reach the lens library, Haskell’s type system already partly supports these three topics under different names; newtypes, record types, and sum types.

**Newtypes**

You’re probably already familiar with isomorphisms. An isomorphism in between objects and in a category consists of morphisms and such that and . From the point of view of a mathematician, isomorphic objects; that is, objects for which there exists an isomorphism between them, may be treated as essentially the same. Now thinking about Haskell types, any newtype is manifestly isomorphic to it’s…uhhh…oldtype.

newtype New = New { unNew :: Old }

Given the type `Old`, this constructs not only the type `New` but the inverse functions `New` and `unNew`.

New :: Old -> New

unNew :: New -> Old

— unNew . New = id :: Old -> Old

— New . unNew = id :: New -> New

And GHC is even clever enough to take the mathematician’s insight that one can treat isomorphic objects as essentially the same to optimize. However, not all isomorphisms need in principle to be newtypes, so the question is how to encode isomorphisms generally. The answer is to use profunctors!

**Profunctors**

type Iso s t a b = forall Profunctor p. p a b -> p s t

Whaaaaat? Well, this is somewhat mysterious so let’s take a detour and talk a bit about profunctors. If a functor is like a function between categories , then a profunctor is like a relation between categories, . Really, is just a functor which implies that it’s a bifunctor, contravariant in the first argument and covariant in the second. Just like functors, profunctors compose and there’s an identity profunctor. The identity profunctor is a good motivating example. On objects, is the set of all morphisms . On morphisms, is the function which takes a morphism to . Notice, that it was necessary to reverse the expected order of source and target morphisms for $late f$ in order for the composition to work out. This is the reason for the , indicating that profunctors are contravariant in their first argument!

In Haskell, rather than arbitrary categories we can restrict our attention to the category of Haskell types and functions. That’s right, a Profunctor is actually an endoprofunctor on Hask. Let’s recapitulate the math in Haskell.

class Profunctor p :: * -> * -> * where

dimap :: (s -> a) -> (b -> t) -> p a b -> p s t

– dimap id id = id

– dimap (h’ . h) (f . f’) = dimap h f . dimap h’ f’

instance Profunctor (->) where

dimap f h g = f . g . h

These laws express contravariance in the first term and covariance in the second term. Here’s a couple more examples of Profunctors to whet your whistle.

newtype Tagged a b = Tagged { unTagged :: b } — The type b with spooky phantom a

instance Profunctor Tagged where

dimap h f = Tagged . f . unTagged

newtype Forget r a b = Forget { unForget :: a -> r }

instance Profunctor (Forget r) where

dimap h f = Forget . ( . h) . unForget

**Isos**

How do we package our inverse functions `f :: a -> a’` and `h :: a’ -> a` into an Iso? Notice how the type signatures are perfect for fitting them into dimap. We can also get the functions back out again.

dimap h f :: Profunctor p => p a a -> p a’ a’

dimap h f :: Iso a a a’ a’

view :: Iso s t a b -> b -> t

view :: (Tagged a b -> Tagged s t) -> b -> t

view iso = unTagged . iso . Tagged

review :: Iso s t a b -> t -> b

review :: (Forget r a b -> Forget r s t) -> s -> a

review iso = (unForget . iso . Forget) id

We should check that

– review (dimap h f) = f

– view (dimap h f) = h

– dimap (view iso) (review iso) = iso

– view (dimap h f) = (unForget . (dimap h f) . Forget) id

– = (unForget . Forget . ( . h) . unForget . Forget) id = id . h = h

– review (dimap h f) = unTagged . (dimap h f) . Tagged

– = unTagged . Tagged . f . unTagged . Tagged = f

–

Here’s two examples of `Iso`s:

type New = New { unNew :: Old}

newtyped :: Iso Old Old New New

newtyped = dimap New unNew

packed :: String String Text Text

packed = dimap pack unpack

**Natural Isomorphisms**

You may have noticed the repeated types in signatures `Iso a a a’ a’`. How is it useful to have the extra type variables? One really useful application is natural isomorphisms between functors. A natural transformation between functors and consists of a pair of natural transformations and such that and . There’s no need for the component variables and of the two transformations be the same and it’s more polymorphic, so, win? Let’s look at some examples.

curried :: Iso ((a, b) -> c) ((d, e) -> f) (a -> b -> c) (d -> e -> f)

curried = dimap curry uncurry

type Tsil a = Empty | Snoc (Tsil a) a

reversed :: Iso [a] [b] (Tsil a) (Tsil b)

reversed = dimap rev unRev where

rev [] = Empty

rev (x:xs) = (rev xs) `Snoc` x

unRev Empty = []

unRev (ys `Snoc` y) = y : unRev ys

While the extra polymorphism let us write the inverse natural transformations without the same component variable, notice that the component variables are related. You’ll never have completely unrelated types `s`, `t`, `a` and `b`.

**Identity and Composition of Isos**

The cool thing about the profunctor representation of `Iso`s is that they’re just functions, so they’re just as first class as functions are. For instance, you can compose them without having to define instance of Category, just use the function composition from Prelude. There’s one weird thing about their composition though.

(.) :: (b -> c) -> (a -> b) -> (a -> c)

(.) :: Profunctor p => (p b b’ -> p c c’) -> (p a a’ -> p b b’) -> (p a a’ -> p c c’)

(.) :: Iso c c’ b b’ -> Iso b b’ a a’ -> Iso c c’ a a’

This sometimes makes it feel like Iso runs backward, but relax dude, the underlying isomorphism arrow goes both ways if you know what I mean ;-)

**Other Representation of Isos**

If you look in the lens library, the above is not the definition of `Iso` you will find. Instead you’ll find a mixed functor-profunctor representation.

type Iso s t a b = forall p f. (Profunctor p, Functor f) => p a (f b) -> p s (f t)

Even more polymorphism, amirite? I think this representation has better compatibility with Prelude, but otherwise it’s…isomorphic. There’s a yo dawg joke in there but I really don’t want to try to encode the `Iso` in my `Iso`s. There’s other encodings of `Iso`s in other libraries too. Here’s a simple one you can write. You’ll have to make your own Category instance to get composition though.

type Iso s t a b = (a -> s, t -> b)

**Products**

In category theory, a product of a finite set of objects** ** is a type along with morphisms such that the following diagram…wait for it………….commutes!!!