diff --git a/Data/Profunctor/Functor.idr b/Data/Profunctor/Functor.idr new file mode 100644 index 0000000..6ae53df --- /dev/null +++ b/Data/Profunctor/Functor.idr @@ -0,0 +1,20 @@ +module Data.Profunctor.Functor + +import Data.Profunctor.Types + +%default total + + +public export +interface ProfunctorFunctor (0 t : (Type -> Type -> Type) -> k -> k' -> Type) where + promap : Profunctor p => p :-> q -> t p :-> t q + +public export +interface ProfunctorFunctor t => ProfunctorMonad (0 t : (Type -> Type -> Type) -> Type -> Type -> Type) where + propure : Profunctor p => p :-> t p + projoin : Profunctor p => t (t p) :-> t p + +public export +interface ProfunctorFunctor t => ProfunctorComonad (0 t : (Type -> Type -> Type) -> Type -> Type -> Type) where + proextract : Profunctor p => t p :-> p + produplicate : Profunctor p => t p :-> t (t p) diff --git a/Data/Profunctor/Types.idr b/Data/Profunctor/Types.idr index 585231a..60ae243 100644 --- a/Data/Profunctor/Types.idr +++ b/Data/Profunctor/Types.idr @@ -19,6 +19,12 @@ interface Profunctor p where rmap = dimap id +infix 0 :-> +public export +0 (:->) : (p, q : k -> k' -> Type) -> Type +p :-> q = {0 a, b : _} -> p a b -> q a b + + -- Instances for existing types export