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

Add visibility for Environment

Browse source
This commit is contained in:
Kiana Sheibani 2023-03-06 12:43:41 -05:00
parent 9f889aaa94
commit 85b9d77079
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
Data/Profunctor/Closed.idr
View file

@ -78,14 +78,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
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
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
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
@ -95,10 +98,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
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
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
@ -107,12 +112,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
Profunctor p => Functor (Environment p a) where Profunctor p => Functor (Environment p a) where
map = rmap map = rmap
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
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)