Profunctor lenses in Idris 2

Lens.idr

module Lens

-- Concrete get/set lens
record Lens s t a b where
  constructor MkLens 
  get : s -> a
  set : s -> b -> t

unitLens : Lens a b a b 
unitLens = MkLens id (\x => id)

-- Example of a lens that focuses on the first component of Prod
data  Prod a b = Pr a b

(Show a, Show b) => Show (Prod a b) where
  show (Pr a b) = "(" ++ show a ++ ", " ++ show b ++ ")"

get0 : Prod a b -> a
get0 (Pr a b) = a

set0 : Prod a b -> c -> Prod c b
set0 (Pr a b) c = Pr c b

lens0 : Lens (Prod a b) (Prod a' b) a a'
lens0 = MkLens get0 set0

-- Existential lens with residue c
record ExLens {0 c : Type} s t a b where
  constructor MkExLens
  decomp : s -> (a, c)
  recomp : (b, c) -> t

-- Example
dec : Prod a b -> (a, b) -- b is the residue c
dec (Pr a b) = (a, b)

rec   : (a, b) -> Prod a b
rec (a, b) = Pr a b

exLens : ExLens {c = b} (Prod a b) (Prod a' b) a a'
exLens = MkExLens dec rec

interface Profunctor (0 p : Type -> Type -> Type) where
  dimap : (a' -> a) -> (b -> b') -> p a b -> p a' b'

interface Profunctor p => Strong (0 p : Type -> Type -> Type) where
  first : {0 c : Type} -> p a b -> p (a, c) (b, c)

-- Profunctor lens
-- Note: p is erased through universal quantification,
-- so it cannto be applied to a b or s t, unless LensP is itself erased
0 LensP : Type -> Type -> Type -> Type -> Type
LensP s t a b =  {0 p : Type -> Type -> Type} -> (Strong p => p a b -> p s t)

-- Example of a strong profunctor

data Hom : Type -> Type -> Type where
  H : (a -> b) -> Hom a b

Profunctor Hom where
  dimap f g (H h) = H (g . h . f)

Strong Hom where
  -- (a -> b) -> (a, c) -> (b, c)
  first {c} (H f) = H (\(a, c) => (f a, c))

-- Inverted concrete lens (swaps parameter pairs)
data InvLens : (a: Type) -> (b :Type) -> (s : Type) -> (t : Type) -> Type where
  MkInvLens : Lens s t a b -> InvLens a b s t

-- A Lens is a Strong profunctor in the arguments s and t

{a : Type} -> {b : Type} -> Profunctor (InvLens a b) where
  -- (s' -> s) -> (t -> t') -> (s -> a, s -> b -> t) -> (s' -> a, s' -> b -> t')
  dimap f g (MkInvLens lens) = MkInvLens $ 
    MkLens (lens.get . f) (\s' => g . lens.set (f s'))

{a : Type} -> {b : Type} -> Strong (InvLens a b) where
  -- ((s, c) -> a,  (s, c) -> b -> (t, c))
  first {c} (MkInvLens lens) = MkInvLens $ 
    MkLens (\(s, c) => lens.get s) (\(s, c) => (\b => (lens.set s b, c)))

-- Profunctor lens from get/set
getSetToP : (s -> a) -> (s -> b -> t) -> LensP s t a b
getSetToP get set pab =
  let p' = first {c = s} pab
  in dimap (\s => (get s, s)) (\(b, s) => set s b) p'

-- get/set from profunctor lens
fromPtoGetSet : {a, b, s, t : Type} -> LensP s t a b -> Lens s t a b
fromPtoGetSet plens = 
  let il0 : InvLens a b a b = MkInvLens unitLens
      il1 : InvLens a b s t  = plens il0
      (MkInvLens ls) = il1
  in ls

toGet2 : {a, s : Type} -> {b, t : Type} -> LensP s t a b -> s -> a
toGet2 = get . fromPtoGetSet

toSet2 : {a, b, s, t : Type} -> LensP s t a b -> s -> b -> t
toSet2 = set . fromPtoGetSet

-- Example 
lensP : LensP (Prod a c) (Prod a' c) a a'
lensP = getSetToP get0 set0

s1 : Prod (Prod Char Int) String
s1 = Pr (Pr 'a' 1) "one"

-- lensP : LensP (Prod a c) (Prod a' c) a a'
-- fromPtoGetSet : LensP s t a b -> Lens s t a b
z : {a, a', c : Type} -> Lens (Prod a c) (Prod a' c) a a'
z = fromPtoGetSet lensP

-- lensP : LensP (Prod a c) (Prod a' c) a a'

bilens : {x : Type} -> LensP (Prod (Prod Char Int) String) (Prod (Prod x Int) String) Char x
bilens = lensP . lensP

main : IO ()
main = do 
  putStrLn "get using lens composition"
  print $ (toGet2 {b=()} bilens) s1
  putStrLn "set using lens composition"
  print $ (toSet2 bilens) s1 True