Edward Kmett recently published a very interesting exploration of modeling Cellular Automata using lenses and comonads. Within it he suggested one might want to peer down the rabbit hole at a very interesting Haskell type, the Pretext.

newtype Pretext s a = Pretext { 
    runPretext :: forall f. Functor f => (s -> f s) -> f a 
  } deriving Functor

In particular, he suggested that it was a total characterization of the Store comonad used throughout the rest of that article, and further that it's an enlightening challenge to define the Comonad instance for Pretext.

To me that was invitation enough to finally figure out what those Pretexts are after seeing them far too often in Lens code.

Warning, spoilers ahead. By the end of this article I will explain how to write a comonad instance for Pretext and how Pretext and Store are related. It's a little messy and a little neat but will hopefully dramatically simplify the relationship between these two types. Try it yourself first if you don't want the spoilers.

Store and Experiment

Let's look at Store itself again. Its definition is rather understated.

data Store s a = Store s (s -> a)

instance Functor (Store s) where
  fmap f (Store s k) = Store s (f . k)

It's a function application with a "privileged" point in the domain. This privileged point gives us the Comonadic extract.

extract :: Store s a -> a
extract (Store s k) = k s

we also might want to move that point around to change our focus

seek :: (s -> s) -> (Store s a -> Store s a)
seek f (Store s k) = Store (f s) k

One intuition for a Store comonad is it's a pointer into a particular codomain, a particular strand (or fiber) stretching from the domain to the codomain extended over any number of extra mapping steps stacked atop via fmap h. We can always begin these strands in the identity mapping as well.

exact :: s -> Store s s
exact s = Store s id

Getting to the meat of this article, we also might want to perform an experiment on a Store, which might be thought of as perturbing our privileged point in a computational context and seeing what final result occurs.

experiment :: Functor f => Store s a -> (s -> f s) -> f a
experiment (Store s k) f = k <$> f s

This was the core of using Store to model cellular automata—experimenting in the [] context allows the Stored rule to be stretched across the entire state of the automata. Taken in one light this might be just one of many things you could do with a Store comonad, but I'd like to explore the idea that experimenting on Stores is using them to the absolute fullest. In particular, I'm going to eventually show that s is isomorphic to experiment s.

Some Pretext first

Let's, as described in Edward's article define exactly the result of experimenting on a Store as a Pretext.

newtype Pretext s a = 
  Pretext { runPretext :: runPretext :: forall f. Functor f => (s -> f s) -> f a }

instance Functor (Pretext s) where
  fmap f (Pretext k) = Pretext (fmap f . k)

experiment :: Store s a -> Pretext s a
experiment (Store s k) = Pretext $ \f -> k <$> f s

Since the claim is that Pretexts are just as powerful as Stores we ought to be able to define instance Comonad (Pretext s).

instance Comonad (Store s) where
  extract (Store s k) = k s
  duplicate (Store s k) = Store s (\s -> Store s k)

instance Comonad (Pretext s) where
  extract   :: Pretext s a -> a
  extract   (Pretext k) = ???

  duplicate :: Pretext s a -> Pretext s (Pretext s a)
  duplicate (Pretext k) = Pretext $ \(f :: forall f . Functor f => s -> f s) -> ???

For each function we become the users of a Pretext and must carefully construct functors and injections inj :: s -> f s that we give to the Pretext in order to get the results we want. Doing this directly is a little bit challenging, so instead we'll examine the correspondence between Store and Pretext more directly.

Reverse Engineering a Pretext

Let's analyze Pretexts through reverse engineering in the style of Dan Piponi's Reverse Engineering Machines. For a particular s and a particular a we have a machine m :: (s -> f s) -> f a that works for any Functor => f we can imagine. Is it possible to reverse engineer that machine?

How can the machine possibly work? Since it doesn't know what Functor we're going to choose nor how we're going to inject s there's not a whole lot that can be going on behind the scenes. Here are some things that can't be happening, for instance.

The machine cannot simply contain a secret f a and return it like m = const secret_f_a since while it does know what a is it cannot know which Functor we're going to choose ahead of time.
It also can't have a secret a and examine the injection we give it to get f, since if all it knows about f is that it's a Functor the machine will have no way to uniformly get its secret a inside of f: there is no such function forall f . Functor f => a -> f a.

Let's look at it from a different angle. Assuming the machine uses what we give it, it almost certainly must apply our injection function to some secret s which it's holding on to. Once it's done that it'll have (our_injector :: s -> f s) (secret_s :: s) :: f s. Can it get an f a from an f s regardless of f?

Of course, if it has a function go :: s -> a it can always use fmap go :: f s -> f a.

By this exploration, we can come to believe that any implementation of Pretext s a must secretly contain an s and a s -> a—which is exactly what we need to build a Store s a as well. This suggests that there ought to be a function like this

guess :: Pretext s a -> Store s a

Can we build it?

The finer points of Pretext

Since Store is just a product type, let's build guess one piece at a time. We want to find some sequence of operations with our Pretext machine that gets it to hand us its secret s and then some other sequence that gets it to give us its secret s -> a.

guess (Pretext m) = Store (get_s m) (get_s_to_a m)

Store smuggling

What is the type of get_s?

get_s (m :: forall f . Functor f => (s -> f s) -> f a) :: s

Since the return type of m is f a there's no way we can get m to give us its secret s directly... we'll need to smuggle it out inside of f. For instance, if f we (s, a) then the return type of m would be (s, a) and we could just look at the fst component to get our needed s.

Unfortunately, we can't build an injector s -> (s, a) without an a, which we don't have. Instead, we'll need a different trick---a Functor which actually holds a secret payload while only pretending to hold its real payload.

