Fair warning: this post assumes some familiarity with Haskell’s `Control.Lens`

library. Source code for this post can be found here.

Recently I’ve been working on a major rewrite of the open game engine, based on some newer theoretical ideas such as this paper. A major objective is to no longer require a custom DSL, removing the dependency on Template Haskell and especially the need to maintain a parser. For reasons that are brutally obvious to anyone who’s ever programmed with open games, it’s a hard requirement to have a syntax based on name-binding: working with point-free combinators is not humanly possible at this scale. This post is a spin-off from that work, explaining how to use Haskell’s Lens library in a name-binding rather than point-free style.

The key idea is that if you have a lens of type `Lens s t a b`

, and you want to treat it as though it’s a function, then the corresponding notion of “value” is something of type `(s, t -> r)`

. That is, it’s an input for the lens’ getter, together with a *continuation* from the output of the setter. Given a lens and such a value-continuation pair, you can get an “output value” of type `(a, b -> r)`

.

It turns out that this type is already exported by `Control.Lens`

, where it’s called

```
data Context s t r = Context (t -> r) s
```

But it will be convenient to rewrite this in an isomorphic van Laarhoven style, in order that we get “lens application” for free. Here’s the key definition of this post:

```
type Value f s t r = (s -> f t) -> f r
```

Now we have a type isomorphism

```
(s, t -> r) === forall f. (Functor f) => Value f s t r
```

and we can also compose a `Value`

with a `Lens`

, using ordinary function application, to get a new `Value`

.

(It transpires that putting off the quantification over `f`

until later works much better, for the same reason that `Lens`

is defined in terms of `LensLike`

.)

Now a lens is equivalently a function that returns a `Value`

:

```
Lens s t a b === forall f. (Functor f) => s -> Value f a b t
```

We’re going to build things like the right hand side with our name-binding style, so it’s most useful to be able to go from right to left:

```
buildLens :: (s -> Value f a b t) -> LensLike f s t a b
buildLens f k s = f s k
```

If we have an ordinary value, we can upgrade it to a `Value`

that has the identity function for its continuation:

```
value :: s -> Value f s t t
value s k = k s
```

And that’s all we need! Let’s test it out by importing `Control.Lens.Tutorial`

to get some examples to play with. A recurring example in that tutorial is

```
atpx :: Traversal' Atom Double
atpx = atoms . traverse . point . x
```

Let’s rewrite it in a name-binding style:

```
atpx :: Traversal' Molecule Double
atpx = buildLens $ \molecule -> let atom = value molecule . atoms
traversal = atom . traverse
xy = traversal . point
in xy . x
```

Here you can see all the pieces in use. We lambda-abstract to bring a `Molecule`

into scope, which we then need to turn into a `Value`

using our `value`

function. Now we can apply lenses to it using function application. Because of how we postponed the quantification over `f`

, by van Laarhoven magic it works for everything in the `Lens`

type hierarchy, demonstrated here with `Traversal`

s.

One additional upside of this style is we can write local type signatures, although we need `PartialTypeSignatures`

because the quantification over f can’t be locally solved, and then by default `ghc`

spams us with its solutions for the holes:

```
atpx :: Traversal' Molecule Double
atpx = buildLens $ \molecule -> let atom :: Value _ [Atom] [Atom] Molecule
atom = value molecule . atoms
traversal :: Value _ Atom Atom Molecule
traversal = atom . traverse
xy :: Value _ Point Point Molecule
xy = traversal . point
in xy . x
```

I doubt I’m going to convince anyone to use this style to replace such a simple “linear pipeline” of lenses, but when it comes into its own is when the pipeline splits and merges, something that’s ubiquitous in my research. To demonstrate this, let’s write a lens that computes the average of two `Double`

s, and if the average is updated then it modifies both values by an equal amount in order to get the desired average:

```
average :: Lens' (Double, Double) Double
average = lens (\(x, y) -> f x y)
(\(x, y) a -> let a' = f x y
in (x - a' + a, y - a' + a))
where f x y = (x + y)/2
```

Now if we have a pair of `Atom`

s, we can write a lens to their average x-coordinate like this:

```
averageX :: Lens' (Atom, Atom) Double
averageX = ((point . x) `alongside` (point . x)) . average
```

The `alongside`

operator, exported by `Control.Lens`

, implements the tensor product of lenses, focussing onto two things at once. This is still feasible to write point-free, but it becomes humanly impossible surprisingly quickly on bigger examples.

In order to write this with name-binding we need one more thing for our library: a way of turning a pair of `Value`

s into a `Value`

of pairs. Its implementation is pretty mysterious and almost exactly the same as the implementation of `alongside`

:

```
(/\) :: Value (AlongsideLeft f b') a b t
-> Value (AlongsideRight f t) a' b' t'
-> Value f (a, a') (b, b') (t, t')
(l /\ m) k = getAlongsideRight (m (\a' -> AlongsideRight
(getAlongsideLeft (l (\a -> AlongsideLeft (k (a, a')))))))
```

Here `AlongsideLeft`

and `AlongsideRight`

are helper functors which are exported from `Control.Lens.Internal.Getter`

. Fortunately you can cheerfully use this operator without understanding its type or implementation. (`Control.Lens`

exports so many infix operators, I had to get slightly creative thinking of a name for this one.)

Armed with this operator, we can rewrite `averageX`

in name-binding style:

```
averageX :: Lens' (Atom, Atom) Double
averageX = buildLens $ \(a1, a2) -> let pos1 = value a1 . point
pos2 = value a2 . point
x1 = pos1 . x
x2 = pos2 . x
in (x1 /\ x2) . average
```

(Who thought it was a good idea to give `(.)`

the highest possible operator precedence in `Prelude`

?)

And that’s all I’ve got. I’m still on the fence about whether to build `cybercat-core`

on top of `Control.Lens`

or on top of linear lenses `s -> (a, b -> t)`

: the former allows van Laarhoven subtyping magic but it’s not clear whether I actually need that for my purposes, while the latter gives much easier type errors and is generally much easier to work with.