Welcome to the first blog post of the Heilmann Software Developer Blog! We are a smallish company in southern Germany, and we create a mobile-first work organisation app for chimney sweeps, using a full Haskell stack🎉 Yes, that's right, Haskell in the backend and the frontend.

In some future blog post, we will talk about our stack in detail. For now let it suffice to say that we have an extensive model of the work that a chimney sweep has to do, and we manipulate these nested structures using good ol' lenses. You might think that everything important about optics has already been said, but then I stumbled over something puzzling recently.

We got work to do

In Germany, chimney sweeps do a lot of different work, ranging from actual chimney sweeping to safety inspections. When they have a work package, they have to document meticulously what they have done, or why they weren't able to complete the task. After all, a furnace emitting carbon monoxide can become a death trap, so chimney sweeps are grateful for a smooth application that tracks all work steps reliably.

Let's get to it and model a unit of work!

First, we model three different kinds of work a chimney sweep can do.

-- | One chimney sweep work item
data WorkItem
  = SweepChimney (Status SweepMeters)
  | CheckFurnace (Status ())
  | MeasureCarbonMonoxide (Status CarbonMonoxideMeasurement)

-- | How many meters of chimney or flue were swept.
newtype SweepMeters = SweepMeters Int
  deriving newtype (Num)

-- | CO concentration in parts per million.
newtype CarbonMonoxideMeasurement = CarbonMonoxideMeasurement Int
  -- Deriving Num allows us to write integer literals as values of this type ;)
  deriving newtype (Num, Eq, Ord)

-- | A CO measurement above 1 permille is dangerous and has to be reported!
coLifeThreatening :: CarbonMonoxideMeasurement -> Bool
coLifeThreatening co = co > 1000

Note that we have annotated the work items with a Status, which is parametrised by a type. Let's see what that is.

A work item can be still to do, it can be done, or it might have been impossible to do the work because of some unforeseen reason. If it was done, we want to track how long it took, and we might want to attach additional information that was specific to this task. For example, when sweeping a chimney it is relevant how long the chimney is, and when measuring carbon monoxide, the measured concentration must be tracked. That's the additional type variable result in the Status type!

-- | What's the status of the work item?
data Status result
  = ToDo
  | Done result Minutes
  | NotDone Excuse

-- | Why was it not possible to complete the work?
--   Maybe the door to the building was locked and noone opened?
newtype Excuse = Excuse Text
  deriving newtype (IsString)

-- | How many minutes did it take to complete the work item. Relevant for billing.
newtype Minutes = Minutes Int
  deriving newtype (Num)

A focus on optics

We can create optics to work with these types:

makePrisms ''WorkItem
makePrisms ''Status

This Template Haskell incantation brings a few Prisms into scope, such as:

_SweepChimney :: Prism' WorkItem (Status SweepMeters)
_CheckFurnace :: Prism' WorkItem (Status ())
_MeasureCarbonMonoxide :: Prism' WorkItem (Status CarbonMonoxideMeasurement)
_ToDo :: Prism' (Status result) ()
_Done :: Prism' (Status result) (result, Minutes)
_NotDone :: Prism' (Status result) Excuse

The underscore _ in front of every prism name is the naming convention for prisms in lens.

The tick in Prism' says that this is a "simple" prism. There is a more general prism type which we won't need today.

These prisms allow us to analyse the different cases of work items and there statuses.

Just your regular optics? Look closer.

If you know your way around van Laarhoven optics or the lens package just go on reading. If prisms, lenses and optics are new or unfamiliar for you, we have a little optics primer prepared for you down below.

All work and no type signature

So let's crunch some data. How about we find out whether there was a really important high CO measurement today, so we can display a big fat red warning sign?

coWarning :: [WorkItem] -> Bool
coWarning = has
  $ traversed
  . _MeasureCarbonMonoxide
  . _Done
  . _1
  . filtered coLifeThreatening

Fantastic. Readable, maintainable, succinct, reliable through typechecking. Let's call it a day and cash in the bill!

