Mainline Profunctor Heirarchy for Optics

> {-# LANGUAGE RankNTypes, ScopedTypeVariables, TupleSections #-}
> module ProfunctorOptics where
> 
> import Control.Applicative
> import Control.Arrow ((&&&), (+++))
> import Data.Foldable
> import Data.Traversable
> import Data.Monoid

At the bottom of the optical hierarchy rests the humble Semantic Editor Combinator (SEC) also known as a Setter, which denotes an isomorphism between sₓ and F(aₓ) for some Functor F. The types s and a are possibly parametrized which we indicate by a subscript x. The rest of the mainline optical hierarchy consists of various refinements of the class of functors being quantified over.

For lenses and prisms the functors are of the form (c₁×) and (c₀+) respectively for some residual type. At the top of the hierarchy we have ‘Iso’, where we are quantifying over only the Identity functor, so the existential appears to disappear. All these classes of functors are closed under composition, though I am not sure how important this fact is.

To build profunctor implementations of these optics, we add additional methods that allow profunctors to be lifted through these various classes of functors

> class Profunctor p where
>   dimap :: (a -> b) -> (c -> d) -> p b c -> p a d

> class Profunctor p => Strong p where
>   first :: p a b -> p (a, c) (b, c)
>   second :: p a b -> p (c, a) (c, b)
>   second = dimap swap swap . first
>    where
>     swap (a,b) = (b,a)

> class Profunctor p => Choice p where
>   left :: p a b -> p (Either a c) (Either b c)
>   right :: p a b -> p (Either c a) (Either c b)
>   right = dimap switch switch . left
>    where
>     switch (Left x) = Right x
>     switch (Right y) = Left y

> class (Choice p, Strong p) => Step p where
>   step ::  p a b -> p (Either c (a,d)) (Either c (b,d))
>   step = right . first

> class Step p => Walk p where
>   walk :: Traversable f => p a b -> p (f a) (f b)

> class Walk p => Settable p where
>   mapping :: Functor f => p a b -> p (f a) (f b)

The profunctor implementation of the optical hierarchy quantifies over these various extensions of profunctors

> type Optic p s t a b = p a b -> p s t

> type Iso s t a b = forall p. Profunctor p => Optic p s t a b
> type Lens s t a b = forall p. Strong p => Optic p s t a b
> type Prism s t a b = forall p. Choice p => Optic p s t a b
> type AffineTraversal s t a b = forall p. Step p => Optic p s t a b
> type Traversal s t a b = forall p. Walk p => Optic p s t a b
> type SEC s t a b = forall p. Settable p => Optic p s t a b

Now we want to show that these optics actually correspond to their canonical definitions. The functions below are all isomorphisms, but I will only give the hard directions for now.

> iso :: forall s t a b. (s -> a) -> (b -> t) -> Iso s t a b
> iso = dimap

> lens :: forall s t a b. (s -> a) -> (s -> b -> t) -> Lens s t a b
> lens f g = dimap (f &&& id) (uncurry $ flip g) . first

> prism :: forall s t a b. (s -> Either t a) -> (b -> t) -> Prism s t a b
> prism f g = dimap f (either id g) . right

> affineTraversal :: forall s t a b. (s -> Either t a) -> (s -> b -> t) -> AffineTraversal s t a b
> affineTraversal f g = dimap from (either id (uncurry $ flip g)) . right . first
>  where
>   from :: s -> Either t (a,s)
>   from s = (id +++ (,s)) (f s)

> traversal :: forall s t a b. (forall f. Applicative f => (a -> f b) -> s -> f t) -> Traversal s t a b
> traversal f = dimap (Rotate . from) (to . unrotate) . walk
>  where
>   from :: s -> PKStore a b t
>   from = f (Battery (Unit id))
>   to :: PKStore b b t -> t
>   to = extract

> sec :: forall s t a b. ((a -> b) -> s -> t) -> SEC s t a b
> sec f = dimap from to . mapping
>  where
>   from :: s -> PStore s a a
>   from = PStore id
>   to :: PStore s a b -> t
>   to (PStore g s) = f g s

The sec solution places the argument f on the to side, while the traversal places the argument f on the from side. I suspect there is lots of wiggle room to slide f from one side to the other side. I also suspect that there are much more elegant solutions to traversal and sec, possibly using different characterizations of the Walk and Settable classes.

This just leaves Views and Reviews, which are created my making one of the two variables of a profunctor into a phantom variable.

> class Strong p => PhantomR p where
>   contrarmap :: (b -> a) -> p c a -> p c b
>   coerceRight :: p c a -> p c b
>   coerceRight = dimap id absurd . contrarmap absurd
>
> firstDefault :: PhantomR p => p a b -> p (a,c) (b,c)
> firstDefault = coerceRight . dimap fst id

> class Choice p => PhantomL p where
>   colmap :: (a -> b) -> p a c -> p b c
>   coerceLeft :: p a c -> p b c
>   coerceLeft = colmap absurd . dimap absurd id
>
> leftDefault :: PhantomL p => p a b -> p (Either a c) (Either b c)
> leftDefault = coerceLeft . dimap id Left

> type View s t a b = forall p. PhantomR p => Optic p s t a b
> type Review s t a b = forall p. PhantomL p => Optic p s t a b

> view :: forall s t a b. (s -> a) -> View s t a b
> view f = coerceRight . dimap f id

> review :: forall s t a b. (b -> t) -> Review s t a b
> review f = coerceLeft . dimap id f

This file is effectively a copy of part of bennofs's profunctor lenses library. He is the one who figured out how to implement 'sec', which I had no idea how to do and thought was impossible. His library is more extensive and is in turn based on his many discussions on the #haskell-lens channel on freenode. Once he demonstrated to me that sec was in fact possible, I felt that travesal must be possible. The trick was noticing that PKStore i j a is applicative in its third argument and traversable in its first argument. This lets us use the PKStore functor in both contexts.

Edward Kmett hinted to me that all this is known and has been derived many times (but nobody told me). Readers should work under the assumption that everything presented here is not novel and I am simply writing this down for me so that when I do build a profunctor based optics library in the future, I can reference it.

Nothing in this post is tested, none of the laws for the classes have been presented, and I have no proofs that anything is correct. All I know is that it all typechecks, so it is probably close to correct.

> newtype Void = Void Void
>
> absurd :: Void -> a
> absurd (Void x) = absurd x
>
> data PStore i j x = PStore (j -> x) i
>
> instance Functor (PStore i j) where
>   fmap f (PStore g i) = PStore (f . g) i

A PKStore is really the free applicative functor generated by PStore.

> data PKStore i j x = Unit x
>                    | Battery (PKStore i j (j -> x)) i
>
> instance Functor (PKStore i j) where
>   fmap f (Unit x) = Unit (f x)
>   fmap f (Battery g i) = Battery (fmap (f .) g) i
>
> instance Applicative (PKStore i j) where
>   pure = Unit
>   Unit x <*> c = fmap x c
>   Battery g i <*> c = Battery (flip <$> g <*> c) i
>
> newtype RotatePKStore j x i = Rotate { unrotate :: PKStore i j x }
>
> instance Functor (RotatePKStore j x) where
>   fmap f (Rotate (Unit x)) = Rotate (Unit x)
>   fmap f (Rotate (Battery g i)) = Rotate (Battery (unrotate (fmap f (Rotate g))) (f i))
>
> -- I am not 100% certain that the Foldable and Traversable instances are not reversed.
> instance Foldable (RotatePKStore j x) where
>   foldMap f (Rotate (Unit x)) = mempty
>   foldMap f (Rotate (Battery g i)) = f i <> foldMap f (Rotate g)
>
> instance Traversable (RotatePKStore j x) where
>   traverse f (Rotate (Unit x)) = pure (Rotate (Unit x))
>   traverse f (Rotate (Battery g i)) =  Rotate <$> (f i <**> (Battery . unrotate <$> traverse f (Rotate g)))
>
> extract :: PKStore i i x -> x
> extract (Unit x) = x
> extract (Battery g i) = extract g i