Profunctor optics, a categorical update - Bryce Clarke, Derek Elkins, Jeremy Gibbons, Fosco Loregian, Bartosz Milewski, Emily Pillmore, Mario Román

ProfunctorOpticsCategoricalUpdate.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

{-
copied from: 7.1 and 7.2 
Profunctor optics, a categorical update
Bryce Clarke, Derek Elkins, Jeremy Gibbons, Fosco Loregian, Bartosz Milewski, Emily Pillmore, Mario Román

updated using:
https://github.com/mroman42/vitrea/blob/master/Categories.hs
https://github.com/mroman42/vitrea/blob/master/Tambara.hs
and suggestions from @topos 
-}

class Category objc c where
  unit :: (objc x) => c x x
  comp :: (objc x) => c y z -> c x y -> c x z

class ( Category objc c, Category objd d
      , forall x . objc x => objd (f x)
      ) => VFunctor objc c objd d f where
  map :: (objc x, objc y) => c x y -> d (f x) (f y)

class ( Category objc c, Category objd d, Category obje e
      , forall x y . (objc x , objd y) => obje (f x y) )
      => Bifunctor objc c objd d obje e f where
  bimap :: ( objc x1, objc x2, objd y1, objd y2 )
       => c x1 x2 -> d y1 y2 -> e (f x1 y1) (f x2 y2)

class ( Category objc c, Category objd d )
       => Profunctor objc c objd d p where
   dimap :: (objc x1, objc x2, objd y1, objd y2)
        => c x2 x1 -> d y1 y2 -> p x1 y1 -> p x2 y2

class ( Category obja a
      , Bifunctor obja a obja a obja a o
      , obja i )
   => MonoidalCategory obja a o i where
 alpha :: (obja x, obja y, obja z)
    => a (x `o` (y `o` z)) ((x `o` y) `o` z)
 alphainv :: (obja x, obja y, obja z)
    => a ((x `o` y) `o` z) (x `o` (y `o` z))
 lambda    :: (obja x) => a (x `o` i) x
 lambdainv :: (obja x) => a x (x `o` i)
 rho       :: (obja x) => a (i `o` x) x
 rhoinv    :: (obja x) => a x (i `o` x)

class ( MonoidalCategory objm m o i
      , Bifunctor objm m objc c objc c f
      , Category objc c )
      => MonoidalAction objm m o i objc c f where
  unitor           :: (objc x) => c (f i x) x
  unitorinv        :: (objc x) => c x (f i x)
  multiplicator    :: (objc x, objm p, objm q)
                             => c (f p (f q x)) (f (p `o` q) x)
  multiplicatorinv :: (objc x, objm p, objm q)
                             => c (f (p `o` q) x) (f p (f q x))

data Optic objc c objd d objm m o i f g a b s t where
  Optic :: ( MonoidalAction objm m o i objc c f
           , MonoidalAction objm m o i objd d g
           , objc a, objc s , objd b, objd t, objm x )
      => c s (f x a) -> d (g x b) t
      -> Optic objc c objd d objm m o i f g a b s t

class ( MonoidalAction objm m o i objc c f
      , MonoidalAction objm m o i objd d g
      , Profunctor objc c objd d p )
      => Tambara objc c objd d objm m o i f g p where
  tambara :: (objc x, objd y, objm w)
          => p x y -> p (f w x) (g w y)

type ProfOptic   objc c objd d objm m o i f g a b s t = forall p .
       ( Tambara objc c objd d objm m o i f g p
       , MonoidalAction objm m o i objc c f
       , MonoidalAction objm m o i objd d g
       , objc a, objd b, objc s, objd t
       ) => p a b -> p s t

instance ( MonoidalAction objm m o i objc c f
         , MonoidalAction objm m o i objd d g
         , objc a, objd b)
         => Profunctor objc c objd d (Optic objc c objd d objm m o i f g a b) where
    dimap f g (Optic l r) = Optic (comp @objc @c l f) (comp @objd @d g r)

instance ( MonoidalAction objm m o i objc c f
         , MonoidalAction objm m o i objd d g
         , objc a, objd b)
         => Tambara objc c objd d objm m o i f g (Optic objc c objd d objm m o i f g a b) where
    tambara (Optic l r) = Optic
      (comp @objc @c (multiplicator @objm @m @o @i @objc @c @f) (bimap @objm @m @objc @c @objc @c (unit @objm @m) l))
      (comp @objd @d (bimap @objm @m @objd @d @objd @d (unit @objm @m) r) (multiplicatorinv @objm @m @o @i @objd @d @g))

ex2prof :: forall objc c objd d objm m o i f g a b s t .
      Optic       objc c objd d objm m o i f g a b s t
   -> ProfOptic   objc c objd d objm m o i f g a b s t
ex2prof (Optic l r) =
       dimap @objc @c @objd @d l r .
       tambara @objc @c @objd @d @objm @m @o @i

prof2ex :: forall objc c objd d objm m o i f g a b s t .
  ( MonoidalAction objm m o i objc c f
  , MonoidalAction objm m o i objd d g
  , objc a, objc s
  , objd b, objd t)
  => ProfOptic objc c objd d objm m o i f g a b s t
  -> Optic     objc c objd d objm m o i f g a b s t
prof2ex p = p (Optic
  (unitorinv @objm @m @o @i @objc @c @f)
  (unitor @objm @m @o @i @objd @d @g))