Oleg's gists — Archive

Coindexed optics

Posted on 2021-01-04 by Oleg Grenrus lens, optics

The term coindexed optics is sometimes brought up. But what are they? One interpretation is optics with error reporting, i.e. which can tell why e.g. Prism didn’t match¹. For some time I started to dislike that interpretation. It doesn’t feel right.

Recently I run into documentation of witherable. There is Wither, which is like a lens, but not quite. I think that is closer to what coindexed optics could be. (However, there are plenty arrows to flip, and you may flip others).

This blog post is a literate Haskell file, so we start with language extensions

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}

The import list is shorter, Data.SOP is the only module (from sop-core) which is not in base library.

import Control.Applicative (liftA2)
import Data.Kind           (Type)
import Data.Bifunctor      (Bifunctor (first))
import Data.Char           (toUpper)
import Data.Coerce         (coerce)
import Data.SOP            (NP (..), NS (..), I (..))

import qualified Data.Maybe as L (mapMaybe)

I will use a variant of profunctor encoding of optics. The plan is to show

ordinary, unindexed optics;
then indexed optics;
and finally coindexed optics.

#Ordinary, unindexed optics

The profunctor encoding of optics is relatively simple. However, instead of ordinary profunctors, we will use a variant with additional type level list argument. This is similar to indexed-profunctors, though there the type list is curried. Currying works well for indexed optics, but complicates coindexed story.

type Optic p (is :: [Type]) (js :: [Type]) s t a b = p is a b -> p js s t

To not make this post unnecessarily long, we will use only a subset of profunctor hierarchy: Profunctor and Mapping for now. Profunctor is used to encode isomorphisms (isos), and Mapping is used to encode setters.

class Profunctor (p :: [Type] -> Type -> Type -> Type) where
    dimap :: (a -> b) -> (c -> d) -> p is b c -> p is a d

class Profunctor p => Mapping p where
    roam :: ((a -> b) -> s -> t) -> p is a b -> p is s t

A go to example of a setter is mapped. With mapped we can set, or map over, elements in a Functor.

mapped :: (Mapping p, Functor f)
       => Optic p is is (f a) (f b) a b
mapped = roam fmap

To implement the over operation we need a concrete profunctor. If we used ordinary profunctors, the function arrow would do. In this setup we need a newtype to adjust the kind:

newtype FunArrow (is :: [Type]) a b =
    FunArrow { runFunArrow :: a  -> b }

Instance implementations are straight forward:

instance Profunctor FunArrow where
    dimap f g (FunArrow k) = FunArrow (g . k . f)

instance Mapping FunArrow where
    roam f (FunArrow k) = FunArrow (f k)

Using FunArrow we can implement over. over uses a setter to map over focused elements in a bigger structure. Note, we allow any index type-lists. We (or rather FunArrow) simply ignore them.

over :: Optic FunArrow is js s t a b
     -> (a -> b)
     -> (s -> t)
over o f = runFunArrow (o (FunArrow f))

Some examples, to show it works what we have written so far. over mapped is a complicated way to say fmap:

-- "FOOBAR"
example01 :: String
example01 = over mapped toUpper "foobar"

Optics compose. over (mapped . mapped) maps over two composed functors:

-- ["FOOBAR","XYZZY"]
example02 :: [String]
example02 = over (mapped . mapped) toUpper ["foobar", "xyzzy"]

This was a brief refresher of profunctor optics. It is "standard", except that we added an additional type-level list argument to the profunctors.

We will next use that type-level list to implement indexed optics.

#Indexed optics

Indexed optics let us set, map, traverse etc. using an additional index. The operation we want to generalize with optics is provided by few classes, like FunctorWithIndex:

class Functor f => FunctorWithIndex i f | f -> i where
    imap :: (i -> a -> b) -> f a -> f b

imap operation is sometimes called mapWithKey (for example in containers library).

Ordinary lists are indexed with integers. Map k v is indexed with k. We will use lists in the examples, so let us define an instance:

instance FunctorWithIndex Int [] where
    imap f = zipWith f [0..]