billedMinutes :: [WorkItem] -> Minutes
billedMinutes = sumOf $ traversed . _allWorkItems . _Done . _2

We just need to fill in our hole _allWorkItems, a traversal that ranges over all work items and plucks out every Status. From there, we already know how to finish, we focus on the Done constructor, then on its second field which contains Minutes, and we have the bill. So let's work this out.

allWorkItems :: Traversal' Work (Status ...)
allWorkItems = ...

Huh. Already the type signature doesn't work out. What should be the type variable of Status?

First try: Prisms are monoids

A seasoned optics developer might tell you that prisms like _SweepChimney are monoids, and we can just <> them together:

allWorkItems = _SweepChimney <> _CheckFurnace <> _MeasureCarbonMonoxide

But GHC will quickly call you out on that:

• Couldn't match type ‘()’ with ‘SweepMeters’

And it's right! After all, the prisms focus on Statuses applied to different types.

Nevermind, we don't like this solution anyways, since it's too easy to forget a constructor here! What if we add a constructor to the WorkItem type definition later and don't add it in the allWorkItems traversal? Customers would not get billed for those work items, and that's something they'll quickly complain about😉

Second try: Hands on

Let's try and write a traversal hands-on. This is more work, but as a bonus GHC would spit out a warning if we forgot a case.

allWorkItems handler (SweepChimney status) = SweepChimney <$> handler status
allWorkItems handler (CheckFurnace status) = CheckFurnace <$> handler status
allWorkItems handler (MeasureCarbonMonoxide status) = MeasureCarbonMonoxide <$> handler status

Again:

• Couldn't match type ‘()’ with ‘SweepMeters’

No such luck. Probably there is a meaningful reason we can't get this to work.

Third try: A dirty way out

But isn't it weird that we have GHC complaining about types that we don't even care about? Let's look briefly at the type signature:

data Status result
  = ToDo
  | Done result Minutes
  | NotDone Excuse

Yes, the whole Status type depends on result, but Minutes doesn't, so why can't we just focus on them, and nothing else?

allWorkItemsMinutes :: Traversal' WorkItem Minutes
allWorkItemsMinutes handler (SweepChimney (Done result minutes))
  = SweepChimney . Done result <$> handler minutes
allWorkItemsMinutes handler workItem@(SweepChimney _)
  = pure workItem
allWorkItemsMinutes handler (CheckFurnace (Done result minutes))
  = CheckFurnace . Done result <$> handler minutes
allWorkItemsMinutes handler workItem@(CheckFurnace _)
  = pure workItem
allWorkItemsMinutes handler (MeasureCarbonMonoxide (Done result minutes))
  = MeasureCarbonMonoxide . Done result <$> handler minutes
allWorkItemsMinutes handler workItem@(MeasureCarbonMonoxide _)
  = pure workItem

This works. Tedious and lengthy, but ok. Note that we basically wrote a traversal over two structures at once: First over WorkItem, and then over Status. Not very modular!

Now how about we also create a traversal to focus on all excuses that were made in a work item? Fingers aren't even twitching: We would need to redo all of the tedious work again. Same for the ToDo constructor. And if we extend the Status type, we need to add new functions for every new constructor. Sounds like bitrot. Even worse if we reuse Status anywhere else, then we'd have to redo all of these functions!

Fourth try: We have to focus on something

The issue is that we combined two traversals, one focussing into WorkItem, and the second one into Status, in order to hide the result type. Actually, the second of these steps is not the issue here! _Done :: Prism' (Status result) (result, Minutes) is a perfectly valid prism. Yes, it's polymorphic in result, but that doesn't create a problem.

But in the first step, when diving into a WorkItem, we want to look at the Status, but ignore everything related to the result type! We don't care about the exact type of the status as long as it is, well, some status!

-- If you need this in production use https://hackage.haskell.org/package/some
data Some a = forall result . Some {getSome :: a result}

The go-to solution that might spring to mind is an existential type. Let's wrap the Status type in a Some Status container, so that users of the container don't know the result type, but they still know that it's some type of status. We could go on working with this in principle:

