Posted on January 4, 2017

Monadic profunctors work to compose invertible parsers and lenses in very similar ways. Here I present a perspective unifying the two, and a spectrum of transformations inbetween.

First, let me outline another example which got me on this track.

``````{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE FlexibleContexts #-}

import Data.Profunctor``````

### Zippers

``````data Tree a = Leaf | Node (Tree a) a (Tree a)
deriving (Eq, Show)

isLeaf, isNode :: Tree a -> Bool

isLeaf Leaf = True
isLeaf _ = False

isNode (Node _ _ _) = True
isNode _ = False

data Cxt a = L a (Tree a) | R (Tree a) a

data Zipper a = Zipper [Cxt a] (Tree a)

toZipper :: Tree a -> Zipper a
toZipper = Zipper []

toTree :: Zipper a -> Tree a
toTree (Zipper [] t) = t
toTree (Zipper (L a r : cxt) l) = toTree (Zipper cxt (Node l a r))
toTree (Zipper (R l a : cxt) r) = toTree (Zipper cxt (Node l a r))``````

A zipper represents a “position” within a tree, allowing fast operations around that position. If we’re not at a leaf position, we can focus further down, in the left or right subtree.

``````unzipZ :: Zipper a -> (Zipper a, Zipper a)
unzipZ (Zipper cxt (Node l a r)) =
(Zipper (L a r : cxt) l, Zipper (R l a : cxt) r)
unzipZ (Zipper _ Leaf) = error "Can't unzip leaf."``````

Or we can focus back up if we’re not at the root.

``````zipZ :: Zipper a -> Zipper a
zipZ (Zipper (L a r : cxt) l) = Zipper cxt (Node l a r)
zipZ (Zipper (R l a : cxt) r) = Zipper cxt (Node l a r)
zipZ (Zipper [] _) = error "Can't zip root."``````

We can navigate monadically in a tree using a `Zipper` as state.

``````newtype ZipperM e x a = ZipperM (State (Zipper e) a)

We can look where we are currently, whether it is a `Node` containing a value or an empty `Leaf`.

``````look :: ZipperM e x (Maybe e)
look = ZipperM \$ do
Zipper _ t <- get
pure \$ case t of
Leaf -> Nothing
Node _ e _ -> Just e``````

And we can move around using monadic actions.

``````moveLeft, moveRight, moveUp :: ZipperM e x ()
moveLeft  = ZipperM (modify (fst . unzipZ))
moveRight = ZipperM (modify (snd . unzipZ))
moveUp    = ZipperM (modify zipZ)``````

Here’s a traversal of the right spine of a tree.

``````traverseRightSpine :: ZipperM e x [e]
traverseRightSpine = do
e' <- look
case e' of
Nothing -> pure []
Just e ->
moveRight *>
((e :) <\$> traverseRightSpine)``````

We can run `ZipperM` actions to “read” trees to values.

``````runZipperM :: ZipperM e x a -> Tree e -> a
runZipperM (ZipperM f) = evalState f . toZipper

aTree :: Tree Int
aTree = Node (Node Leaf 0 Leaf) 1 (Node (Node Leaf 2 Leaf) 2 Leaf)

xs :: [Int]
xs = runZipperM traverseRightSpine aTree
-- [1,2]``````

Let’s use our profunctor technique to convert back values to trees. In fact, we get a way to update trees with a value, but we can also use this to generate trees from a single `Leaf`.

``````newtype ReZipperM e x a = ReZipperM (R.ReaderT x (State (Zipper e)) a)

runReZipperM :: ReZipperM e x a -> x -> Tree e -> Tree e
runReZipperM (ReZipperM f) x t =
toTree \$ f `R.runReaderT` x `execState` toZipper t

-- ZipperM = State (Zipper e) a
-- ReZipperM = s -> State (Zipper e) a``````
``````instance Profunctor (ZipperM e) where
rmap = fmap
lmap _ (ZipperM f) = ZipperM f

instance Profunctor (ReZipperM e) where
rmap = fmap
lmap f (ReZipperM g) = ReZipperM (R.withReaderT f g)

class Poke p where
poke :: p e (Maybe e) (Maybe e)
left :: p e x ()
right :: p e x ()
up :: p e x ()

instance Poke ZipperM where
poke = look
left = moveLeft
right = moveRight
up = moveUp

instance Poke ReZipperM where
poke = ReZipperM \$ do
modify \$ \(Zipper cxt t) ->
Zipper cxt \$ case (e_, t) of
(Nothing, _) -> Leaf
(Just e, Leaf) -> Node Leaf e Leaf
(Just e, Node l _ r) -> Node l e r
pure e_
left  = ReZipperM (modify (fst . unzipZ))
right = ReZipperM (modify (snd . unzipZ))
up    = ReZipperM (modify zipZ)``````

And here is the traversal again, but now polymorphic.

``````rightSpine
:: (Poke p, Profunctor (p e), Monad (p e [e]))
=> p e [e] [e]
rightSpine = do
case e' of
Nothing -> pure []
Just e -> fmap (e :) . lmap tail \$ right *> rightSpine

safeHead :: [a] -> Maybe a
safeHead (a : _) = Just a

ys :: [Int]
ys = runZipperM rightSpine aTree

-- Write a new spine.
anotherTree :: Tree Int
anotherTree = runReZipperM rightSpine [4, 5, 6, 7] aTree

testTrees :: IO ()
testTrees = do
print xs
print ys  -- Should be equal.
print aTree
print anotherTree``````

We can use the same code to read from and write to trees.

## Partial Sources and Coupling

My bidirectional examples all have a common point: there is a source type which is read from in one direction, and written to in another. Parsers and printers read and write strings, a lens gets and puts views from and into the source, and the zipper monads above read and write trees.

We can also compare the way a “reader” can correspond to a “writer”. In order to reuse the same code, the writer has to behave quite like the reader while having only partial information about the source, since the writer is the one producing it.

We can represent this information in a poset of partial sources (i.e., “partially defined sources”) ordered by definedness. `s > t` if `s` is “more defined” than `t`. There is a bottom value `Bot` smaller than any other corresponding to the absence of information. Another way to look at this is that these partial sources represent sets of fully defined sources, ordered by inclusion: a value `s` is more defined than `t` if `s` represents a subset of sources of `t`; `Bot` represents the set of all sources.

Printers are associated with a poset of prefixes, which can be open- or close-ended (depending on whether the last element is `Bot` or `Nil`). A close-ended prefix represents a single string (it is a “fully defined” value), while an open-ended one represents all strings it is a prefix of.

``````data Prefix
= PrefixBot
| PrefixCons Char Prefix
| PrefixNil

prefixLEq :: Prefix -> Prefix -> Bool
prefixLEq PrefixBot _ = True
prefixLEq PrefixNil PrefixNil = True
prefixLEq (PrefixCons a p) (PrefixCons b q) =
a == b && prefixLEq p q
prefixLEq _ _ = False``````

`ReZipperM` has a poset of “tree prefixes”.

``````data TreePx e
= TreePxBot
| TreePxLeaf
| TreePxNode (TreePx e) e (TreePx e)

treePxLEq :: Eq e => TreePx e -> TreePx e -> Bool
treePxLEq TreePxBot _ = True
treePxLEq TreePxLeaf TreePxLeaf = True
treePxLEq (TreePxNode l e r) (TreePxNode l' e' r') =
e == e' && treePxLEq l l' && treePxLEq r r'
treePxLEq _ _ = False``````

Lenses can live with lots of different posets. Using the set of values interpretation, the most general representation of partial sources of type `s` is simply as subsets, or indicator functions `s -> Bool`. In the perspective presented here, lenses thus generalize the preceding two examples.

``````-- Power set of a.
type Partial s = s -> Bool``````

We say that a source `s` completes `p :: Partial a` if `p s = True`, i.e., `s` belongs to the set of values represented by the partial value `p`.

A reader maps a fully defined source to a value:

``type Reader s a = s -> a``

A writer maps a value and a partial source to a more defined source. It may not be fully defined, in which case a domain-specific completion method must be provided, e.g., using a default value to fill undefined holes.

``````type Writer s x = x -> Monotonic s

-- Makes a partial value more defined.
type Monotonic s = Partial s -> Partial s``````

Note that `Monotonic Source` is a monoid, hence “writer”.

We say that `r :: Reader source value` and `w :: Writer source value` are coupled if if writing then reading results in the same value.

For all `v :: value`, `p :: Partial source`, and `s :: source`, if `s` completes `w v p`, then `r s = v`.

We may also consider the other identity, that reading a value from an initial source and then writing it results in the same source, up to some completion, but this is often too strong a requirement. For instance, parsers can read many strings to the same AST, if they differ only in whitespace for example, but one only needs a (pretty-)printer to write each AST as a single source string, discarding other alternatives.

The type of readers is a monad, but the type of writers is not, because `x` is in negative position.

A rewriter is a writer with an extra function. We can make this type a monad with respect to the last parameter, which is the result type of the function.

``type Rewriter s x a = (x -> Monotonic s, x -> a)``

We thus reformulate coupling between `r :: Reader source value` and `(w, f) :: Rewriter source unvalue value`.

For all `x :: unvalue`, `p :: Partial source`, and `s :: source`, if `s` completes `w x p`, then `r s = f x`.

`pure` actions are clearly coupled. We can also check that coupling is preserved by `lmap` and `(>>=)`.

``````pure :: a -> (Reader s a, Rewriter s x a)

lmap
:: (y -> x)
-> (Reader s a, Rewriter s x a)
-> (Reader s a, Rewriter s y a)

(>>=)
:: (Reader s a, Rewriter s x a)
-> (a -> (Reader s b, Rewriter s x b))
-> (Reader s b, Rewriter s x b)``````

### Inconsistency

A rewriter may fail because it tries to write content which is inconsistent with known information. That inconsistency can be represented by the greatest value `Top`, associated with no fully defined value.

``````top :: Partial a
top _ = False``````

### Cursor

`ZipperM` and parsers, both hold a cursor to the location from which values are read and to which they are written. `ZipperM` provides specialized actions to move the cursor around (`left`, `right`, `up`), while the parser implicitly moves the cursor forward as the input is consumed.

This can be represented in our model as a state transformer on top of `Reader` and `Rewriter`, containing that cursor as state.