Next, we need to make that available in optics framework. New functionality means new profunctor type class. Note how an indexed combinator conses the index to the list.

class Mapping p => IMapping p where
    iroam :: ((i -> a -> b) -> s -> t) -> p (i ': is) a b -> p is s t

Using iroam and imap we can define imapped, which is an example of indexed setter.

imapped :: (FunctorWithIndex i f, IMapping p)
        => p (i ': is) a b -> p is (f a) (f b)
imapped = iroam imap

Here, we should note that FunArrow can be given an instance of IMapping. We simply ignore the index argument.

instance IMapping FunArrow where
    iroam f (FunArrow k) = FunArrow (f (\_ -> k))

That allows us to use imapped instead of mapped. (both optics and lens libraries have tricks to make that efficient).

-- ["FOOBAR","XYZZY"]
example03 :: [String]
example03 = over (mapped . imapped) toUpper ["foobar", "xyzzy"]

To actually use indices, we need new concrete profunctor. The IxFunArrow takes a heterogeneous list, NP I (n-ary product), of indices in addition to the element as an argument of an arrow.

newtype IxFunArrow is a b =
    IxFunArrow { runIxFunArrow :: (NP I is, a) -> b }

The IxFunArrow instances are similar to FunArrow ones, they involve just a bit of additional plumbing.

instance Profunctor IxFunArrow where
    dimap f g (IxFunArrow k) = IxFunArrow (g . k . fmap f)

instance Mapping IxFunArrow where
    roam f (IxFunArrow k) = IxFunArrow (\(is, s) -> f (\a -> k (is, a)) s)

IMapping instance is the most interesting. As the argument provides an additional index i, it is consed to the the list of existing indices.

instance IMapping IxFunArrow where
    iroam f (IxFunArrow k) = IxFunArrow $
        \(is, s) -> f (\i a -> k (I i :* is, a)) s

As I already mentioned, indexed-profunctors uses curried variant, so the index list is implicitly encoded in uncurried form i1 -> i2 -> .... That is clever, but hides the point.

Next, the indexed over. The general variant takes an optic with any indices list.

gen_iover :: Optic IxFunArrow is '[] s t a b
         -> ((NP I is, a) -> b)
         -> s -> t
gen_iover o f s = runIxFunArrow (o (IxFunArrow f)) (Nil, s)

Usually we use the single-index variant, iover:

iover :: Optic IxFunArrow '[i] '[] s t a b
      -> (i -> a -> b)
      -> s -> t
iover o f = gen_iover o (\(I i :* Nil, a) -> f i a)

We can also define the double-index variant, iover2 (and so on).

iover2 :: Optic IxFunArrow '[i,j] '[] s t a b
       -> (i -> j -> a -> b)
       -> (s -> t)
iover2 o f = gen_iover o (\(I i :* I j :* Nil, a) -> f i j a)

Lets see what we can do with indexed setters. For example we can upper case every odd character in the string:

-- "fOoBaR"
example04 :: String
example04 = iover imapped (\i a -> if odd i then toUpper a else a) "foobar"

In nested case, we have access to all indices:

-- ["fOoBaR","XyZzY","uNoRdErEd-cOnTaInErS"]
example05 :: [String]
example05 = iover2
    (imapped . imapped)
    (\i j a -> if odd (i + j) then toUpper a else a)
    ["foobar", "xyzzy", "unordered-containers"]

We don’t need to index at each step, e.g. we can index only at the top level:

-- ["foobar","XYZZY","unordered-containers"]
example06 :: [String]
example06 = iover
    (imapped . mapped)
    (\i a -> if odd i then toUpper a else a)
    ["foobar", "xyzzy", "unordered-containers"]

Indexed optics are occasionally very useful. We can provide extra information in indices, which would otherwise not fit into optical frameworks.

#Coindexes

The indexed optics from previous sections can be flipped to be coindexed ones. As I mentioned in the introduction, I got an idea at looking at witherable. package.

witherable provides (among many things) a useful type-class, in a simplified form:

class Functor f => Filterable f where
    mapMaybe :: (a -> Maybe b) -> f a -> f b

It is however too simple. (Hah!). The connection to indexed optics is easier to see using an Either variant:

class Functor f => FunctorWithCoindex j f | f -> j where
    jmap :: (a -> Either j b) -> f a -> f b

We’ll also need a Traversable variant (Witherable in witherable):

class (Traversable f, FunctorWithCoindex j f)
    => TraversableWithCoindex j f | f -> j
  where
    jtraverse :: Applicative m => (a -> m (Either j b)) -> f a -> m (f b)

Instances for list are not complicated. The coindex of list is a unit ().

instance FunctorWithCoindex () [] where
    jmap f = L.mapMaybe (either (const Nothing) Just . f)

instance TraversableWithCoindex () [] where
    jtraverse _ [] = pure []
    jtraverse f (x:xs) = liftA2 g (f x) (jtraverse f xs) where
        g (Left ()) ys = ys
        g (Right y) ys = y : ys

With "boring" coindex, like the unit, we can recover mapMaybe:

mapMaybe' :: FunctorWithCoindex () f => (a -> Maybe b) -> f a -> f b
mapMaybe' f = jmap (maybe (Left ()) Right . f)

With TraversableWithCoindex class, doing the same tricks as previously with indexed optics, we get coindexed optics. Easy.

I didn’t manage to get JMapping (a coindexed mapping) to work, so I’ll use JTraversing. We abuse the index list for coindices.

class Profunctor p => Traversing p where
    wander :: (forall f. Applicative f => (a -> f b) -> s -> f t)
           -> p js a b -> p js s t

class Traversing p => JTraversing p where
    jwander
        :: (forall f. Applicative f => (a -> f (Either j b)) -> s -> f t)
        -> p (j : js) a b -> p js s t

Using JTraversing we can define our first coindexed optic.

traversed :: (Traversable f, Traversing p) => p js a b -> p js (f a) (f b)
traversed = wander traverse

jtraversed :: (TraversableWithCoindex j f, JTraversing p)
           => p (j : js) a b -> p js (f a) (f b)
jtraversed = jwander jtraverse

To make use of it we once again need a concrete profunctor.

newtype CoixFunArrow js a b = CoixFunArrow
    { runCoixFunArrow :: a -> Either (NS I js) b }

instance Profunctor CoixFunArrow where
    dimap f g (CoixFunArrow p) = CoixFunArrow (fmap g . p . f)

instance Traversing CoixFunArrow where
    wander f (CoixFunArrow p) = CoixFunArrow $ f p

instance JTraversing CoixFunArrow where
    jwander f (CoixFunArrow p) = CoixFunArrow $ f (plumb . p) where
        plumb :: Either (NS I (j : js)) b -> Either (NS I js) (Either j b)
        plumb (Right x)        = Right (Right x)
        plumb (Left (Z (I y))) = Right (Left y)
        plumb (Left (S z))     = Left z

Interestingly, Traversing CoixFunArrow instance looks like Mapping FunArrow, and it seems to be impossible to write Mapping IxFunArrow.

Anyway, next we define a coindexed over, which I unimaginatively call jover. Like in the previous section, I start with a generic version first.

gen_jover
    :: Optic CoixFunArrow is '[] s t a b
    -> (a -> Either (NS I is) b) -> s -> t
gen_jover o f s = either nsAbsurd id
                $ runCoixFunArrow (o (CoixFunArrow f)) s

jover
    :: Optic CoixFunArrow '[i] '[] s t a b
    -> (a -> Either i b) -> s -> t
jover o f = gen_jover o (first (Z . I) . f)

jover2
    :: Optic CoixFunArrow '[i,j] '[] s t a b
    -> (a -> Either (Either i j) b)
    -> s -> t
jover2 o f = gen_jover o (first plumb . f) where
    plumb (Left i)  = Z (I i)
    plumb (Right j) = S (Z (I j))

And now the most fun: the coindexed optics examples. First we can recover the mapMaybe behavior:

-- ["foobar"]
example07 :: [String]
example07 = jover jtraversed
    (\s -> if length s > 5 then Right s else Left ())
    ["foobar", "xyzzy"]

And because we have separate coindexes in the type level list, we can filter on the different levels of the structure! If we find a character 'y', we skip the whole word, otherwise we skip all vowels.

-- ["fbr","nrdrd-cntnrs"]
example08 :: [String]
example08 = jover2 (jtraversed . jtraversed)
    predicate
    ["foobar", "xyzzy", "unordered-containers"]
  where
    predicate 'y'           = Left (Right ())  -- skip word
    predicate c | isVowel c = Left (Left ())   -- skip character
    predicate c             = Right c

isVowel :: Char -> Bool
isVowel c = elem c ['a','o','u','i','e']

Note, the coindex doesn’t need to mean filtering. For example, consider the following type:

newtype JList j a = JList { unJList :: [Either j a] }
  deriving (Functor, Foldable, Traversable, Show)

It’s not Filterable, but it can write a FunctorWithCoindex instance:

instance FunctorWithCoindex j (JList j) where
    jmap f (JList xs) = JList (map (>>= f) xs) where

instance TraversableWithCoindex j (JList j) where
    jtraverse f (JList xs) = fmap JList (go xs) where
        go []             = pure []
        go (Left j : ys)  = fmap (Left j :) (go ys)
        go (Right x : ys) = liftA2 (:) (f x) (go ys)

Using JList we can do different things. In this example, we return why elements didn’t match, but that information is returned embedded inside the structure itself. We "filter" long strings:

jlist :: [a] -> JList j a
jlist = JList . map Right

ex_jlist_a :: JList Int String
ex_jlist_a = jlist ["foobar", "xyzzy", "unordered-containers"]

-- JList {unJList = [Left 6,Right "xyzzy",Left 20]}
example09 :: JList Int String
example09 = jover jtraversed
    (\s -> let l = length s in if l > 5 then Left l else Right s)
    ex_jlist_a

Similarly we can filter, or rather "change structure", on different levels, and these levels can have different coindices:

ex_jlist_b :: JList Int (JList Bool Char)
ex_jlist_b = fmap jlist ex_jlist_a

example88b :: JList Int (JList Bool Char)
example88b = jover2
    (jtraversed . jtraversed)
    predicate
    ex_jlist_b
  where
    predicate 'x'           = Left (Right 0)
    predicate 'y'           = Left (Right 1)
    predicate 'z'           = Left (Right 2)
    predicate c | isVowel c = Left (Left (c == 'o'))
    predicate c             = Right c

{-
[ Right [Right 'f',Left True,Left True,Right 'b',Left False,Right 'r']
, Left 0
, Right [Left False,Right 'n',Left True,Right 'r',Right 'd',Left False, ...
]
-}
example88b' :: [Either Int [Either Bool Char]]
example88b' = coerce example88b

The "xyzzy" is filtered immediately, we see Left 0 as a reason. We can also see how vowels are filtered, and 'o' are marked specifically with Left True.

Having coindices reside inside the structure makes composition just work. That what makes this different from "error reporting optics". And using coindices approach we can compose filters, the Wither from witherable doesn’t seem to compose with itself.

#Both

Obvious follow up question is whether we can have both indices and coindices. Why not, the concrete profunctor would look like:

newtype DuplexFunArrow is js a b = DuplexFunArrow
    { runDuplexFunArrow :: (NP I is, a) -> Either (NS I js) b }

Intuitively, the structure traversals would provide additional information in indices, and we’ll be able to alter it by optionally returning coindices.

Would that be useful? I have no idea.

#Utilities

nsAbsurd :: NS I '[] -> a
nsAbsurd x = case x of {}

https://blog.fp-tower.com/2020-01-27-introducing-error-reporting-in-optics/ looks like an example of that. In Scala.↩︎

2024-04-21 – A note about coercions
2024-04-18 – What makes a good compiler warning?
2024-04-12 – Core Inspection
2024-04-01 – Implicit arguments
2024-03-17 – ST with an early exit

This work is licensed under a “CC BY SA 4.0” license.

Oleg's gists — Archive

twitter github email linkedin stackoverflow

Site proudly generated by Hakyll