-- | Wrap a traversal with a type variable
withSomeStatus ::
  (forall result . Traversal' (Status result) a) ->
  Traversal' (Some Status) a
withSomeStatus traversal handler (Some status) = Some <$> traversal handler status

someMinutes :: Traversal' (Some Status) Minutes
someMinutes = withSomeStatus $ _Done . _2

All we're missing now is a traversal from WorkItem into Some Status. Should be easy, right?

workItemSomeStatus :: Traversal' WorkItem (Some Status)
workItemSomeStatus handler (SweepChimney status)
  = SweepChimney . (\(Some status) -> status) <$> handler (Some status)
workItemSomeStatus handler (CheckFurnace status)
  = CheckFurnace . (\(Some status) -> status) <$> handler (Some status)
workItemSomeStatus handler (MeasureCarbonMonoxide status)
  = MeasureCarbonMonoxide . (\(Some status) -> status) <$> handler (Some status)

But GHC disagrees:

• Couldn't match type ‘result’ with ‘SweepMeters’
  Expected: Status SweepMeters
    Actual: Status result
  ‘result’ is a rigid type variable bound by
    a pattern with constructor:
      Some :: forall {k} (a :: k -> *) (result :: k). a result -> Some a,
    in a lambda abstraction

Somehow, it doesn't agree that the handler returns a status of the expected type, and insists that the type might be anything. And... GHC is right! handler has the type Some Status -> f (Some Status), and nothing prevents us from changing the result type inside the wrapper! This is clearly not what we wanted.

Let's zoom out to a broader scope

We had two issues so far where we ran into trouble with the result type variable. Let's look at them at the same time.

A quick reminder what a Traversal' is. (The tick still means that there is a more general notion of traversal which doesn't matter here.)

type Traversal' s a = forall f . Applicative f =>
  (a -> f a) ->
  s -> f s

Our first and second tries were insert WorkItem for s and Status result for a:

type FirstAndSecondFail = forall f result . Applicative f =>
  (Status result -> f (Status result)) ->
  WorkItem -> f WorkItem

But this implied that result must be the same for the whole traversal, and it can't depend on the focus. Since it changes based on which kind of WorkItem we are looking at, we get a type error. Somehow, the scope of result is too broad

The fourth attempt tried to hide the result type very tightly. Without the data wrapper (and with ImpredicativeTypes), the type would read as:

type FourthFail = forall f . Applicative f =>
  ((forall result1 . Status result1) -> f (forall result2 . Status result2)) ->
  WorkItem -> f WorkItem

I intentionally called the type variables result1 and result2, because the issue here is precisely that there is no guarantee that they are the same. Here, the scope of the type variable is too narrow.

The solution lies in between.

There must be some traversal!

