Functorial Blog - Comonads for Optionality

Motivation

I've been thinking more about comonads as spaces of user interface states lately. You might like to read that blog post before continuing here, if you haven't already.

Based on the notes in some of my recent blog posts, we have comonads for describing almost all useful compositions of user interfaces:

Independent adjacent components, using Day convolution
Static lists of components, using the free Applicative functor
Components with shared state, constructed using equalizers of comonads

This approach certainly seems to be a useful source of new comonads! But there is one sort of component which is notably missing from this list - components for optional data.

Consider the Coproduct comonad. This allows us to represent components with two possible classes of states, which is useful. But the implementation of duplicate means that we cannot move between those two classes. There is no function that we can extend over a Coproduct in order to move from the left to the right, or back again.

Compare this to a component for a list of subcomponents which is built from the free applicative. Since the free applicative is essentially built from coproducts and Day convolution, we end up being able to manipulate the state of each list, but unable to change the length of the list or permute its elements.

In this post, I'll show how we can create a Comonad to recover this sort of functionality.

Inspiration

Let's consider the Store comonad. This comonad certainly allows us a lot of freedom - we can move freely to any other state we want!

To see why we are able to change the state s, we can look at the Extend instance:

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

instance extendStore :: Extend (Store s) where
  extend f (Store s get) = Store s \next -> f (Store next get)

Notice that f receives the store refocussed at the next state.

We can take this as inspiration for our new comonad.

Comonads for optionality

Let's start by creating a comonad with two possible states: empty and non-empty. The possible states in the non-empty case will be represented by some other comonad w.

We could start with a Store with two possible states, represented by the Boolean type. But this wouldn't work, because the return type a needs to depend on the current boolean state. If the boolean is true (representing an empty state), we can return a value of type a (there is only one empty state, after all), but if the boolean is false (representing a non-empty state), then we need to return a value of type w a (representing all possible future states of the subcomponent).

So what we really need is some sort of "dependent store" comonad:

data DependentStore index (w :: index -> * -> *) a = DependentStore index ((i :: index) -> w i a)

Here, the comonad w is parameterized by an index type, and the choice of comonad in the result depends on the new index that we receive.

Of course, we can't represent this type in Haskell directly, but fortunately, we don't need to in the case of a Boolean-valued index, since a dependent function from a Boolean can be represented directly as a product:

data Optional w a = Optional Boolean a (w a)

The idea here is that the a argument here tracks the case where the incoming Boolean is true, and the w a tracks the case where it is false. With that in mind, we can write out our Store-inspired instances:

instance extendOptional :: Extend w => Extend (Optional w) where
  extend f (Optional b a wa) =
    Optional b
             (f (Optional true a wa))
             (extend (f <<< Optional false a) wa)

instance comonadOptional :: Comonad w => Comonad (Optional w) where
  extract (Optional true a _) = a
  extract (Optional false _ wa) = extract wa

There are a couple of interesting things to note here:

The f function passed to extend receives a refocussed comonad, whose state is true or false depending on if it is being used to redecorate the left-hand a or the right-hand w a. This is just like in the Store case above.
The extract function behaves as if it were passing the current state into the (dependent) function, so it takes the left-hand a if the current state is true, or extracts from the right-hand w a if the state is false.

This comonad is enough to model user interfaces with optional subcomponents, such as tabs, but we can do more!

Comonads for lists

A linked list is isomorphic to an optional pair of its head and its tail:

List a ~ Maybe (Tuple a (List a))

Similarly, we can use our Optional comonad to build a comonad for lists of subcomponents:

newtype ListOf w a = ListOf (Optional (Day w (ListOf w)) a)

In the definition of ListOf, we use Day convolution to represent the conjunction of the component modeling the head of the list, and the component modeling the tail.

This is a Comonad by construction. Since this is a newtype, we can even derive its instances:

derive newtype instance extendListOf :: Extend w => Extend (ListOf w)
derive newtype instance comonadListOf :: Comonad w => Comonad (ListOf w)

The ListOf w a type represents an infinite structure, with alternatives for every possible future length of our list. We can extend a function across this structure which changes the length to any new length we want.

Another approach to lists

In fact, there is another way to construct a component for lists - we can consider a list to be indexed by its length, and use our dependent store comonad:

data ListOf' w a = ListOf' Nat ((n :: Nat) -> FreeAp n w a)

(again, of course, this type is not representable directly in Haskell or PureScript)

Here, FreeAp is an indexed free applicative functor, indexed by the number of copies of w that it contains:

data FreeAp (n :: Nat) w a where
  Nil :: Identity a -> FreeAp 0 w a
  Cons :: Day w (FreeAp n w) a -> FreeAp (n + 1) w a

So we can think of our dependent store comonad as recovering some of the dynamic behavior that we lost when we modeled our list using the free applicative.

Conclusion

This construction fills in the remaining gap in the comonads as spaces approach to user interfaces, and suggests a new interesting way to build new comonads from old. We can construct models for optional subcomponents, and as we've seen, for lists of subcomponents.

I'd like to thank Arthur Xavier for providing valuable feedback and testing on the ideas presented here.

Appendix: Proofs of the comonad laws

`extract . duplicate = id`

extract (duplicate e@(Optional b a wa))
= if b then (Optional true a wa) else extract (map (Optional false a) (duplicate wa))
= if b then e else Optional false a wa
= if b then e else e
= e

`map extract . duplicate = id`

map extract (duplicate e@(Optional b a wa))
= map extract (Optional b (Optional true a wa) (map (Optional false a) (duplicate wa)))
= Optional b (extract (Optional true a wa)) (map extract (map (Optional false a) (duplicate wa))))
= Optional b a (map (extract <<< Optional false a) (duplicate wa)))
= Optional b a (map extract (duplicate wa)))
= Optional b a wa
= e

`duplicate . duplicate = map duplicate . duplicate`

duplicate (duplicate e@(Optional b a wa))
= duplicate (Optional b (Optional true a wa) (map (Optional false a) (duplicate wa)))
= Optional b (Optional true (Optional true a wa) (map (Optional false a) (duplicate wa))) (map (Optional false (Optional true a wa)) (duplicate (map (Optional false a) (duplicate wa))))
= Optional b (duplicate (Optional true a wa)) (map (Optional false (Optional true a wa)) (duplicate (map (Optional false a) (duplicate wa))))
= ... (see lemma below)
= Optional b (duplicate (Optional true a wa)) (map duplicate (map (Optional false a) (duplicate wa)))
= map duplicate (Optional b (Optional true a wa) (map (Optional false a) (duplicate wa)))
= map duplicate (duplicate e@(Optional b a wa))

Proof of Lemma

map (Optional false (Optional true a wa)) (duplicate (map (Optional false a) (duplicate wa)))
= map (Optional false (Optional true a wa)) (map (map (Optional false a)) (duplicate (duplicate wa)))
= map (Optional false (Optional true a wa) <<< map (Optional false a)) (map duplicate (duplicate wa))
= map (\w -> Optional false (Optional true a wa) (map (Optional false a) w)) (map duplicate (duplicate wa))
= map (\w -> Optional false (Optional true a wa) (map (Optional false a) (duplicate w))) (duplicate wa)
= map (\w -> duplicate (Optional false a w)) (duplicate wa)
= map duplicate (map (Optional false a) (duplicate wa))