toki/idris2-profunctors
1
0
Fork 0
Code Issues Pull requests Activity

Implement Traversing profunctors

Browse source
This commit is contained in:
Kiana Sheibani 2023-03-06 19:24:07 -05:00
parent f68a0c517c
commit 013ceae011
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
1 changed files with 23 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
Data/Profunctor/Traversing.idr
View file

@ -3,10 +3,7 @@ module Data.Profunctor.Traversing
import Control.Monad.Identity
import Data.Morphisms
import Data.Tensor
import Data.Profunctor.Types
import Data.Profunctor.Functor
import Data.Profunctor.Strong
import Data.Profunctor.Closed
import Data.Profunctor
%default total
@ -73,6 +70,28 @@ interface (Strong p, Choice p) => Traversing p where
wander f = dimap (\s => MkBaz $ \afb => f afb s) sold . traverse'
export
Traversing Morphism where
traverse' (Mor f) = Mor (map f)
wander f (Mor p) = Mor (runIdentity . (f $ Id . p))
export
[Function] Traversing (\a,b => a -> b) using Strong.Function where
traverse' = map
wander f g = runIdentity . (f $ Id . g)
export
Applicative f => Traversing (Kleislimorphism f) where
traverse' (Kleisli p) = Kleisli (traverse p)
wander f (Kleisli p) = Kleisli (f p)
export
Applicative f => Traversing (Star f) where
traverse' (MkStar p) = MkStar (traverse p)
wander f (MkStar p) = MkStar (f p)
-- CofreeTraversing
public export