newtype Secret s a = Secret { openOSesame :: s }   -- this is also known as `Const`, btw.

instance Functor (Secret s) where
  fmap _ (Secret s) = Secret s

secret :: s -> Secret s s
secret = Secret

This trick functor Secret does just what we want. It uses a phantom type to appear to be holding an a while actually fully ignoring any fmapping that happens to it in order to just protect its hidden cargo. Finally, the injector function secret builds a Secret s a without ever needing an actual a. What happens when we use this injector on m?

openOSesame $ (m :: forall f . Functor f => (s -> f s) -> f a) (secret :: s -> Secret s a)
===
openOSesame $ (m :: (s -> Secret s s) -> Secret s a) (secret :: s -> Secret s a)
===
openOSesame $ (m secret :: Secret s a)
===
openOSesame (m secret) :: s    -- ka. boom.

Our Secret container does the trick and we smuggle the context s out of the Pretext m.

get_s m = openOSesame (m secret)

Storing functions

We can use pretty much the same trick to extract the Pretext's s -> a map as well. We want a box which ignores one thing while secretly capturing and preserving another. In this case, unlike above, we want to ignore the s that gets passed during injection and nab the function which gets passed by fmap. Can we do that?

I'll skip the longer exploration this time and note that if we take advantage of the law f . id == f we have a very handy way of capturing functions.

newtype Capture s a = Capture { release :: s -> a }

instance Functor (Capture s) where
  fmap f (Capture s) = Capture (f . s)   -- append the function to capture it

capture :: s -> Capture s s
capture _ = Capture id                   -- id won't affect our captured function

Which lets us define

get_s_to_a m = release (m capture)

Guessing the merchandise

Together these pieces build our guess function just right while also giving a lot of intuition about what Pretext must be doing behind the scenes. If we look back at experiment it's a complete description.

experiment (Store s k) = Pretext $ \f -> k <$> f s

apply the given injector to the Store's s and then fmap the Store's k :: s -> a over the result.

And then guess just packs up our smuggling functors to rebuild the Store.

guess :: Pretext s a -> Store s a
guess (Pretext m) = Store (openOSesame $ m secret) (release $ m capture)

With these pieces, we can prove that guess and experiment are isomorphisms.

guess . experiment
===
\store@(Store s k) -> guess . experiment $ store
===
\(Store s k) -> guess $ Pretext $ \f -> k <$> f s
===
\(Store s k) -> (\(Pretext m) -> Store (openOSesame $ m secret) (release $ m capture)) $ Pretext $ \f -> k <$> f s
===
\(Store s k) -> (\m -> Store (openOSesame $ m secret) (release $ m capture)) $ \f -> k <$> f s
===
\(Store s k) -> Store (openOSesame $ (\f -> k <$> f s) secret) (release $ (\f -> k <$> f s) capture)
===
\(Store s k) -> Store (openOSesame (k <$> secret s)) (release (k <$> capture s))
===
\(Store s k) -> Store (openOSesame (k <$> Secret s)) (release (k <$> Capture id))
===
\(Store s k) -> Store (openOSesame (Secret s)) (release (Capture (k . id)))
===
\(Store s k) -> Store s (k . id)
===
\(Store s k) -> Store s k 
===
id

Though the other direction is significantly tougher. (The proof, due to Russell O'Connor, Appendix C relies on generating a free theorem from the parametricity of Pretext, clearly necessary to bootstrap the meaning it has.)

Another way of looking at it

One particularly interesting simplification of guess comes from noting that Secret and Capture both represent two sides of the Store comonad, the pointer in to the domain and the mapping function respectively. It turns out that given the right injection function and extraction functions, we can use Store itself to replace both Secret and Capture. Here's an alternative definition of guess.

guess :: Pretext s a -> Store s a
guess (Pretext m) = Store (pos $ m exact) (peek $ m exact)
  where
    pos :: Store s a -> s
    pos (Store s _) = s
    peek :: Store s a -> (s -> a)
    peek (Store _ k) = k

This is absolutely the "right" want to see the correspondance between Pretext and Store.

So what about Comonads?

I promised at the start that this whole effort would go toward defining instance Comonad (Pretext s) but we haven't even looked at that yet. What gives?

Well, given an isomorphism we have a really trivial definition of Comonad—we'll just lift it from Store.

instance Comonad (Store s) where
  extract (Store s k)  = k s
  extend f (Store s k)  = Store s (f . flip Store k)
  duplicate (Store s k) = Store s (flip Store k)

instance Comonad (Pretext s) where
  extract = extract . guess
  extend f = experiment . extend (f . experiment) . guess
  duplicate = experiment . fmap experiment . duplicate . guess

But that's unfair, right? Fortunately, this is Haskell and we can just expand our isomorphisms and simplify mechanically using equational reasoning to get a more compact definition.

Extract

experiment . guess
===
\(Pretext m) -> (\(Store s k) -> k s) $ Store (openOSesame $ m secret) (release $ m capture)
===
\(Pretext m) -> (peek $ m exact) (pos $ m exact)
===
\(Pretext m) -> peek <*> pos $ m exact

Duplicate

experiment . fmap experiment . duplicate . guess
===
\(Pretext m) -> (Pretext $ \f -> (\s -> Pretext $ \f -> (peek $ m exact) <$> f s) <$> f (pos $ m exact))

instance Comonad (Pretext s) where
  extract (Pretext m)   = peek <*> pos $ m exact
  duplicate (Pretext m) = 
    Pretext $ \f ->     f (pos $ m exact)
                    <&> \s -> Pretext $ \f -> (peek $ m exact) <$> f s

Which I'm glad to only ever have to write once.

Comments on Reddit

Pretext by experiments and guesses

Sections