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

Compare commits

base: toki:4be8bc5dfc72927a3088daa480570a8e9d887c42
Branches Tags
toki:main
toki:v1.1.0
toki:v1.0.0
..
compare: toki:e862ef887f9dcdf90eacb1ca1c0a997d7a251135
Branches Tags
toki:main
toki:v1.1.0
toki:v1.0.0

10 commits
4be8bc5dfc ... e862ef887f

Author SHA1 Message Date
Kiana Sheibani e862ef887f
Update ipkg 2023-03-30 14:10:13 -04:00
Kiana Sheibani 3c87261627
Prefer using Prelude.id over Identity 2023-03-30 14:08:24 -04:00
Kiana Sheibani 5b55d39ab5
Refactor Data.Profunctor.Mapping 2023-03-30 13:43:33 -04:00
Kiana Sheibani 68ef29160f
Change visibility on everything to public export 2023-03-30 13:32:45 -04:00
Kiana Sheibani 573c461d9b
Add brief package description 2023-03-14 14:06:13 -04:00
Kiana Sheibani 38970b9cd5
Fix Traversing default implementation 2023-03-14 12:52:45 -04:00
Kiana Sheibani 3f6936b5b1
Update ipkg 2023-03-08 15:05:57 -05:00
Kiana Sheibani 55061adc1b
Fix documentation headers 2023-03-08 15:05:28 -05:00
Kiana Sheibani 7ff2746ab4
Define new profunctors Forget and Coforget 2023-03-08 15:05:07 -05:00
Kiana Sheibani 99ff1476aa
Implement Corepresentable for Morphism 2023-03-08 13:30:55 -05:00
12 changed files with 389 additions and 214 deletions
Show stats Expand all files Collapse all files

22
Data/Profunctor/Cayley.idr
View file

@ -18,50 +18,50 @@ record Cayley {0 k1,k2,k3 : Type} f (p : k1 -> k2 -> k3) a b where
runCayley : f (p a b) runCayley : f (p a b)
export public export
Functor f => Profunctor p => Profunctor (Cayley f p) where Functor f => Profunctor p => Profunctor (Cayley f p) where
dimap f g (MkCayley p) = MkCayley (dimap f g <$> p) dimap f g (MkCayley p) = MkCayley (dimap f g <$> p)
lmap f (MkCayley p) = MkCayley (lmap f <$> p) lmap f (MkCayley p) = MkCayley (lmap f <$> p)
rmap g (MkCayley p) = MkCayley (rmap g <$> p) rmap g (MkCayley p) = MkCayley (rmap g <$> p)
export public export
Functor f => ProfunctorFunctor (Cayley f) where Functor f => ProfunctorFunctor (Cayley f) where
promap f (MkCayley p) = MkCayley (map f p) promap f (MkCayley p) = MkCayley (map f p)
export public export
Monad m => ProfunctorMonad (Cayley m) where Monad m => ProfunctorMonad (Cayley m) where
propure = MkCayley . pure propure = MkCayley . pure
projoin (MkCayley p) = MkCayley $ p >>= runCayley projoin (MkCayley p) = MkCayley $ p >>= runCayley
export public export
Functor f => GenStrong ten p => GenStrong ten (Cayley f p) where Functor f => GenStrong ten p => GenStrong ten (Cayley f p) where
strongl (MkCayley p) = MkCayley (strongl {ten} <$> p) strongl (MkCayley p) = MkCayley (strongl {ten} <$> p)
strongr (MkCayley p) = MkCayley (strongr {ten} <$> p) strongr (MkCayley p) = MkCayley (strongr {ten} <$> p)
export public export
Functor f => GenCostrong ten p => GenCostrong ten (Cayley f p) where Functor f => GenCostrong ten p => GenCostrong ten (Cayley f p) where
costrongl (MkCayley p) = MkCayley (costrongl {ten} <$> p) costrongl (MkCayley p) = MkCayley (costrongl {ten} <$> p)
costrongr (MkCayley p) = MkCayley (costrongr {ten} <$> p) costrongr (MkCayley p) = MkCayley (costrongr {ten} <$> p)
export public export
Functor f => Closed p => Closed (Cayley f p) where Functor f => Closed p => Closed (Cayley f p) where
closed (MkCayley p) = MkCayley (closed <$> p) closed (MkCayley p) = MkCayley (closed <$> p)
export public export
Functor f => Traversing p => Traversing (Cayley f p) where Functor f => Traversing p => Traversing (Cayley f p) where
traverse' (MkCayley p) = MkCayley (traverse' <$> p) traverse' (MkCayley p) = MkCayley (traverse' <$> p)
wander f (MkCayley p) = MkCayley (wander f <$> p) wander f (MkCayley p) = MkCayley (wander f <$> p)
export public export
Functor f => Mapping p => Mapping (Cayley f p) where Functor f => Mapping p => Mapping (Cayley f p) where
map' (MkCayley p) = MkCayley (map' <$> p) map' (MkCayley p) = MkCayley (map' <$> p)
roam f (MkCayley p) = MkCayley (roam f <$> p) roam f (MkCayley p) = MkCayley (roam f <$> p)
export public export
Functor g => Sieve p f => Sieve (Cayley g p) (g . f) using Functor.Compose where Functor g => Sieve p f => Sieve (Cayley g p) (g . f) using Functor.Compose where
sieve (MkCayley p) x = ($ x) . sieve <$> p sieve (MkCayley p) x = ($ x) . sieve <$> p
export public export
mapCayley : (forall x. f x -> g x) -> Cayley f p a b -> Cayley g p a b mapCayley : (forall x. f x -> g x) -> Cayley f p :-> Cayley g p
mapCayley f (MkCayley p) = MkCayley (f p) mapCayley f (MkCayley p) = MkCayley (f p)

42
Data/Profunctor/Closed.idr
View file

