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 21:36:44 -05:00
parent 8cd11e401d
commit 22da62a6f5
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
1 changed files with 14 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
Data/Profunctor/Closed.idr
View file

@ -1,5 +1,6 @@
module Data.Profunctor.Closed module Data.Profunctor.Closed
import Data.Morphisms
import Data.Profunctor.Types import Data.Profunctor.Types
import Data.Profunctor.Functor import Data.Profunctor.Functor
import Data.Profunctor.Strong import Data.Profunctor.Strong
@ -12,6 +13,19 @@ interface Profunctor p => Closed p where
closed : p a b -> p (x -> a) (x -> b) closed : p a b -> p (x -> a) (x -> b)
export
Closed Morphism where
closed (Mor f) = Mor (f .)
export
[Function] Closed (\a,b => a -> b) using Profunctor.Function where
closed = (.)
export
Functor f => Closed (Costar f) where
closed (MkCostar p) = MkCostar $ \f,x => p (map ($ x) f)
export 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
@ -24,7 +38,6 @@ yon : (s -> a, s -> b) -> s -> (a,b)
yon h s = (fst h s, snd h s) yon h s = (fst h s, snd h s)
-- Closure -- Closure
public export public export