Without further ado, here is the solution. (Well, the type signature of the solution at least. (But you know, in Haskell that's often all that really matters.))

type ThisWorks = forall f .
  (forall result . Status result -> f (Status result)) ->
  WorkItem -> f WorkItem

We have given the handler an existential type variable. So once per handler call, result will be some type, and on the next handler call it can be a different one.

Put differently: When using the handler, you have to make sure that the result type stays the same.

Let's generalise this again.

type SomeTraversal' s a = forall f . Applicative f =>
  (forall x . a x -> f (a x)) ->
  s -> f s

We've renamed result to x, generalized WorkItem to s and Status to a. Note that a is not a type, it's a type operator of kind a :: Type -> Type! So let's implement some traversal.

workItemStatus :: SomeTraversal' WorkItem Status -- Note: No type variable!
workItemStatus handler (SweepChimney status) = SweepChimney <$> handler status
workItemStatus handler (CheckFurnace status) = CheckFurnace <$> handler status
workItemStatus handler (MeasureCarbonMonoxide status)
  = MeasureCarbonMonoxide <$> handler status

Sweet and simple! But does it blend? I mean, does it blend in with the rest of the code? Does it compose?

minutes :: Traversal' WorkItem Minutes
minutes = workItemStatus . _Done . _2

• Couldn't match type: Status result0 -> f (Status result0)
                 with: forall x. Status x -> f (Status x)
  Expected: (Minutes -> f Minutes)
            -> forall x. Status x -> f (Status x)
    Actual: (Minutes -> f Minutes)
            -> Status result0 -> f (Status result0)

Will it never end? What kind of horrid skolem just escaped its scope? But don't worry, there is a relatively simple solution.

infixr 9 .:

-- | Compose 'SomeTraversal'' with a regular traversal
--   in such a way that the type variable vanishes.
(.:) :: SomeTraversal' s a -> (forall x . Traversal' (a x) b) -> Traversal' s b
tsa .: taxb = \bhandler -> tsa (taxb bhandler)

The issue is just that the focus of SomeTraversal' contains an existential type variable, and we need to make sure to compose it with a traversal that accepts any type in that place. In the end, if we want to retrieve some data in a concrete type without any existentials, we have to compose workItemStatus with a traversal that accepts Status result and then focuses on something that doesn't mention result, such as _Done . _2:

minutes :: Traversal' WorkItem Minutes
minutes = workItemStatus .: _Done . _2

And that's it! We're back in good ol' standard optics land.

Thanks for reading!

Addenda

What, you're still reading? Ok, there is a bit more to say. A bit advanced material in this section, you have been warned!

Some action

Inevitably, you might want to retrieve the status of a work item. In standard lens, you can do this with an action such as ^?:

(^?) :: Traversal' s a -> s -> Maybe a

Of course, this won't work here:

sweepingChimneyStatus :: Maybe (Status SweepMeters)
sweepingChimneyStatus = SweepChimney (Done 23 42) ^? workItemStatus

• Couldn't match type: forall x.
                       Status x
                       -> Const (Data.Monoid.First (Status SweepMeters)) (Status x)
                 with: Status SweepMeters
                       -> Const
                            (Data.Monoid.First (Status SweepMeters)) (Status SweepMeters)

Never mind the Const (Data.MonoidFirst ...) bit. That's got to do with the kind of operation we are performing. The important bit is that forall x . Status x ... is not Status SweepMeters. We're not allowed to sneak in a forall x here.

And it kind of makes sense! Our new existential traversal makes a big point of not knowing the type parameter, so we shouldn't be expecting an action on it to be able to specify that type.

Instead, we need to hide it somehow. Remember Some Status?

data Some a = forall result . Some {getSome :: a result}

We can use this to hide the result type of the output of our action:

(^?:) :: SomeTraversal' s a -> s -> Maybe (Some a)
stsa ^?: s = getFirst $ getConst $ stsa (Const . First . Just . Some) s

Other optics

Everything we've done here applies to other kinds of optics as well, as long as they are encoded in van-Laarhoven style. A very general optic can be defined like this:

type SomeLensLike f s t a b = (forall tag. a tag -> f (b tag)) -> s -> f t

If you quantify f and give it type classes like Functor, Applicative, ..., you recover existential lenses, traversals, and so on.

Other encodings

When people hear about optics and existentials, they often think about the existential encoding of optics. This is completely orthogonal to what is discussed here, but I believe the two can be combined! Homework exercise for you.

Profunctors

Nowadays, no blog post about optics is complete without a mention of profunctor optics. So here it is!

This whole spiel can also be generalised to profunctor optics:

-- | Hide a type variable in the input & output types of the profunctor
data SomeProfunctor p a b = forall x . SomeProfunctor {getSomeProfunctor :: p (a x) (b x)}

-- This goes from profunctors on regular Haskell types to type operators!
type SomeProfunctorOptic' p s a = p s s -> SomeProfunctor p a a

For p = (->), we recover our existential optics from before. But with this generalisation, we can also tackle prisms, indexed optics, and so on.

A quick optics primer

Prisms and lenses are special cases of "optics". Optics are a particular family of constructions to analyse manipulate complex nested data structures. There are many different concepts and implementations of optics with numerable tradeoffs which we won't cover here. We are concerned with a very direct and simple approach to optics, the "van Laarhoven style", where optics are simply a particular sort of higher order functions.

Let's look at one particular kind of optics that generalises prisms and lenses, namely traversals.

Often we have a nested data structure that has some small bits deep inside it, and we want to, well, "do" something with them. For example, extract, overwrite, or modify them. In our chimney sweep example, we might want to go through a list of work items and filter out all the excuses. Or sum up all of the Minutes of work. Or check whether there was a dangerous carbon monoxide measurement anywhere in the list. And so on.

A very general pattern capturing many kinds of operations on a data structure is a traversal:

type Traversal' s a
  = forall f . (Applicative f)
  => (a -> f a)
  ->  s -> f s

This is a quite a bit to unwrap here. The s type is the big, nested data structure. a is the type of "small bits", which we'll call the focus in the following. And f is the kind of operation we are allowed to do, we'll see in a second how that can be.

The big picture here is that a traversal accepts a handler a -> f a which operates on a focus, and returns a function s -> f s. In our example, a might be the type Minutes, while s might be [WorkItem] (or even some bigger data structure like Map Date [WorkItem]).

With the handler, a user of the traversal can specify what should happen with each focus. For example, we might want to modify the minutes value and multiply it by 2 in order to pretend that all the work took twice as long today😉 Or we could sum up all the minutes. The traversal then aggregates all the operations on the foci in one operation on the big structure.

This is where the forall f part comes in. The user can not only choose the handler, it can also choose the type of f, that is, they can choose what kind of operation to perform! For example, f = Identity means that the handler is isomorphic to Minutes -> Minutes, and the resulting function of type [WorkItem] -> [WorkItem], so we can modify each focus with the handler, and get a modified data structure. A sort of nested functor! But we could also choose f = Const (Sum Minutes), so the handler type becomes Minutes -> Const (Sum Minutes) which is just a tedious wrapping of newtypes, and the resulting function is [WorkItem] -> Const (Sum Minutes). Magically, we can sum up all minutes of work with the same traversal. The only restriction about f is Applicative f, but there are many useful such fs around.

You may say that these traversals sound nice and powerful, but how would we create them? Luckily, all Prism's from above are special cases of traversals!

Also, every Traversable structure (lists, maps, even your own types when you DeriveTraversable!) gives a traversal:

traversed :: Traversable t => Traversal' (t a) a

And what's more, the lens package also provides Lens'es which focus on parts of a tuple:

_1 :: Lens' (result, Minutes) result
_2 :: Lens' (result, Minutes) Minutes

Since every lens is also a traversal, we now have a huge library of these structures to play with.

Are you ready for the punch line?

🥁🥁🥁

Optics compose.

Given a traversal from WorkItem to Status SweepMeters, such as _SweepChimney, and a traversal from Status SweepMeters to Excuse, such as _NotDone, we can create a composed traversal:

chimneyNotSwept :: Traversal' WorkItem Excuse
chimneyNotSwept = _SweepChimney . _NotDone

Finally, a note on what is often called "actions" on an optic. We already said that choosing the applicative functor f basically determines what kind of operation we perform on the data structure. But often the result type is a bit unwieldy because of many newtype wrappers (like Const, Identity, Sum, and so on), so it is useful to create little helper functions that monomorphize f to a particular type, and unwraps all the newtypes.

For example, let's choose f x = Const [a] x, which is an applicative because [a] is a monoid:

traversalToList :: s -> Traversal' s a -> [a]
traversalToList s t = s & t (Const . pure) & getConst

Other popular examples (with simplified type signatures) from the lens library include:

-- | Whether the traversal has any matches
has :: Traversal' s a -> s -> Bool

-- | Compute the sum of all foci
sumOf :: Num a => Traversal' s a -> s -> a

That's it for now! If you've read and understood this crash course, and your brain hasn't exploded yet, congratulations! You can jump back to the main post.