Create Data.Profunctor.Representable

This commit is contained in:
Kiana Sheibani 2023-03-07 14:10:36 -05:00
parent 3d350068c5
commit c0de1a7a94
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
2 changed files with 51 additions and 0 deletions

View file

@ -9,6 +9,8 @@ import Data.Profunctor.Sieve
%default total
-- NOTE: This may be better as a type synonym instead of a new type?
public export
record Cayley {0 k1,k2,k3 : Type} f (p : k1 -> k2 -> k3) a b where
constructor MkCayley

View file

@ -0,0 +1,49 @@
module Data.Profunctor.Representable
import Control.Monad.Identity
import Data.Morphisms
import Data.Profunctor
import Data.Profunctor.Costrong
import Data.Profunctor.Sieve
%default total
public export
interface (Sieve p f, Strong p) => Representable p f | p where
tabulate : (a -> f b) -> p a b
export
Representable Morphism Identity where
tabulate f = Mor (runIdentity . f)
export
[Function] Representable (\a,b => a -> b) Identity
using Sieve.Function Strong.Function where
tabulate = (runIdentity .)
export
Functor f => Representable (Kleislimorphism f) f where
tabulate = Kleisli
export
Functor f => Representable (Star f) f where
tabulate = MkStar
export
tabulated : (Representable q f, Representable r g) => forall p. Profunctor p =>
p (q a b) (r a' b') -> p (a -> f b) (a' -> g b')
tabulated = dimap tabulate sieve
public export
interface (Cosieve p f, Costrong p) => Corepresentable p f | p where
cotabulate : (f a -> b) -> p a b
export
cotabulated : (Corepresentable q f, Corepresentable r g) => forall p. Profunctor p =>
p (q a b) (r a' b') -> p (f a -> b) (g a' -> b')
cotabulated = dimap cotabulate cosieve