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 match1. 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.
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 tTo 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 tA 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 fmapTo 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 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 bimap 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 tUsing 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 imapHere, 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)) sAs 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.
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 bIt 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 bWe’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 : ysWith "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 tUsing 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 jtraverseTo 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 zInterestingly, 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_aSimilarly 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 example88bThe "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.
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.
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.↩︎