Indexed Optics as in section 2 of https://arxiv.org/pdf/2112.11145

IndexedOptic.hs

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
module IndexedOptic where

import Data.Kind (Type)

type f ~> g = forall i. f i -> g i

-- The indexed optic
data Ex (act :: (i -> j -> Type) -> (j -> Type) -> i -> Type) (s :: i -> Type) (t :: i -> Type) (a :: j -> Type) (b :: j -> Type) where
  Ex :: (s ~> act m a) -> (act m b ~> t) -> Ex act s t a b

-- Example actions
data Tup m a i where
  Tup :: m i j -> a j -> Tup m a i

data Sum m i a where
  Sum :: Either (m i j) (a j) -> Sum m a i

type ExLens s t a b = Ex Tup s t a b
type ExLens' s a = ExLens s s a a
type ExPrism s t a b = Ex Sum s t a b
type ExPrism' s a = ExPrism s s a a

-- Dependent lenses as natural transformation between polynomial functors
data Poly (s :: i -> Type) (t :: i -> Type) y where
  P :: s i -> (t i -> y) -> Poly s t y

type DLens s t a b = Poly s t ~> Poly a b
type DLens' s a = DLens s s a a

-- Conversion between dependent lenses and indexed optics
data M b t i j where
  M :: (b j -> t i) -> M b t i j

d2e :: DLens s t a b -> ExLens s t a b
d2e l = Ex (\s -> case l (P s id) of P a bt -> Tup (M bt) a) (\(Tup (M bt) b) -> bt b)

e2d :: ExLens s t a b -> DLens s t a b
e2d (Ex sa bt) (P s ty) = case sa s of Tup m a -> P a (\b -> ty (bt (Tup m b)))


-- tests

data EitherI l r i where
  L :: l -> EitherI l r 'False
  R :: r -> EitherI l r 'True

edl :: DLens' (EitherI (s, l) r) (EitherI l r)
edl (P (L (s, l)) f) = P (L l) (\(L l') -> f (L (s, l')))
edl (P (R r) f) = P (R r) (\(R r') -> f (R r'))

data Same m i j where
  Same :: m i -> Same m i i

eex :: ExLens' (EitherI (s, l) r) (EitherI l r)
eex = Ex f g
  where
    f :: EitherI (s, l) r ~> Tup (Same (EitherI s ())) (EitherI l r)
    f (L (s, l)) = Tup (Same (L s)) (L l)
    f (R r) = Tup (Same (R ())) (R r)
    g :: Tup (Same (EitherI s ())) (EitherI l r) ~> EitherI (s, l) r
    g (Tup (Same (L s)) (L l)) = L (s, l)
    g (Tup (Same (R ())) (R r)) = R r