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

Create Data.Profunctor.Mapping

Browse source
This commit is contained in:
Kiana Sheibani 2023-03-06 21:38:42 -05:00
parent b5d5526550
commit 36f5c18f0f
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
1 changed files with 18 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
Data/Profunctor/Mapping.idr Normal file
View file

@ -0,0 +1,18 @@
module Data.Profunctor.Mapping
import Data.Profunctor
import Data.Profunctor.Traversing
%default total
public export
interface (Traversing p, Closed p) => Mapping p where
map' : Functor f => p a b -> p (f a) (f b)
map' = roam map
roam : ((a -> b) -> s -> t) -> p a b -> p s t
roam f = dimap (flip f) ($ id) . map' @{%search} @{functor}
where
functor : Functor (\a => (a -> b) -> t)
functor = MkFunctor (\f => (. (. f)))