Add profunctor functor interfaces
This commit is contained in:
parent
c8dfbb5189
commit
f2392954c2
20
Data/Profunctor/Functor.idr
Normal file
20
Data/Profunctor/Functor.idr
Normal file
|
@ -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)
|
|
@ -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
|
||||
|
|
Loading…
Reference in a new issue