diff --git a/Data/Profunctor/Mapping.idr b/Data/Profunctor/Mapping.idr index f00bb9a..262dd09 100644 --- a/Data/Profunctor/Mapping.idr +++ b/Data/Profunctor/Mapping.idr @@ -1,6 +1,5 @@ module Data.Profunctor.Mapping -import Control.Monad.Identity import Data.Morphisms import Data.Tensor import Data.Profunctor @@ -23,7 +22,7 @@ functor = MkFunctor (\f => (. (. f))) ||| * `map' . lmap f = lmap (map f) . map'` ||| * `map' . rmap f = rmap (map f) . map'` ||| * `map' . map' = map' @{Compose}` -||| * `dimap Identity runIdentity . map' = id` +||| * `dimap Id runIdentity . map' = id` public export interface (Traversing p, Closed p) => Mapping p where map' : Functor f => p a b -> p (f a) (f b) @@ -80,7 +79,7 @@ ProfunctorFunctor CofreeMapping where public export ProfunctorComonad CofreeMapping where - proextract (MkCFM p) = dimap Id runIdentity p + proextract (MkCFM p) = p @{FunctorId} produplicate (MkCFM p) = MkCFM $ MkCFM $ p @{Compose} public export @@ -99,7 +98,7 @@ roamCofree f (MkCFM p) = MkCFM $ dimap (map (flip f)) (map ($ id)) $ public export Profunctor p => Traversing (CofreeMapping p) where traverse' (MkCFM p) = MkCFM (p @{Compose}) - wander f = roamCofree $ f @{MkApplicative @{MkFunctor id} id id} + wander f = roamCofree $ f @{ApplicativeId} public export Profunctor p => Mapping (CofreeMapping p) where @@ -128,7 +127,7 @@ ProfunctorFunctor FreeMapping where public export ProfunctorMonad FreeMapping where - propure p = MkFM runIdentity p Id + propure p = MkFM @{FunctorId} id p id projoin (MkFM l' (MkFM l m r) r') = MkFM @{Compose} (l' . map l) m (map r . r') public export @@ -155,7 +154,7 @@ roamFree f (MkFM l m r) = MkFM @{Compose @{functor}} (($ id) . map @{functor} l) public export Traversing (FreeMapping p) where traverse' (MkFM l m r) = MkFM @{Compose} (map l) m (map r) - wander f = roamFree $ f @{MkApplicative @{MkFunctor id} id id} + wander f = roamFree $ f @{ApplicativeId} public export Mapping (FreeMapping p) where diff --git a/Data/Profunctor/Representable.idr b/Data/Profunctor/Representable.idr index 383cde5..1255c58 100644 --- a/Data/Profunctor/Representable.idr +++ b/Data/Profunctor/Representable.idr @@ -50,9 +50,9 @@ Representable Morphism Identity where ||| A named implementation of `Representable` for function types. ||| Use this to avoid having to use a type wrapper like `Morphism`. export -[Function] Representable (\a,b => a -> b) Identity +[Function] Representable (\a,b => a -> b) Prelude.id using Sieve.Function Strong.Function where - tabulate = (runIdentity .) + tabulate = id export Functor f => Representable (Kleislimorphism f) f where @@ -74,8 +74,8 @@ namespace Corepresentable ||| A named implementation of `Corepresentable` for function types. ||| Use this to avoid having to use a type wrapper like `Morphism`. export - [Function] Corepresentable (\a,b => a -> b) Identity using Cosieve.Function where - cotabulate = (. Id) + [Function] Corepresentable (\a,b => a -> b) Prelude.id using Cosieve.Function where + cotabulate = id export Functor f => Corepresentable (Costar f) f where diff --git a/Data/Profunctor/Sieve.idr b/Data/Profunctor/Sieve.idr index 4444e50..07f6ece 100644 --- a/Data/Profunctor/Sieve.idr +++ b/Data/Profunctor/Sieve.idr @@ -37,8 +37,8 @@ Sieve Morphism Identity where ||| A named implementation of `Sieve` for function types. ||| Use this to avoid having to use a type wrapper like `Morphism`. public export -[Function] Sieve (\a,b => a -> b) Identity using Profunctor.Function where - sieve = (Id .) +[Function] Sieve (\a,b => a -> b) Prelude.id using Profunctor.Function FunctorId where + sieve = id public export Functor f => Sieve (Kleislimorphism f) f where @@ -61,8 +61,8 @@ namespace Cosieve ||| A named implementation of `Cosieve` for function types. ||| Use this to avoid having to use a type wrapper like `Morphism`. public export - [Function] Cosieve (\a,b => a -> b) Identity using Profunctor.Function where - cosieve = (. runIdentity) + [Function] Cosieve (\a,b => a -> b) Prelude.id using Profunctor.Function FunctorId where + cosieve = id public export Functor f => Cosieve (Costar f) f where diff --git a/Data/Profunctor/Traversing.idr b/Data/Profunctor/Traversing.idr index 01b72f5..d3ccbb4 100644 --- a/Data/Profunctor/Traversing.idr +++ b/Data/Profunctor/Traversing.idr @@ -1,7 +1,6 @@ module Data.Profunctor.Traversing import Control.Applicative.Const -import Control.Monad.Identity import Data.Morphisms import Data.Tensor import Data.Profunctor @@ -22,14 +21,6 @@ import Data.Profunctor [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 @@ -54,7 +45,7 @@ Functor (Baz t b) where sold : Baz t a a -> t -sold m = runIdentity (runBaz m Id) +sold m = runBaz @{ApplicativeId} m id Foldable (Baz t b) where foldr f i bz = runBaz bz @{appEndo} f i @@ -103,14 +94,14 @@ interface (Strong p, Choice p) => Traversing p where public export Traversing Morphism where traverse' (Mor f) = Mor (map f) - wander f (Mor p) = Mor (runIdentity . (f $ Id . p)) + wander f (Mor p) = Mor (f @{ApplicativeId} p) ||| A named implementation of `Traversing` for function types. ||| Use this to avoid having to use a type wrapper like `Morphism`. public export [Function] Traversing (\a,b => a -> b) using Strong.Function where traverse' = map - wander f g = runIdentity . (f $ Id . g) + wander f = f @{ApplicativeId} public export Applicative f => Traversing (Kleislimorphism f) where @@ -166,7 +157,7 @@ ProfunctorFunctor CofreeTraversing where public export ProfunctorComonad CofreeTraversing where - proextract (MkCFT p) = dimap Id runIdentity $ p @{TraversableIdentity} + proextract (MkCFT p) = p @{TraversableId} produplicate (MkCFT p) = MkCFT $ MkCFT $ p @{Compose} public export @@ -220,7 +211,7 @@ ProfunctorFunctor FreeTraversing where public export ProfunctorMonad FreeTraversing where - propure p = MkFT @{TraversableIdentity} runIdentity p Id + propure p = MkFT @{TraversableId} id p id projoin (MkFT l' (MkFT l m r) r') = MkFT @{Compose} (l' . map l) m (map r . r') @@ -230,4 +221,4 @@ freeTraversing fn (MkFT {f} l m r) = dimap r l (traverse' {f} (fn m)) public export unfreeTraversing : FreeTraversing p :-> q -> p :-> q -unfreeTraversing f p = f (MkFT @{TraversableIdentity} runIdentity p Id) +unfreeTraversing f p = f (MkFT @{TraversableId} id p id) diff --git a/Data/Profunctor/Types.idr b/Data/Profunctor/Types.idr index c8ae8bb..90e314b 100644 --- a/Data/Profunctor/Types.idr +++ b/Data/Profunctor/Types.idr @@ -276,3 +276,37 @@ Profunctor (Coforget r) where dimap _ f (MkCoforget k) = MkCoforget (f . k) lmap _ = recoforget rmap = map + + +------------------------------------------------------------------------------ +-- Identity functor +------------------------------------------------------------------------------ + +-- A few convenience definitions for use in other modules. + +public export +[FunctorId] Functor Prelude.id where + map = id + +public export +[ApplicativeId] Applicative Prelude.id using FunctorId where + pure = id + (<*>) = id + +public export +[MonadId] Monad Prelude.id using ApplicativeId where + join = id + (>>=) = flip id + +public export +[FoldableId] Foldable Prelude.id where + foldr = flip + foldl = id + null _ = False + foldlM = id + toList = pure + foldMap = id + +public export +[TraversableId] Traversable Prelude.id using FunctorId FoldableId where + traverse = id