diff --git a/Data/Profunctor/Traversing.idr b/Data/Profunctor/Traversing.idr index 7e57de2..d52efb0 100644 --- a/Data/Profunctor/Traversing.idr +++ b/Data/Profunctor/Traversing.idr @@ -2,6 +2,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 @@ -9,6 +10,24 @@ import Data.Profunctor.Closed %default total + +[FoldablePair] Foldable (Pair c) where + foldr op init (_, x) = x `op` init + foldl op init (_, x) = init `op` x + null _ = False + +[TraversablePair] Traversable (Pair c) using FoldablePair where + traverse f (l, r) = (l,) <$> f r + +[FoldableIdentity] Foldable Identity where + foldr f i (Id x) = f x i + foldl f i (Id x) = f i x + null _ = False + +[TraversableIdentity] Traversable Identity using FoldableIdentity where + traverse f (Id x) = map Id (f x) + + record Bazaar a b t where constructor MkBazaar getBazaar : forall f. Applicative f => (a -> f b) -> f t @@ -52,3 +71,98 @@ interface (Strong p, Choice p) => Traversing p where wander : (forall f. Applicative f => (a -> f b) -> s -> f t) -> p a b -> p s t wander f = dimap (\s => MkBaz $ \afb => f afb s) sold . traverse' + + +-- CofreeTraversing + +public export +record CofreeTraversing p a b where + constructor MkCFT + getCFT : forall f. Traversable f => p (f a) (f b) + +export +Profunctor p => Profunctor (CofreeTraversing p) where + lmap f (MkCFT p) = MkCFT (lmap (map f) p) + rmap g (MkCFT p) = MkCFT (rmap (map g) p) + dimap f g (MkCFT p) = MkCFT (dimap (map f) (map g) p) + +export +Profunctor p => GenStrong Pair (CofreeTraversing p) where + strongr (MkCFT p) = MkCFT (p @{Compose @{%search} @{TraversablePair}}) + strongl = dimap Builtin.swap Builtin.swap . strongr {p=CofreeTraversing p} + +export +Profunctor p => GenStrong Either (CofreeTraversing p) where + strongr (MkCFT p) = MkCFT (p @{Compose {f=Either c}}) + strongl = dimap swap swap . strongr {p=CofreeTraversing p} + +export +Profunctor p => Traversing (CofreeTraversing p) where + traverse' (MkCFT p) = MkCFT (p @{Compose}) + +export +ProfunctorFunctor CofreeTraversing where + promap f (MkCFT p) = MkCFT (f p) + +export +ProfunctorComonad CofreeTraversing where + proextract (MkCFT p) = dimap Id runIdentity $ p @{TraversableIdentity} + produplicate (MkCFT p) = MkCFT $ MkCFT $ p @{Compose} + +export +Profunctor p => Functor (CofreeTraversing p a) where + map = rmap + + +export +cofreeTraversing : Traversing p => p :-> q -> p :-> CofreeTraversing q +cofreeTraversing f p = MkCFT $ f $ traverse' p + +export +uncofreeTraversing : Profunctor q => p :-> CofreeTraversing q -> p :-> q +uncofreeTraversing f p = proextract $ f p + + +-- FreeTraversing + +public export +data FreeTraversing : (p : Type -> Type -> Type) -> Type -> Type -> Type where + MkFT : Traversable f => (f y -> b) -> p x y -> (a -> f x) -> FreeTraversing p a b + +export +Profunctor (FreeTraversing p) where + lmap f (MkFT l m r) = MkFT l m (r . f) + rmap f (MkFT l m r) = MkFT (f . l) m r + dimap f g (MkFT l m r) = MkFT (g . l) m (r . f) + +export +GenStrong Pair (FreeTraversing p) where + strongr (MkFT l m r) = MkFT @{Compose @{TraversablePair}} (map l) m (map r) + strongl = dimap Builtin.swap Builtin.swap . strongr {p=FreeTraversing p} + +export +GenStrong Either (FreeTraversing p) where + strongr (MkFT l m r) = MkFT @{Compose {t=Either c}} (map l) m (map r) + strongl = dimap swap swap . strongr {p=FreeTraversing p} + +export +Traversing (FreeTraversing p) where + traverse' (MkFT l m r) = MkFT @{Compose} (map l) m (map r) + +export +ProfunctorFunctor FreeTraversing where + promap f (MkFT l m r) = MkFT l (f m) r + +export +ProfunctorMonad FreeTraversing where + propure p = MkFT @{TraversableIdentity} runIdentity p Id + projoin (MkFT l' (MkFT l m r) r') = MkFT @{Compose} (l' . map l) m (map r . r') + + +export +freeTraversing : Traversing q => p :-> q -> FreeTraversing p :-> q +freeTraversing fn (MkFT {f} l m r) = dimap r l (traverse' {f} (fn m)) + +export +unfreeTraversing : FreeTraversing p :-> q -> p :-> q +unfreeTraversing f p = f (MkFT @{TraversableIdentity} runIdentity p Id)