@ -26,26 +26,26 @@ interface Profunctor p => Closed p where
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
-- Implementations for existing types -- Implementations
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
export public export
Closed Morphism where Closed Morphism where
closed (Mor f) = Mor (f .) closed (Mor f) = Mor (f .)
||| A named implementation of `Closed` for function types. ||| A named implementation of `Closed` for function types.
||| Use this to avoid having to use a type wrapper like `Morphism`. ||| Use this to avoid having to use a type wrapper like `Morphism`.
export public export
[Function] Closed (\a,b => a -> b) using Profunctor.Function where [Function] Closed (\a,b => a -> b) using Profunctor.Function where
closed = (.) closed = (.)
export public export
Functor f => Closed (Costar f) where Functor f => Closed (Costar f) where
closed (MkCostar p) = MkCostar $ \f,x => p (map ($ x) f) closed (MkCostar p) = MkCostar $ \f,x => p (map ($ x) f)
export public export
curry' : Closed p => p (a, b) c -> p a (b -> c) curry' : Closed p => p (a, b) c -> p a (b -> c)
curry' = lmap (,) . closed curry' = lmap (,) . closed
@ -71,40 +71,40 @@ record Closure p a b where
runClosure : forall x. p (x -> a) (x -> b) runClosure : forall x. p (x -> a) (x -> b)
export public export
Profunctor p => Profunctor (Closure p) where Profunctor p => Profunctor (Closure p) where
dimap f g (MkClosure p) = MkClosure $ dimap (f .) (g .) p dimap f g (MkClosure p) = MkClosure $ dimap (f .) (g .) p
lmap f (MkClosure p) = MkClosure $ lmap (f .) p lmap f (MkClosure p) = MkClosure $ lmap (f .) p
rmap f (MkClosure p) = MkClosure $ rmap (f .) p rmap f (MkClosure p) = MkClosure $ rmap (f .) p
export public export
ProfunctorFunctor Closure where ProfunctorFunctor Closure where
promap f (MkClosure p) = MkClosure (f p) promap f (MkClosure p) = MkClosure (f p)
export public export
ProfunctorComonad Closure where ProfunctorComonad Closure where
proextract (MkClosure p) = dimap const ($ ()) p proextract (MkClosure p) = dimap const ($ ()) p
produplicate (MkClosure p) = MkClosure $ MkClosure $ dimap uncurry curry p produplicate (MkClosure p) = MkClosure $ MkClosure $ dimap uncurry curry p
export public export
Strong p => GenStrong Pair (Closure p) where Strong p => GenStrong Pair (Closure p) where
strongl (MkClosure p) = MkClosure $ dimap hither yon $ first p strongl (MkClosure p) = MkClosure $ dimap hither yon $ first p
strongr (MkClosure p) = MkClosure $ dimap hither yon $ second p strongr (MkClosure p) = MkClosure $ dimap hither yon $ second p
export public export
Profunctor p => Closed (Closure p) where Profunctor p => Closed (Closure p) where
closed p = runClosure $ produplicate p closed p = runClosure $ produplicate p
export public export
Profunctor p => Functor (Closure p a) where Profunctor p => Functor (Closure p a) where
map = rmap map = rmap
export public export
close : Closed p => p :-> q -> p :-> Closure q close : Closed p => p :-> q -> p :-> Closure q
close f p = MkClosure $ f $ closed p close f p = MkClosure $ f $ closed p
export public export
unclose : Profunctor q => p :-> Closure q -> p :-> q unclose : Profunctor q => p :-> Closure q -> p :-> q
unclose f p = dimap const ($ ()) $ runClosure $ f p unclose f p = dimap const ($ ()) $ runClosure $ f p
@ -121,17 +121,17 @@ data Environment : (p : Type -> Type -> Type) -> Type -> Type -> Type where
MkEnv : ((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b MkEnv : ((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b
export public export
Profunctor (Environment p) where Profunctor (Environment p) where
dimap f g (MkEnv l m r) = MkEnv (g . l) m (r . f) dimap f g (MkEnv l m r) = MkEnv (g . l) m (r . f)
lmap f (MkEnv l m r) = MkEnv l m (r . f) lmap f (MkEnv l m r) = MkEnv l m (r . f)
rmap g (MkEnv l m r) = MkEnv (g . l) m r rmap g (MkEnv l m r) = MkEnv (g . l) m r
export public export
ProfunctorFunctor Environment where ProfunctorFunctor Environment where
promap f (MkEnv l m r) = MkEnv l (f m) r promap f (MkEnv l m r) = MkEnv l (f m) r
export public export
ProfunctorMonad Environment where ProfunctorMonad Environment where
propure p = MkEnv ($ ()) p const propure p = MkEnv ($ ()) p const
projoin (MkEnv {x=x',y=y',z=z'} l' (MkEnv {x,y,z} l m r) r') = MkEnv (ll . curry) m rr projoin (MkEnv {x=x',y=y',z=z'} l' (MkEnv {x,y,z} l m r) r') = MkEnv (ll . curry) m rr
@ -141,12 +141,12 @@ ProfunctorMonad Environment where
rr : a -> (z', z) -> x rr : a -> (z', z) -> x
rr a (b, c) = r (r' a b) c rr a (b, c) = r (r' a b) c
export public export
ProfunctorAdjunction Environment Closure where ProfunctorAdjunction Environment Closure where
prounit p = MkClosure (MkEnv id p id) prounit p = MkClosure (MkEnv id p id)
procounit (MkEnv l (MkClosure x) r) = dimap r l x procounit (MkEnv l (MkClosure x) r) = dimap r l x
export public export
Closed (Environment p) where Closed (Environment p) where
closed {x=x'} (MkEnv {x,y,z} l m r) = MkEnv l' m r' closed {x=x'} (MkEnv {x,y,z} l m r) = MkEnv l' m r'
where where
@ -155,15 +155,15 @@ Closed (Environment p) where
r' : (x' -> a) -> (z, x') -> x r' : (x' -> a) -> (z, x') -> x
r' f (z,x) = r (f x) z r' f (z,x) = r (f x) z
export public export
Profunctor p => Functor (Environment p a) where Profunctor p => Functor (Environment p a) where
map = rmap map = rmap
export public export
environment : Closed q => p :-> q -> Environment p :-> q environment : Closed q => p :-> q -> Environment p :-> q
environment f (MkEnv l m r) = dimap r l $ closed (f m) environment f (MkEnv l m r) = dimap r l $ closed (f m)
export public export
unenvironment : Environment p :-> q -> p :-> q unenvironment : Environment p :-> q -> p :-> q
unenvironment f p = f (MkEnv ($ ()) p const) unenvironment f p = f (MkEnv ($ ()) p const)

42
Data/Profunctor/Costrong.idr
View file

@ -80,15 +80,25 @@ unright = costrongr {ten=Either}
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
-- Implementations for existing types -- Implementations
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
export public export
GenCostrong Pair Tagged where GenCostrong Pair Tagged where
costrongl (Tag (x,_)) = Tag x costrongl (Tag (x,_)) = Tag x
costrongr (Tag (_,x)) = Tag x costrongr (Tag (_,x)) = Tag x
public export
GenCostrong Either (Forget r) where
costrongl (MkForget k) = MkForget (k . Left)
costrongr (MkForget k) = MkForget (k . Right)
public export
GenCostrong Pair (Coforget r) where
costrongl (MkCoforget k) = MkCoforget (fst . k)
costrongr (MkCoforget k) = MkCoforget (snd . k)
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
-- Cotambara -- Cotambara
@ -101,27 +111,27 @@ public export
data GenCotambara : (ten, p : Type -> Type -> Type) -> Type -> Type -> Type where data GenCotambara : (ten, p : Type -> Type -> Type) -> Type -> Type -> Type where
MkCotambara : GenCostrong ten q => q :-> p -> q a b -> GenCotambara ten p a b MkCotambara : GenCostrong ten q => q :-> p -> q a b -> GenCotambara ten p a b
export public export
Profunctor (GenCotambara ten p) where Profunctor (GenCotambara ten p) where
lmap f (MkCotambara n p) = MkCotambara n (lmap f p) lmap f (MkCotambara n p) = MkCotambara n (lmap f p)
rmap f (MkCotambara n p) = MkCotambara n (rmap f p) rmap f (MkCotambara n p) = MkCotambara n (rmap f p)
dimap f g (MkCotambara n p) = MkCotambara n (dimap f g p) dimap f g (MkCotambara n p) = MkCotambara n (dimap f g p)
export public export
ProfunctorFunctor (GenCotambara ten) where ProfunctorFunctor (GenCotambara ten) where
promap f (MkCotambara n p) = MkCotambara (f . n) p promap f (MkCotambara n p) = MkCotambara (f . n) p
export public export
GenCostrong ten (GenCotambara ten p) where GenCostrong ten (GenCotambara ten p) where
costrongl (MkCotambara @{costr} n p) = MkCotambara n (costrongl @{costr} p) costrongl (MkCotambara @{costr} n p) = MkCotambara n (costrongl @{costr} p)
costrongr (MkCotambara @{costr} n p) = MkCotambara n (costrongr @{costr} p) costrongr (MkCotambara @{costr} n p) = MkCotambara n (costrongr @{costr} p)
export public export
ProfunctorComonad (GenCotambara ten) where ProfunctorComonad (GenCotambara ten) where
proextract (MkCotambara n p) = n p proextract (MkCotambara n p) = n p
produplicate (MkCotambara n p) = MkCotambara id (MkCotambara n p) produplicate (MkCotambara n p) = MkCotambara id (MkCotambara n p)
export public export
Functor (GenCotambara ten p a) where Functor (GenCotambara ten p a) where
map = rmap map = rmap
@ -143,11 +153,11 @@ CotambaraSum : (p : Type -> Type -> Type) -> Type -> Type -> Type
CotambaraSum = GenCotambara Either CotambaraSum = GenCotambara Either
export public export
cotambara : GenCostrong ten p => p :-> q -> p :-> GenCotambara ten q cotambara : GenCostrong ten p => p :-> q -> p :-> GenCotambara ten q
cotambara f = MkCotambara f cotambara f = MkCotambara f
export public export
uncotambara : Tensor ten i => Profunctor q => p :-> GenCotambara ten q -> p :-> q uncotambara : Tensor ten i => Profunctor q => p :-> GenCotambara ten q -> p :-> q
uncotambara f p = proextract (f p) uncotambara f p = proextract (f p)
@ -164,27 +174,27 @@ record GenCopastro (ten, p : Type -> Type -> Type) a b where
constructor MkCopastro constructor MkCopastro
runCopastro : forall q. GenCostrong ten q => p :-> q -> q a b runCopastro : forall q. GenCostrong ten q => p :-> q -> q a b
export public export
Profunctor (GenCopastro ten p) where Profunctor (GenCopastro ten p) where
dimap f g (MkCopastro h) = MkCopastro $ \n => dimap f g (h n) dimap f g (MkCopastro h) = MkCopastro $ \n => dimap f g (h n)
lmap f (MkCopastro h) = MkCopastro $ \n => lmap f (h n) lmap f (MkCopastro h) = MkCopastro $ \n => lmap f (h n)
rmap f (MkCopastro h) = MkCopastro $ \n => rmap f (h n) rmap f (MkCopastro h) = MkCopastro $ \n => rmap f (h n)
export public export
ProfunctorFunctor (GenCopastro ten) where ProfunctorFunctor (GenCopastro ten) where
promap f (MkCopastro h) = MkCopastro $ \n => h (n . f) promap f (MkCopastro h) = MkCopastro $ \n => h (n . f)
export public export
ProfunctorMonad (GenCopastro ten) where ProfunctorMonad (GenCopastro ten) where
propure p = MkCopastro ($ p) propure p = MkCopastro ($ p)
projoin p = MkCopastro $ \x => runCopastro p (\y => runCopastro y x) projoin p = MkCopastro $ \x => runCopastro p (\y => runCopastro y x)
export public export
GenCostrong ten (GenCopastro ten p) where GenCostrong ten (GenCopastro ten p) where
costrongl (MkCopastro h) = MkCopastro $ \n => costrongl {ten} (h n) costrongl (MkCopastro h) = MkCopastro $ \n => costrongl {ten} (h n)
costrongr (MkCopastro h) = MkCopastro $ \n => costrongr {ten} (h n) costrongr (MkCopastro h) = MkCopastro $ \n => costrongr {ten} (h n)
export public export
ProfunctorAdjunction (GenCopastro ten) (GenCotambara ten) where ProfunctorAdjunction (GenCopastro ten) (GenCotambara ten) where
prounit p = MkCotambara id (propure {t=GenCopastro ten} p) prounit p = MkCotambara id (propure {t=GenCopastro ten} p)
procounit (MkCopastro h) = proextract (h id) procounit (MkCopastro h) = proextract (h id)
@ -207,10 +217,10 @@ CopastroSum : (p : Type -> Type -> Type) -> Type -> Type -> Type
CopastroSum = GenCopastro Either CopastroSum = GenCopastro Either
export public export
copastro : GenCostrong ten q => p :-> q -> GenCopastro ten p :-> q copastro : GenCostrong ten q => p :-> q -> GenCopastro ten p :-> q
copastro f (MkCopastro h) = h f copastro f (MkCopastro h) = h f
export public export
uncopastro : Tensor ten i => GenCopastro ten p :-> q -> p :-> q uncopastro : Tensor ten i => GenCopastro ten p :-> q -> p :-> q
uncopastro f x = f (MkCopastro ($ x)) uncopastro f x = f (MkCopastro ($ x))

65
Data/Profunctor/Mapping.idr
View file

@ -1,6 +1,5 @@
module Data.Profunctor.Mapping module Data.Profunctor.Mapping
import Control.Monad.Identity
import Data.Morphisms import Data.Morphisms
import Data.Tensor import Data.Tensor
import Data.Profunctor import Data.Profunctor
@ -9,6 +8,9 @@ import Data.Profunctor.Traversing
%default total %default total
functor : Functor (\a => (a -> b) -> t)
functor = MkFunctor (\f => (. (. f)))
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
-- Mapping interface -- Mapping interface
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
@ -20,7 +22,7 @@ import Data.Profunctor.Traversing
||| * `map' . lmap f = lmap (map f) . map'` ||| * `map' . lmap f = lmap (map f) . map'`
||| * `map' . rmap f = rmap (map f) . map'` ||| * `map' . rmap f = rmap (map f) . map'`
||| * `map' . map' = map' @{Compose}` ||| * `map' . map' = map' @{Compose}`
||| * `dimap Identity runIdentity . map' = id` ||| * `dimap Id runIdentity . map' = id`
public export public export
interface (Traversing p, Closed p) => Mapping p where interface (Traversing p, Closed p) => Mapping p where
map' : Functor f => p a b -> p (f a) (f b) map' : Functor f => p a b -> p (f a) (f b)
@ -28,24 +30,21 @@ interface (Traversing p, Closed p) => Mapping p where
roam : ((a -> b) -> s -> t) -> p a b -> p s t roam : ((a -> b) -> s -> t) -> p a b -> p s t
roam f = dimap (flip f) ($ id) . map' @{%search} @{functor} roam f = dimap (flip f) ($ id) . map' @{%search} @{functor}
where
functor : Functor (\a => (a -> b) -> t)
functor = MkFunctor (\f => (. (. f)))
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
-- Implementations for existing types -- Implementations
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
export public export
Mapping Morphism where Mapping Morphism where
map' (Mor f) = Mor (map f) map' (Mor f) = Mor (map f)
roam f (Mor x) = Mor (f x) roam f (Mor x) = Mor (f x)
||| A named implementation of `Mapping` for function types. ||| A named implementation of `Mapping` for function types.
||| Use this to avoid having to use a type wrapper like `Morphism`. ||| Use this to avoid having to use a type wrapper like `Morphism`.
export public export
[Function] Mapping (\a,b => a -> b) [Function] Mapping (\a,b => a -> b)
using Traversing.Function Closed.Function where using Traversing.Function Closed.Function where
map' = map map' = map
@ -53,7 +52,7 @@ export
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
-- Implementations for existing types -- CofreeMapping
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
@ -64,47 +63,44 @@ record CofreeMapping p a b where
constructor MkCFM constructor MkCFM
runCFM : forall f. Functor f => p (f a) (f b) runCFM : forall f. Functor f => p (f a) (f b)
export public export
Profunctor p => Profunctor (CofreeMapping p) where Profunctor p => Profunctor (CofreeMapping p) where
lmap f (MkCFM p) = MkCFM (lmap (map f) p) lmap f (MkCFM p) = MkCFM (lmap (map f) p)
rmap f (MkCFM p) = MkCFM (rmap (map f) p) rmap f (MkCFM p) = MkCFM (rmap (map f) p)
dimap f g (MkCFM p) = MkCFM (dimap (map f) (map g) p) dimap f g (MkCFM p) = MkCFM (dimap (map f) (map g) p)
export public export
Profunctor p => Functor (CofreeMapping p a) where Profunctor p => Functor (CofreeMapping p a) where
map = rmap map = rmap
export public export
ProfunctorFunctor CofreeMapping where ProfunctorFunctor CofreeMapping where
promap f (MkCFM p) = MkCFM (f p) promap f (MkCFM p) = MkCFM (f p)
export public export
ProfunctorComonad CofreeMapping where ProfunctorComonad CofreeMapping where
proextract (MkCFM p) = dimap Id runIdentity p proextract (MkCFM p) = p @{FunctorId}
produplicate (MkCFM p) = MkCFM $ MkCFM $ p @{Compose} produplicate (MkCFM p) = MkCFM $ MkCFM $ p @{Compose}
export public export
Symmetric ten => Profunctor p => GenStrong ten (CofreeMapping p) where Symmetric ten => Profunctor p => GenStrong ten (CofreeMapping p) where
strongr (MkCFM p) = MkCFM (p @{Compose {g=ten c} @{%search} @{MkFunctor mapSnd}}) strongr (MkCFM p) = MkCFM (p @{Compose {g=ten c} @{%search} @{MkFunctor mapSnd}})
strongl (MkCFM p) = MkCFM (p @{Compose {g=(`ten` c)} @{%search} @{MkFunctor mapFst}}) strongl (MkCFM p) = MkCFM (p @{Compose {g=(`ten` c)} @{%search} @{MkFunctor mapFst}})
export public export
Profunctor p => Closed (CofreeMapping p) where Profunctor p => Closed (CofreeMapping p) where
closed (MkCFM p) = MkCFM (p @{Compose {g = \b => x -> b} @{%search} @{MkFunctor (.)}}) closed (MkCFM p) = MkCFM (p @{Compose {g = \b => x -> b} @{%search} @{MkFunctor (.)}})
roamCofree : Profunctor p => ((a -> b) -> s -> t) -> CofreeMapping p a b -> CofreeMapping p s t roamCofree : Profunctor p => ((a -> b) -> s -> t) -> CofreeMapping p a b -> CofreeMapping p s t
roamCofree f (MkCFM p) = MkCFM $ dimap (map (flip f)) (map ($ id)) $ roamCofree f (MkCFM p) = MkCFM $ dimap (map (flip f)) (map ($ id)) $
p @{Compose @{%search} @{functor}} p @{Compose @{%search} @{functor}}
where
functor : Functor (\a => (a -> b) -> t)
functor = MkFunctor (\f => (. (. f)))
export public export
Profunctor p => Traversing (CofreeMapping p) where Profunctor p => Traversing (CofreeMapping p) where
traverse' (MkCFM p) = MkCFM (p @{Compose}) traverse' (MkCFM p) = MkCFM (p @{Compose})
wander f = roamCofree $ (runIdentity .) . f . (Id .) wander f = roamCofree $ f @{ApplicativeId}
export public export
Profunctor p => Mapping (CofreeMapping p) where Profunctor p => Mapping (CofreeMapping p) where
map' (MkCFM p) = MkCFM (p @{Compose}) map' (MkCFM p) = MkCFM (p @{Compose})
roam = roamCofree roam = roamCofree
@ -119,51 +115,48 @@ public export
data FreeMapping : (p : Type -> Type -> Type) -> Type -> Type -> Type where data FreeMapping : (p : Type -> Type -> Type) -> Type -> Type -> Type where
MkFM : Functor f => (f y -> b) -> p x y -> (a -> f x) -> FreeMapping p a b MkFM : Functor f => (f y -> b) -> p x y -> (a -> f x) -> FreeMapping p a b
export public export
Profunctor (FreeMapping p) where Profunctor (FreeMapping p) where
lmap f (MkFM l m r) = MkFM l m (r . f) lmap f (MkFM l m r) = MkFM l m (r . f)
rmap f (MkFM l m r) = MkFM (f . l) m r rmap f (MkFM l m r) = MkFM (f . l) m r
dimap f g (MkFM l m r) = MkFM (g . l) m (r . f) dimap f g (MkFM l m r) = MkFM (g . l) m (r . f)
export public export
ProfunctorFunctor FreeMapping where ProfunctorFunctor FreeMapping where
promap f (MkFM l m r) = MkFM l (f m) r promap f (MkFM l m r) = MkFM l (f m) r
export public export
ProfunctorMonad FreeMapping where 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') projoin (MkFM l' (MkFM l m r) r') = MkFM @{Compose} (l' . map l) m (map r . r')
export public export
Functor (FreeMapping p a) where Functor (FreeMapping p a) where
map = rmap map = rmap
export public export
GenStrong Pair (FreeMapping p) where GenStrong Pair (FreeMapping p) where
strongr (MkFM l m r) = MkFM @{Compose} (map l) m (map r) strongr (MkFM l m r) = MkFM @{Compose} (map l) m (map r)
strongl = dimap swap' swap' . strongr {p=FreeMapping p} strongl = dimap swap' swap' . strongr {p=FreeMapping p}
export public export
GenStrong Either (FreeMapping p) where GenStrong Either (FreeMapping p) where
strongr (MkFM l m r) = MkFM @{Compose} (map l) m (map r) strongr (MkFM l m r) = MkFM @{Compose} (map l) m (map r)
strongl = dimap swap' swap' . strongr {p=FreeMapping p} strongl = dimap swap' swap' . strongr {p=FreeMapping p}
export public export
Closed (FreeMapping p) where Closed (FreeMapping p) where
closed (MkFM l m r) = dimap Mor applyMor $ MkFM @{Compose} (map l) m (map r) closed (MkFM l m r) = dimap Mor applyMor $ MkFM @{Compose} (map l) m (map r)
roamFree : ((a -> b) -> s -> t) -> FreeMapping p a b -> FreeMapping p s t roamFree : ((a -> b) -> s -> t) -> FreeMapping p a b -> FreeMapping p s t
roamFree f (MkFM l m r) = MkFM @{Compose @{functor}} (($ id) . map @{functor} l) m (map @{functor} r . flip f) roamFree f (MkFM l m r) = MkFM @{Compose @{functor}} (($ id) . map @{functor} l) m (map @{functor} r . flip f)
where
functor : Functor (\a => (a -> b) -> t)
functor = MkFunctor (\f => (. (. f)))
export public export
Traversing (FreeMapping p) where Traversing (FreeMapping p) where
traverse' (MkFM l m r) = MkFM @{Compose} (map l) m (map r) traverse' (MkFM l m r) = MkFM @{Compose} (map l) m (map r)
wander f = roamFree $ (runIdentity .) . f . (Id .) wander f = roamFree $ f @{ApplicativeId}
export public export
Mapping (FreeMapping p) where Mapping (FreeMapping p) where
map' (MkFM l m r) = MkFM @{Compose} (map l) m (map r) map' (MkFM l m r) = MkFM @{Compose} (map l) m (map r)
roam = roamFree roam = roamFree

25
Data/Profunctor/Representable.idr
View file

@ -1,5 +1,6 @@
module Data.Profunctor.Representable module Data.Profunctor.Representable
import Control.Applicative.Const
import Control.Monad.Identity import Control.Monad.Identity
import Data.Morphisms import Data.Morphisms
import Data.Profunctor import Data.Profunctor
@ -20,7 +21,7 @@ interface (Sieve p f, Strong p) => Representable p f | p where
tabulate : (a -> f b) -> p a b tabulate : (a -> f b) -> p a b
||| A profunctor `p` is representable if it is isomorphic to `Costar f` for some `f`. ||| A profunctor `p` is corepresentable if it is isomorphic to `Costar f` for some `f`.
public export public export
interface Cosieve p f => Corepresentable p f | p where interface Cosieve p f => Corepresentable p f | p where
cotabulate : (f a -> b) -> p a b cotabulate : (f a -> b) -> p a b
@ -49,9 +50,9 @@ Representable Morphism Identity where
||| A named implementation of `Representable` for function types. ||| A named implementation of `Representable` for function types.
||| Use this to avoid having to use a type wrapper like `Morphism`. ||| Use this to avoid having to use a type wrapper like `Morphism`.
export export
[Function] Representable (\a,b => a -> b) Identity [Function] Representable (\a,b => a -> b) Prelude.id
using Sieve.Function Strong.Function where using Sieve.Function Strong.Function where
tabulate = (runIdentity .) tabulate = id
export export
Functor f => Representable (Kleislimorphism f) f where Functor f => Representable (Kleislimorphism f) f where
@ -61,9 +62,25 @@ export
Functor f => Representable (Star f) f where Functor f => Representable (Star f) f where
tabulate = MkStar tabulate = MkStar
export
Representable (Forget r) (Const r) where
tabulate = MkForget . (runConst .)
export
Corepresentable Morphism Identity where
cotabulate f = Mor (f . Id)
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) Prelude.id using Cosieve.Function where
cotabulate = id
export export
Functor f => Corepresentable (Costar f) f where Functor f => Corepresentable (Costar f) f where
cotabulate = MkCostar cotabulate = MkCostar
export
Corepresentable (Coforget r) (Const r) where
cotabulate = MkCoforget . (. MkConst)

30
Data/Profunctor/Sieve.idr
View file

@ -1,5 +1,6 @@
module Data.Profunctor.Sieve module Data.Profunctor.Sieve
import Control.Applicative.Const
import Control.Monad.Identity import Control.Monad.Identity
import Data.Morphisms import Data.Morphisms
import Data.Profunctor import Data.Profunctor
@ -29,37 +30,44 @@ interface (Profunctor p, Functor f) => Cosieve p f | p where
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
export public export
Sieve Morphism Identity where Sieve Morphism Identity where
sieve (Mor f) = Id . f sieve (Mor f) = Id . f
||| A named implementation of `Sieve` for function types. ||| A named implementation of `Sieve` for function types.
||| Use this to avoid having to use a type wrapper like `Morphism`. ||| Use this to avoid having to use a type wrapper like `Morphism`.
export public export
[Function] Sieve (\a,b => a -> b) Identity using Profunctor.Function where [Function] Sieve (\a,b => a -> b) Prelude.id using Profunctor.Function FunctorId where
sieve = (Id .) sieve = id
export public export
Functor f => Sieve (Kleislimorphism f) f where Functor f => Sieve (Kleislimorphism f) f where
sieve = applyKleisli sieve = applyKleisli
export public export
Functor f => Sieve (Star f) f where Functor f => Sieve (Star f) f where
sieve = applyStar sieve = applyStar
public export
Sieve (Forget r) (Const r) where
sieve (MkForget k) = MkConst . k
export public export
Cosieve Morphism Identity where Cosieve Morphism Identity where
cosieve (Mor f) = f . runIdentity cosieve (Mor f) = f . runIdentity
namespace Cosieve namespace Cosieve
||| A named implementation of `Cosieve` for function types. ||| A named implementation of `Cosieve` for function types.
||| Use this to avoid having to use a type wrapper like `Morphism`. ||| Use this to avoid having to use a type wrapper like `Morphism`.
export public export
[Function] Cosieve (\a,b => a -> b) Identity using Profunctor.Function where [Function] Cosieve (\a,b => a -> b) Prelude.id using Profunctor.Function FunctorId where
cosieve = (. runIdentity) cosieve = id
export public export
Functor f => Cosieve (Costar f) f where Functor f => Cosieve (Costar f) f where
cosieve = applyCostar cosieve = applyCostar
public export
Cosieve (Coforget r) (Const r) where
cosieve (MkCoforget k) = k . runConst

63
Data/Profunctor/Strong.idr
View file

@ -80,58 +80,73 @@ right : Choice p => p a b -> p (Either c a) (Either c b)
right = strongr {ten=Either} right = strongr {ten=Either}
export public export
uncurry' : Strong p => p a (b -> c) -> p (a, b) c uncurry' : Strong p => p a (b -> c) -> p (a, b) c
uncurry' = rmap (uncurry id) . first uncurry' = rmap (uncurry id) . first
export public export
strong : Strong p => (a -> b -> c) -> p a b -> p a c strong : Strong p => (a -> b -> c) -> p a b -> p a c
strong f = dimap dup (uncurry $ flip f) . first strong f = dimap dup (uncurry $ flip f) . first
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
-- Implementations for existing types -- Implementations
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
export public export
Bifunctor ten => GenStrong ten Morphism where Bifunctor ten => GenStrong ten Morphism where
strongl (Mor f) = Mor (mapFst f) strongl (Mor f) = Mor (mapFst f)
strongr (Mor f) = Mor (mapSnd f) strongr (Mor f) = Mor (mapSnd f)
||| A named implementation of `GenStrong` for function types. ||| A named implementation of `GenStrong` for function types.
||| Use this to avoid having to use a type wrapper like `Morphism`. ||| Use this to avoid having to use a type wrapper like `Morphism`.
export public export
[Function] Bifunctor ten => GenStrong ten (\a,b => a -> b) [Function] Bifunctor ten => GenStrong ten (\a,b => a -> b)
using Profunctor.Function where using Profunctor.Function where
strongl = mapFst strongl = mapFst
strongr = mapSnd strongr = mapSnd
export public export
Functor f => GenStrong Pair (Kleislimorphism f) where Functor f => GenStrong Pair (Kleislimorphism f) where
strongl (Kleisli f) = Kleisli $ \(a,c) => (,c) <$> f a strongl (Kleisli f) = Kleisli $ \(a,c) => (,c) <$> f a
strongr (Kleisli f) = Kleisli $ \(c,a) => (c,) <$> f a strongr (Kleisli f) = Kleisli $ \(c,a) => (c,) <$> f a
export public export
Applicative f => GenStrong Either (Kleislimorphism f) where Applicative f => GenStrong Either (Kleislimorphism f) where
strongl (Kleisli f) = Kleisli $ either (map Left . f) (pure . Right) strongl (Kleisli f) = Kleisli $ either (map Left . f) (pure . Right)
strongr (Kleisli f) = Kleisli $ either (pure . Left) (map Right . f) strongr (Kleisli f) = Kleisli $ either (pure . Left) (map Right . f)
export public export
Functor f => GenStrong Pair (Star f) where Functor f => GenStrong Pair (Star f) where
strongl (MkStar f) = MkStar $ \(a,c) => (,c) <$> f a strongl (MkStar f) = MkStar $ \(a,c) => (,c) <$> f a
strongr (MkStar f) = MkStar $ \(c,a) => (c,) <$> f a strongr (MkStar f) = MkStar $ \(c,a) => (c,) <$> f a
export public export
Applicative f => GenStrong Either (Star f) where Applicative f => GenStrong Either (Star f) where
strongl (MkStar f) = MkStar $ either (map Left . f) (pure . Right) strongl (MkStar f) = MkStar $ either (map Left . f) (pure . Right)
strongr (MkStar f) = MkStar $ either (pure . Left) (map Right . f) strongr (MkStar f) = MkStar $ either (pure . Left) (map Right . f)
export public export
GenStrong Either Tagged where GenStrong Either Tagged where
strongl (Tag x) = Tag (Left x) strongl (Tag x) = Tag (Left x)
strongr (Tag x) = Tag (Right x) strongr (Tag x) = Tag (Right x)
public export
GenStrong Pair (Forget r) where
strongl (MkForget k) = MkForget (k . fst)
strongr (MkForget k) = MkForget (k . snd)
public export
Monoid r => GenStrong Either (Forget r) where
strongl (MkForget k) = MkForget (either k (const neutral))
strongr (MkForget k) = MkForget (either (const neutral) k)
public export
GenStrong Either (Coforget r) where
strongl (MkCoforget k) = MkCoforget (Left . k)
strongr (MkCoforget k) = MkCoforget (Right . k)
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
-- Tambara -- Tambara
@ -145,26 +160,26 @@ record GenTambara (ten, p : Type -> Type -> Type) a b where
constructor MkTambara constructor MkTambara
runTambara : forall c. p (a `ten` c) (b `ten` c) runTambara : forall c. p (a `ten` c) (b `ten` c)
export public export
Bifunctor ten => Profunctor p => Profunctor (GenTambara ten p) where Bifunctor ten => Profunctor p => Profunctor (GenTambara ten p) where
dimap f g (MkTambara p) = MkTambara $ dimap (mapFst f) (mapFst g) p dimap f g (MkTambara p) = MkTambara $ dimap (mapFst f) (mapFst g) p
export public export
ProfunctorFunctor (GenTambara ten) where ProfunctorFunctor (GenTambara ten) where
promap f (MkTambara p) = MkTambara (f p) promap f (MkTambara p) = MkTambara (f p)
export public export
Tensor ten i => ProfunctorComonad (GenTambara ten) where Tensor ten i => ProfunctorComonad (GenTambara ten) where
proextract (MkTambara p) = dimap unitr.rightToLeft unitr.leftToRight p proextract (MkTambara p) = dimap unitr.rightToLeft unitr.leftToRight p
produplicate (MkTambara p) = MkTambara $ MkTambara $ dimap assocr assocl p produplicate (MkTambara p) = MkTambara $ MkTambara $ dimap assocr assocl p
export public export
Associative ten => Symmetric ten => Profunctor p => GenStrong ten (GenTambara ten p) where Associative ten => Symmetric ten => Profunctor p => GenStrong ten (GenTambara ten p) where
strongl (MkTambara p) = MkTambara $ dimap assocr assocl p strongl (MkTambara p) = MkTambara $ dimap assocr assocl p
strongr (MkTambara p) = MkTambara $ dimap (assocr . mapFst swap') strongr (MkTambara p) = MkTambara $ dimap (assocr . mapFst swap')
(mapFst swap' . assocl) p (mapFst swap' . assocl) p
export public export
Bifunctor ten => Profunctor p => Functor (GenTambara ten p a) where Bifunctor ten => Profunctor p => Functor (GenTambara ten p a) where
map = rmap map = rmap
@ -186,11 +201,11 @@ TambaraSum : (p : Type -> Type -> Type) -> Type -> Type -> Type
TambaraSum = GenTambara Either TambaraSum = GenTambara Either
export public export
tambara : GenStrong ten p => p :-> q -> p :-> GenTambara ten q tambara : GenStrong ten p => p :-> q -> p :-> GenTambara ten q
tambara @{gs} f x = MkTambara $ f $ strongl @{gs} x tambara @{gs} f x = MkTambara $ f $ strongl @{gs} x
export public export
untambara : Tensor ten i => Profunctor q => p :-> GenTambara ten q -> p :-> q untambara : Tensor ten i => Profunctor q => p :-> GenTambara ten q -> p :-> q
untambara f x = dimap unitr.rightToLeft unitr.leftToRight $ runTambara $ f x untambara f x = dimap unitr.rightToLeft unitr.leftToRight $ runTambara $ f x
@ -207,17 +222,17 @@ data GenPastro : (ten, p : Type -> Type -> Type) -> Type -> Type -> Type where
MkPastro : (y `ten` z -> b) -> p x y -> (a -> x `ten` z) -> GenPastro ten p a b MkPastro : (y `ten` z -> b) -> p x y -> (a -> x `ten` z) -> GenPastro ten p a b
export public export
Profunctor (GenPastro ten p) where Profunctor (GenPastro ten p) where
dimap f g (MkPastro l m r) = MkPastro (g . l) m (r . f) dimap f g (MkPastro l m r) = MkPastro (g . l) m (r . f)
lmap f (MkPastro l m r) = MkPastro l m (r . f) lmap f (MkPastro l m r) = MkPastro l m (r . f)
rmap g (MkPastro l m r) = MkPastro (g . l) m r rmap g (MkPastro l m r) = MkPastro (g . l) m r
export public export
ProfunctorFunctor (GenPastro ten) where ProfunctorFunctor (GenPastro ten) where
promap f (MkPastro l m r) = MkPastro l (f m) r promap f (MkPastro l m r) = MkPastro l (f m) r
export public export
(Tensor ten i, Symmetric ten) => ProfunctorMonad (GenPastro ten) where (Tensor ten i, Symmetric ten) => ProfunctorMonad (GenPastro ten) where
propure x = MkPastro unitr.leftToRight x unitr.rightToLeft propure x = MkPastro unitr.leftToRight x unitr.rightToLeft
projoin (MkPastro {x=x',y=y',z=z'} l' (MkPastro {x,y,z} l m r) r') = MkPastro ll m rr projoin (MkPastro {x=x',y=y',z=z'} l' (MkPastro {x,y,z} l m r) r') = MkPastro ll m rr
@ -228,12 +243,12 @@ export
rr : a -> x `ten` (z' `ten` z) rr : a -> x `ten` (z' `ten` z)
rr = mapSnd swap' . assocr . mapFst r . r' rr = mapSnd swap' . assocr . mapFst r . r'
export public export
ProfunctorAdjunction (GenPastro ten) (GenTambara ten) where ProfunctorAdjunction (GenPastro ten) (GenTambara ten) where
prounit x = MkTambara (MkPastro id x id) prounit x = MkTambara (MkPastro id x id)
procounit (MkPastro l (MkTambara x) r) = dimap r l x procounit (MkPastro l (MkTambara x) r) = dimap r l x
export public export
(Associative ten, Symmetric ten) => GenStrong ten (GenPastro ten p) where (Associative ten, Symmetric ten) => GenStrong ten (GenPastro ten p) where
strongl (MkPastro {x,y,z} l m r) = MkPastro l' m r' strongl (MkPastro {x,y,z} l m r) = MkPastro l' m r'
where where
@ -266,11 +281,11 @@ PastroSum : (p : Type -> Type -> Type) -> Type -> Type -> Type
PastroSum = GenPastro Either PastroSum = GenPastro Either
export public export
pastro : GenStrong ten q => p :-> q -> GenPastro ten p :-> q pastro : GenStrong ten q => p :-> q -> GenPastro ten p :-> q
pastro @{gs} f (MkPastro l m r) = dimap r l (strongl @{gs} (f m)) pastro @{gs} f (MkPastro l m r) = dimap r l (strongl @{gs} (f m))
export public export
unpastro : Tensor ten i => GenPastro ten p :-> q -> p :-> q unpastro : Tensor ten i => GenPastro ten p :-> q -> p :-> q
unpastro f x = f (MkPastro unitr.leftToRight x unitr.rightToLeft) unpastro f x = f (MkPastro unitr.leftToRight x unitr.rightToLeft)

86
Data/Profunctor/Traversing.idr
View file

@ -1,6 +1,6 @@
module Data.Profunctor.Traversing module Data.Profunctor.Traversing
import Control.Monad.Identity import Control.Applicative.Const
import Data.Morphisms import Data.Morphisms
import Data.Tensor import Data.Tensor
import Data.Profunctor import Data.Profunctor
@ -8,6 +8,11 @@ import Data.Profunctor
%default total %default total
------------------------------------------------------------------------------
-- Default implementation machinery
------------------------------------------------------------------------------
[FoldablePair] Foldable (Pair c) where [FoldablePair] Foldable (Pair c) where
foldr op init (_, x) = x `op` init foldr op init (_, x) = x `op` init
foldl op init (_, x) = init `op` x foldl op init (_, x) = init `op` x
@ -16,14 +21,6 @@ import Data.Profunctor
[TraversablePair] Traversable (Pair c) using FoldablePair where [TraversablePair] Traversable (Pair c) using FoldablePair where
traverse f (l, r) = (l,) <$> f r 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 record Bazaar a b t where
constructor MkBazaar constructor MkBazaar
@ -48,7 +45,7 @@ Functor (Baz t b) where
sold : Baz t a a -> t sold : Baz t a a -> t
sold m = runIdentity (runBaz m Id) sold m = runBaz @{ApplicativeId} m id
Foldable (Baz t b) where Foldable (Baz t b) where
foldr f i bz = runBaz bz @{appEndo} f i foldr f i bz = runBaz bz @{appEndo} f i
@ -60,6 +57,11 @@ Foldable (Baz t b) where
Traversable (Baz t b) where Traversable (Baz t b) where
traverse f bz = map (\m => MkBaz (runBazaar m)) $ runBaz bz @{Compose} $ \x => sell <$> f x traverse f bz = map (\m => MkBaz (runBazaar m)) $ runBaz bz @{Compose} $ \x => sell <$> f x
public export
wanderDef : Profunctor p => (forall f. Traversable f => p a b -> p (f a) (f b))
-> (forall f. Applicative f => (a -> f b) -> s -> f t) -> p a b -> p s t
wanderDef tr f = dimap (\s => MkBaz $ \afb => f afb s) sold . tr
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
-- Traversing interface -- Traversing interface
@ -81,31 +83,41 @@ interface (Strong p, Choice p) => Traversing p where
traverse' = wander traverse traverse' = wander traverse
wander : (forall f. Applicative f => (a -> f b) -> s -> f t) -> p a b -> p s t 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' wander = wanderDef traverse'
export ------------------------------------------------------------------------------
-- Implementations
------------------------------------------------------------------------------
public export
Traversing Morphism where Traversing Morphism where
traverse' (Mor f) = Mor (map f) 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. ||| A named implementation of `Traversing` for function types.
||| Use this to avoid having to use a type wrapper like `Morphism`. ||| Use this to avoid having to use a type wrapper like `Morphism`.
export public export
[Function] Traversing (\a,b => a -> b) using Strong.Function where [Function] Traversing (\a,b => a -> b) using Strong.Function where
traverse' = map traverse' = map
wander f g = runIdentity . (f $ Id . g) wander f = f @{ApplicativeId}
export public export
Applicative f => Traversing (Kleislimorphism f) where Applicative f => Traversing (Kleislimorphism f) where
traverse' (Kleisli p) = Kleisli (traverse p) traverse' (Kleisli p) = Kleisli (traverse p)
wander f (Kleisli p) = Kleisli (f p) wander f (Kleisli p) = Kleisli (f p)
export public export
Applicative f => Traversing (Star f) where Applicative f => Traversing (Star f) where
traverse' (MkStar p) = MkStar (traverse p) traverse' (MkStar p) = MkStar (traverse p)
wander f (MkStar p) = MkStar (f p) wander f (MkStar p) = MkStar (f p)
public export
Monoid r => Traversing (Forget r) where
traverse' (MkForget k) = MkForget (foldMap k)
wander f (MkForget k) = MkForget (runConst . f (MkConst . k))
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
-- CofreeTraversing -- CofreeTraversing
@ -119,45 +131,45 @@ record CofreeTraversing p a b where
constructor MkCFT constructor MkCFT
runCFT : forall f. Traversable f => p (f a) (f b) runCFT : forall f. Traversable f => p (f a) (f b)
export public export
Profunctor p => Profunctor (CofreeTraversing p) where Profunctor p => Profunctor (CofreeTraversing p) where
lmap f (MkCFT p) = MkCFT (lmap (map f) p) lmap f (MkCFT p) = MkCFT (lmap (map f) p)
rmap g (MkCFT p) = MkCFT (rmap (map g) p) rmap g (MkCFT p) = MkCFT (rmap (map g) p)
dimap f g (MkCFT p) = MkCFT (dimap (map f) (map g) p) dimap f g (MkCFT p) = MkCFT (dimap (map f) (map g) p)
export public export
Profunctor p => GenStrong Pair (CofreeTraversing p) where Profunctor p => GenStrong Pair (CofreeTraversing p) where
strongr (MkCFT p) = MkCFT (p @{Compose @{%search} @{TraversablePair}}) strongr (MkCFT p) = MkCFT (p @{Compose @{%search} @{TraversablePair}})
strongl = dimap swap' swap' . strongr {p=CofreeTraversing p} strongl = dimap swap' swap' . strongr {p=CofreeTraversing p}
export public export
Profunctor p => GenStrong Either (CofreeTraversing p) where Profunctor p => GenStrong Either (CofreeTraversing p) where
strongr (MkCFT p) = MkCFT (p @{Compose {f=Either c}}) strongr (MkCFT p) = MkCFT (p @{Compose {f=Either c}})
strongl = dimap swap' swap' . strongr {p=CofreeTraversing p} strongl = dimap swap' swap' . strongr {p=CofreeTraversing p}
export public export
Profunctor p => Traversing (CofreeTraversing p) where Profunctor p => Traversing (CofreeTraversing p) where
traverse' (MkCFT p) = MkCFT (p @{Compose}) traverse' (MkCFT p) = MkCFT (p @{Compose})
export public export
ProfunctorFunctor CofreeTraversing where ProfunctorFunctor CofreeTraversing where
promap f (MkCFT p) = MkCFT (f p) promap f (MkCFT p) = MkCFT (f p)
export public export
ProfunctorComonad CofreeTraversing where ProfunctorComonad CofreeTraversing where
proextract (MkCFT p) = dimap Id runIdentity $ p @{TraversableIdentity} proextract (MkCFT p) = p @{TraversableId}
produplicate (MkCFT p) = MkCFT $ MkCFT $ p @{Compose} produplicate (MkCFT p) = MkCFT $ MkCFT $ p @{Compose}
export public export
Profunctor p => Functor (CofreeTraversing p a) where Profunctor p => Functor (CofreeTraversing p a) where
map = rmap map = rmap
export public export
cofreeTraversing : Traversing p => p :-> q -> p :-> CofreeTraversing q cofreeTraversing : Traversing p => p :-> q -> p :-> CofreeTraversing q
cofreeTraversing f p = MkCFT $ f $ traverse' p cofreeTraversing f p = MkCFT $ f $ traverse' p
export public export
uncofreeTraversing : Profunctor q => p :-> CofreeTraversing q -> p :-> q uncofreeTraversing : Profunctor q => p :-> CofreeTraversing q -> p :-> q
uncofreeTraversing f p = proextract $ f p uncofreeTraversing f p = proextract $ f p
@ -173,40 +185,40 @@ public export
data FreeTraversing : (p : Type -> Type -> Type) -> Type -> Type -> Type where 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 MkFT : Traversable f => (f y -> b) -> p x y -> (a -> f x) -> FreeTraversing p a b
export public export
Profunctor (FreeTraversing p) where Profunctor (FreeTraversing p) where
lmap f (MkFT l m r) = MkFT l m (r . f) lmap f (MkFT l m r) = MkFT l m (r . f)
rmap f (MkFT l m r) = MkFT (f . l) m r rmap f (MkFT l m r) = MkFT (f . l) m r
dimap f g (MkFT l m r) = MkFT (g . l) m (r . f) dimap f g (MkFT l m r) = MkFT (g . l) m (r . f)
export public export
GenStrong Pair (FreeTraversing p) where GenStrong Pair (FreeTraversing p) where
strongr (MkFT l m r) = MkFT @{Compose @{TraversablePair}} (map l) m (map r) strongr (MkFT l m r) = MkFT @{Compose @{TraversablePair}} (map l) m (map r)
strongl = dimap swap' swap' . strongr {p=FreeTraversing p} strongl = dimap swap' swap' . strongr {p=FreeTraversing p}
export public export
GenStrong Either (FreeTraversing p) where GenStrong Either (FreeTraversing p) where
strongr (MkFT l m r) = MkFT @{Compose {t=Either c}} (map l) m (map r) strongr (MkFT l m r) = MkFT @{Compose {t=Either c}} (map l) m (map r)
strongl = dimap swap' swap' . strongr {p=FreeTraversing p} strongl = dimap swap' swap' . strongr {p=FreeTraversing p}
export public export
Traversing (FreeTraversing p) where Traversing (FreeTraversing p) where
traverse' (MkFT l m r) = MkFT @{Compose} (map l) m (map r) traverse' (MkFT l m r) = MkFT @{Compose} (map l) m (map r)
export public export
ProfunctorFunctor FreeTraversing where ProfunctorFunctor FreeTraversing where
promap f (MkFT l m r) = MkFT l (f m) r promap f (MkFT l m r) = MkFT l (f m) r
export public export
ProfunctorMonad FreeTraversing where 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') projoin (MkFT l' (MkFT l m r) r') = MkFT @{Compose} (l' . map l) m (map r . r')
export public export
freeTraversing : Traversing q => p :-> q -> FreeTraversing p :-> q freeTraversing : Traversing q => p :-> q -> FreeTraversing p :-> q
freeTraversing fn (MkFT {f} l m r) = dimap r l (traverse' {f} (fn m)) freeTraversing fn (MkFT {f} l m r) = dimap r l (traverse' {f} (fn m))
export public export
unfreeTraversing : FreeTraversing p :-> q -> p :-> q unfreeTraversing : FreeTraversing p :-> q -> p :-> q
unfreeTraversing f p = f (MkFT @{TraversableIdentity} runIdentity p Id) unfreeTraversing f p = f (MkFT @{TraversableId} id p id)

156
Data/Profunctor/Types.idr
View file

@ -59,7 +59,7 @@ p :-> q = forall a, b. p a b -> q a b
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
export public export
Profunctor Morphism where Profunctor Morphism where
dimap f g (Mor h) = Mor (g . h . f) dimap f g (Mor h) = Mor (g . h . f)
lmap f (Mor g) = Mor (g . f) lmap f (Mor g) = Mor (g . f)
@ -68,13 +68,13 @@ Profunctor Morphism where
namespace Profunctor namespace Profunctor
||| A named implementation of `Profunctor` for function types. ||| A named implementation of `Profunctor` for function types.
||| Use this to avoid having to use a type wrapper like `Morphism`. ||| Use this to avoid having to use a type wrapper like `Morphism`.
export public export
[Function] Profunctor (\a,b => a -> b) where [Function] Profunctor (\a,b => a -> b) where
dimap f g h = g . h . f dimap f g h = g . h . f
lmap = flip (.) lmap = flip (.)
rmap = (.) rmap = (.)
export public export
Functor f => Profunctor (Kleislimorphism f) where Functor f => Profunctor (Kleislimorphism f) where
dimap f g (Kleisli h) = Kleisli (map g . h . f) dimap f g (Kleisli h) = Kleisli (map g . h . f)
lmap f (Kleisli g) = Kleisli (g . f) lmap f (Kleisli g) = Kleisli (g . f)
@ -82,7 +82,7 @@ Functor f => Profunctor (Kleislimorphism f) where
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
-- Implementations for existing types -- New profunctor types
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
@ -95,27 +95,27 @@ record Star {0 k : Type} (f : k -> Type) a (b : k) where
constructor MkStar constructor MkStar
applyStar : a -> f b applyStar : a -> f b
export public export
Functor f => Functor (Star f a) where Functor f => Functor (Star f a) where
map f (MkStar g) = MkStar (map f . g) map f (MkStar g) = MkStar (map f . g)
export public export
Applicative f => Applicative (Star f a) where Applicative f => Applicative (Star f a) where
pure = MkStar . const . pure pure = MkStar . const . pure
MkStar f <*> MkStar g = MkStar (\x => f x <*> g x) MkStar f <*> MkStar g = MkStar (\x => f x <*> g x)
export public export
Monad f => Monad (Star f a) where Monad f => Monad (Star f a) where
MkStar f >>= g = MkStar $ \x => do MkStar f >>= g = MkStar $ \x => do
a <- f x a <- f x
applyStar (g a) x applyStar (g a) x
export public export
Contravariant f => Contravariant (Star f a) where Contravariant f => Contravariant (Star f a) where
contramap f (MkStar g) = MkStar (contramap f . g) contramap f (MkStar g) = MkStar (contramap f . g)
export public export
Functor f => Profunctor (Star f) where Functor f => Profunctor (Star f) where
dimap f g (MkStar h) = MkStar (map g . h . f) dimap f g (MkStar h) = MkStar (map g . h . f)
lmap f (MkStar g) = MkStar (g . f) lmap f (MkStar g) = MkStar (g . f)
@ -128,20 +128,20 @@ record Costar {0 k : Type} (f : k -> Type) (a : k) b where
constructor MkCostar constructor MkCostar
applyCostar : f a -> b applyCostar : f a -> b
export public export
Functor (Costar f a) where Functor (Costar f a) where
map f (MkCostar g) = MkCostar (f . g) map f (MkCostar g) = MkCostar (f . g)
export public export
Applicative (Costar f a) where Applicative (Costar f a) where
pure = MkCostar . const pure = MkCostar . const
MkCostar f <*> MkCostar g = MkCostar (\x => f x (g x)) MkCostar f <*> MkCostar g = MkCostar (\x => f x (g x))
export public export
Monad (Costar f a) where Monad (Costar f a) where
MkCostar f >>= g = MkCostar (\x => applyCostar (g (f x)) x) MkCostar f >>= g = MkCostar (\x => applyCostar (g (f x)) x)
export public export
Functor f => Profunctor (Costar f) where Functor f => Profunctor (Costar f) where
dimap f g (MkCostar h) = MkCostar (g . h . map f) dimap f g (MkCostar h) = MkCostar (g . h . map f)
lmap f (MkCostar g) = MkCostar (g . map f) lmap f (MkCostar g) = MkCostar (g . map f)
@ -160,21 +160,21 @@ public export
retag : Tagged a c -> Tagged b c retag : Tagged a c -> Tagged b c
retag (Tag x) = Tag x retag (Tag x) = Tag x
export public export
Functor (Tagged a) where Functor (Tagged a) where
map f (Tag x) = Tag (f x) map f (Tag x) = Tag (f x)
export public export
Applicative (Tagged a) where Applicative (Tagged a) where
pure = Tag pure = Tag
Tag f <*> Tag x = Tag (f x) Tag f <*> Tag x = Tag (f x)
export public export
Monad (Tagged a) where Monad (Tagged a) where
join = runTagged join = runTagged
Tag x >>= f = f x Tag x >>= f = f x
export public export
Foldable (Tagged a) where Foldable (Tagged a) where
foldr f x (Tag y) = f y x foldr f x (Tag y) = f y x
foldl f x (Tag y) = f x y foldl f x (Tag y) = f x y
@ -183,12 +183,130 @@ Foldable (Tagged a) where
toList (Tag x) = [x] toList (Tag x) = [x]
foldMap f (Tag x) = f x foldMap f (Tag x) = f x
export public export
Traversable (Tagged a) where Traversable (Tagged a) where
traverse f (Tag x) = map Tag (f x) traverse f (Tag x) = map Tag (f x)
export public export
Profunctor Tagged where Profunctor Tagged where
dimap _ f (Tag x) = Tag (f x) dimap _ f (Tag x) = Tag (f x)
lmap = const retag lmap = const retag
rmap f (Tag x) = Tag (f x) rmap f (Tag x) = Tag (f x)
||| `Forget r` is equivalent to `Star (Const r)`.
public export
record Forget {0 k : Type} r a (b : k) where
constructor MkForget
runForget : a -> r
public export
reforget : Forget r a b -> Forget r a c
reforget (MkForget k) = MkForget k
public export
Functor (Forget r a) where
map _ = reforget
public export
Contravariant (Forget {k=Type} r a) where
contramap _ = reforget
public export
Monoid r => Applicative (Forget r a) where
pure _ = MkForget (const neutral)
MkForget f <*> MkForget g = MkForget (f <+> g)
public export
Monoid r => Monad (Forget {k=Type} r a) where
join = reforget
(>>=) = reforget .: const
public export
Foldable (Forget r a) where
foldr _ x _ = x
foldl _ x _ = x
null = const True
foldlM _ x _ = pure x
toList _ = []
foldMap _ _ = neutral
public export
Traversable (Forget r a) where
traverse _ = pure . reforget
public export
Profunctor (Forget r) where
dimap f _ (MkForget k) = MkForget (k . f)
lmap f (MkForget k) = MkForget (k . f)
rmap = map
||| `Coforget r` is equivalent to `Costar (Const r)`.
public export
record Coforget {0 k : Type} r (a : k) b where
constructor MkCoforget
runCoforget : r -> b
public export
recoforget : Coforget r a c -> Coforget r b c
recoforget (MkCoforget k) = MkCoforget k
public export
Functor (Coforget r a) where
map f (MkCoforget k) = MkCoforget (f . k)
public export
Bifunctor (Coforget r) where
bimap _ f (MkCoforget k) = MkCoforget (f . k)
mapFst _ = recoforget
mapSnd = map
public export
Applicative (Coforget r a) where
pure = MkCoforget . const
MkCoforget f <*> MkCoforget g = MkCoforget (\r => f r (g r))
public export
Monad (Coforget r a) where
MkCoforget k >>= f = MkCoforget (\r => runCoforget (f $ k r) r)
public export
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

56
Data/Profunctor/Yoneda.idr
View file

@ -20,69 +20,69 @@ record Yoneda p a b where
constructor MkYoneda constructor MkYoneda
runYoneda : forall x, y. (x -> a) -> (b -> y) -> p x y runYoneda : forall x, y. (x -> a) -> (b -> y) -> p x y
export public export
Profunctor (Yoneda p) where Profunctor (Yoneda p) where
lmap f (MkYoneda p) = MkYoneda $ \l,r => p (f . l) r lmap f (MkYoneda p) = MkYoneda $ \l,r => p (f . l) r
rmap f (MkYoneda p) = MkYoneda $ \l,r => p l (r . f) rmap f (MkYoneda p) = MkYoneda $ \l,r => p l (r . f)
dimap f g (MkYoneda p) = MkYoneda $ \l,r => p (f . l) (r . g) dimap f g (MkYoneda p) = MkYoneda $ \l,r => p (f . l) (r . g)
export public export
ProfunctorFunctor Yoneda where ProfunctorFunctor Yoneda where
promap f (MkYoneda p) = MkYoneda $ f .: p promap f (MkYoneda p) = MkYoneda $ f .: p
export public export
ProfunctorMonad Yoneda where ProfunctorMonad Yoneda where
propure p = MkYoneda $ \l,r => dimap l r p propure p = MkYoneda $ \l,r => dimap l r p
projoin (MkYoneda p) = p id id projoin (MkYoneda p) = p id id
export public export
ProfunctorComonad Yoneda where ProfunctorComonad Yoneda where
proextract (MkYoneda p) = p id id proextract (MkYoneda p) = p id id
produplicate p = MkYoneda $ \l,r => dimap l r p produplicate p = MkYoneda $ \l,r => dimap l r p
||| A witness that `Yoneda p` and `p` are equivalent when `p` is a profunctor. ||| A witness that `Yoneda p` and `p` are equivalent when `p` is a profunctor.
export public export
yonedaEqv : Profunctor p => p a b <=> Yoneda p a b yonedaEqv : Profunctor p => p a b <=> Yoneda p a b
yonedaEqv = MkEquivalence propure proextract yonedaEqv = MkEquivalence propure proextract
export public export
yonedaIso : (Profunctor q, Profunctor r) => forall p. Profunctor p => yonedaIso : (Profunctor q, Profunctor r) => forall p. Profunctor p =>
p (q a b) (r a' b') -> p (Yoneda q a b) (Yoneda r a' b') p (q a b) (r a' b') -> p (Yoneda q a b) (Yoneda r a' b')
yonedaIso = dimap proextract propure yonedaIso = dimap proextract propure
export public export
Functor (Yoneda p a) where Functor (Yoneda p a) where
map = rmap map = rmap
export public export
GenStrong ten p => GenStrong ten (Yoneda p) where GenStrong ten p => GenStrong ten (Yoneda p) where
strongl = propure . strongl {ten,p} . proextract strongl = propure . strongl {ten,p} . proextract
strongr = propure . strongr {ten,p} . proextract strongr = propure . strongr {ten,p} . proextract
export public export
GenCostrong ten p => GenCostrong ten (Yoneda p) where GenCostrong ten p => GenCostrong ten (Yoneda p) where
costrongl = propure . costrongl {ten,p} . proextract costrongl = propure . costrongl {ten,p} . proextract
costrongr = propure . costrongr {ten,p} . proextract costrongr = propure . costrongr {ten,p} . proextract
export public export
Closed p => Closed (Yoneda p) where Closed p => Closed (Yoneda p) where
closed = propure . closed . proextract closed = propure . closed . proextract
export public export
Traversing p => Traversing (Yoneda p) where Traversing p => Traversing (Yoneda p) where
traverse' = propure . traverse' . proextract traverse' = propure . traverse' . proextract
wander f = propure . wander f . proextract wander f = propure . wander f . proextract
export public export
Mapping p => Mapping (Yoneda p) where Mapping p => Mapping (Yoneda p) where
map' = propure . map' . proextract map' = propure . map' . proextract
roam f = propure . roam f . proextract roam f = propure . roam f . proextract
export public export
Sieve p f => Sieve (Yoneda p) f where Sieve p f => Sieve (Yoneda p) f where
sieve = sieve . proextract sieve = sieve . proextract
export public export
Cosieve p f => Cosieve (Yoneda p) f where Cosieve p f => Cosieve (Yoneda p) f where
cosieve = cosieve . proextract cosieve = cosieve . proextract
@ -98,68 +98,68 @@ data Coyoneda : (p : Type -> Type -> Type) -> Type -> Type -> Type where
MkCoyoneda : (a -> x) -> (y -> b) -> p x y -> Coyoneda p a b MkCoyoneda : (a -> x) -> (y -> b) -> p x y -> Coyoneda p a b
export public export
Profunctor (Coyoneda p) where Profunctor (Coyoneda p) where
lmap f (MkCoyoneda l r p) = MkCoyoneda (l . f) r p lmap f (MkCoyoneda l r p) = MkCoyoneda (l . f) r p
rmap f (MkCoyoneda l r p) = MkCoyoneda l (f . r) p rmap f (MkCoyoneda l r p) = MkCoyoneda l (f . r) p
dimap f g (MkCoyoneda l r p) = MkCoyoneda (l . f) (g . r) p dimap f g (MkCoyoneda l r p) = MkCoyoneda (l . f) (g . r) p
export public export
ProfunctorFunctor Coyoneda where ProfunctorFunctor Coyoneda where
promap f (MkCoyoneda l r p) = MkCoyoneda l r (f p) promap f (MkCoyoneda l r p) = MkCoyoneda l r (f p)
export public export
ProfunctorMonad Coyoneda where ProfunctorMonad Coyoneda where
propure = MkCoyoneda id id propure = MkCoyoneda id id
projoin (MkCoyoneda l r p) = dimap l r p projoin (MkCoyoneda l r p) = dimap l r p
export public export
ProfunctorComonad Coyoneda where ProfunctorComonad Coyoneda where
proextract (MkCoyoneda l r p) = dimap l r p proextract (MkCoyoneda l r p) = dimap l r p
produplicate = MkCoyoneda id id produplicate = MkCoyoneda id id
||| A witness that `Coyoneda p` and `p` are equivalent when `p` is a profunctor. ||| A witness that `Coyoneda p` and `p` are equivalent when `p` is a profunctor.
export public export
coyonedaEqv : Profunctor p => p a b <=> Coyoneda p a b coyonedaEqv : Profunctor p => p a b <=> Coyoneda p a b
coyonedaEqv = MkEquivalence propure proextract coyonedaEqv = MkEquivalence propure proextract
export public export
coyonedaIso : (Profunctor q, Profunctor r) => forall p. Profunctor p => coyonedaIso : (Profunctor q, Profunctor r) => forall p. Profunctor p =>
p (q a b) (r a' b') -> p (Coyoneda q a b) (Coyoneda r a' b') p (q a b) (r a' b') -> p (Coyoneda q a b) (Coyoneda r a' b')
coyonedaIso = dimap proextract propure coyonedaIso = dimap proextract propure
export public export
Functor (Coyoneda p a) where Functor (Coyoneda p a) where
map = rmap map = rmap
export public export
GenStrong ten p => GenStrong ten (Coyoneda p) where GenStrong ten p => GenStrong ten (Coyoneda p) where
strongl = propure . strongl {ten,p} . proextract strongl = propure . strongl {ten,p} . proextract
strongr = propure . strongr {ten,p} . proextract strongr = propure . strongr {ten,p} . proextract
export public export
GenCostrong ten p => GenCostrong ten (Coyoneda p) where GenCostrong ten p => GenCostrong ten (Coyoneda p) where
costrongl = propure . costrongl {ten,p} . proextract costrongl = propure . costrongl {ten,p} . proextract
costrongr = propure . costrongr {ten,p} . proextract costrongr = propure . costrongr {ten,p} . proextract
export public export
Closed p => Closed (Coyoneda p) where Closed p => Closed (Coyoneda p) where
closed = propure . closed . proextract closed = propure . closed . proextract
export public export
Traversing p => Traversing (Coyoneda p) where Traversing p => Traversing (Coyoneda p) where
traverse' = propure . traverse' . proextract traverse' = propure . traverse' . proextract
wander f = propure . wander f . proextract wander f = propure . wander f . proextract
export public export
Mapping p => Mapping (Coyoneda p) where Mapping p => Mapping (Coyoneda p) where
map' = propure . map' . proextract map' = propure . map' . proextract
roam f = propure . roam f . proextract roam f = propure . roam f . proextract
export public export
Sieve p f => Sieve (Coyoneda p) f where Sieve p f => Sieve (Coyoneda p) f where
sieve = sieve . proextract sieve = sieve . proextract
export public export
Cosieve p f => Cosieve (Coyoneda p) f where Cosieve p f => Cosieve (Coyoneda p) f where
cosieve = cosieve . proextract cosieve = cosieve . proextract

12
Data/Tensor.idr
View file

@ -58,16 +58,16 @@ interface Associative ten => Tensor ten i | ten where
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
export public export
Associative Pair where Associative Pair where
assocl (x,(y,z)) = ((x,y),z) assocl (x,(y,z)) = ((x,y),z)
assocr ((x,y),z) = (x,(y,z)) assocr ((x,y),z) = (x,(y,z))
export public export
Symmetric Pair where Symmetric Pair where
swap' = swap swap' = swap
export public export
Tensor Pair () where Tensor Pair () where
unitl = MkEquivalence snd ((),) unitl = MkEquivalence snd ((),)
unitr = MkEquivalence fst (,()) unitr = MkEquivalence fst (,())
@ -78,7 +78,7 @@ Tensor Pair () where
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
export public export
Associative Either where Associative Either where
assocl (Left x) = Left (Left x) assocl (Left x) = Left (Left x)
assocl (Right (Left x)) = Left (Right x) assocl (Right (Left x)) = Left (Right x)
@ -88,11 +88,11 @@ Associative Either where
assocr (Left (Right x)) = Right (Left x) assocr (Left (Right x)) = Right (Left x)
assocr (Right x) = Right (Right x) assocr (Right x) = Right (Right x)
export public export
Symmetric Either where Symmetric Either where
swap' = either Right Left swap' = either Right Left
export public export
Tensor Either Void where Tensor Either Void where
unitl = MkEquivalence (either absurd id) Right unitl = MkEquivalence (either absurd id) Right
unitr = MkEquivalence (either id absurd) Left unitr = MkEquivalence (either id absurd) Left

4
profunctors.ipkg
View file

@ -1,5 +1,7 @@
package profunctors package profunctors
version = 1.0.0 version = 1.1.2
brief = "Profunctors for Idris2"
authors = "Kiana Sheibani" authors = "Kiana Sheibani"
license = "MIT" license = "MIT"