idris2-profunctors/Data/Profunctor/Representable.idr

78 lines
2.2 KiB
Idris
Raw Normal View History

2023-03-07 14:10:36 -05:00
module Data.Profunctor.Representable
import Control.Monad.Identity
import Data.Morphisms
import Data.Profunctor
import Data.Profunctor.Costrong
import Data.Profunctor.Sieve
%default total
2023-03-07 22:15:08 -05:00
------------------------------------------------------------------------------
-- Interfaces
------------------------------------------------------------------------------
||| A profunctor `p` is representable if it is isomorphic to `Star f` for some `f`.
2023-03-07 14:10:36 -05:00
public export
interface (Sieve p f, Strong p) => Representable p f | p where
tabulate : (a -> f b) -> p a b
2023-03-07 22:15:08 -05:00
||| A profunctor `p` is representable if it is isomorphic to `Costar f` for some `f`.
public export
interface Cosieve p f => Corepresentable p f | p where
cotabulate : (f a -> b) -> p a b
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
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
------------------------------------------------------------------------------
-- Implementations
------------------------------------------------------------------------------
2023-03-07 14:10:36 -05:00
export
Representable Morphism Identity where
tabulate f = Mor (runIdentity . f)
2023-03-07 22:15:08 -05:00
||| A named implementation of `Representable` for function types.
||| Use this to avoid having to use a type wrapper like `Morphism`.
2023-03-07 14:10:36 -05:00
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
2023-03-08 13:30:55 -05:00
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) Identity using Cosieve.Function where
cotabulate = (. Id)
2023-03-07 14:10:36 -05:00
export
2023-03-07 22:15:08 -05:00
Functor f => Corepresentable (Costar f) f where
cotabulate = MkCostar