
   0 | module Data.Profunctor.Yoneda
   1 | 
   2 | import Data.Profunctor
   3 | import Data.Profunctor.Costrong
   4 | import Data.Profunctor.Traversing
   5 | import Data.Profunctor.Mapping
   6 | import Data.Profunctor.Sieve
   7 | 
   8 | %default total
   9 | 
  10 | 
  11 | ------------------------------------------------------------------------------
  12 | -- Yoneda
  13 | ------------------------------------------------------------------------------
  14 | 
  15 | 
  16 | ||| The cofree profunctor given a data constructor with two type parameters.
  17 | public export
  18 | record Yoneda p a b where
  19 |   constructor MkYoneda
  20 |   runYoneda : forall x, y. (x -> a) -> (b -> y) -> p x y
  21 | 
  22 | public export
  23 | Profunctor (Yoneda p) where
  24 |   lmap f (MkYoneda p) = MkYoneda $ \l,r => p (f . l) r
  25 |   rmap f (MkYoneda p) = MkYoneda $ \l,r => p l (r . f)
  26 |   dimap f g (MkYoneda p) = MkYoneda $ \l,r => p (f . l) (r . g)
  27 | 
  28 | public export
  29 | ProfunctorFunctor Yoneda where
  30 |   promap f (MkYoneda p) = MkYoneda $ f .: p
  31 | 
  32 | public export
  33 | ProfunctorMonad Yoneda where
  34 |   propure p = MkYoneda $ \l,r => dimap l r p
  35 |   projoin (MkYoneda p) = p id id
  36 | 
  37 | public export
  38 | ProfunctorComonad Yoneda where
  39 |   proextract (MkYoneda p) = p id id
  40 |   produplicate p = MkYoneda $ \l,r => dimap l r p
  41 | 
  42 | ||| A witness that `Yoneda p` and `p` are equivalent when `p` is a profunctor.
  43 | public export
  44 | yonedaEqv : Profunctor p => p a b <=> Yoneda p a b
  45 | yonedaEqv = MkEquivalence propure proextract
  46 | 
  47 | public export
  48 | yonedaIso : (Profunctor q, Profunctor r) => forall p. Profunctor p =>
  49 |               p (q a b) (r a' b') -> p (Yoneda q a b) (Yoneda r a' b')
  50 | yonedaIso = dimap proextract propure
  51 | 
  52 | public export
  53 | Functor (Yoneda p a) where
  54 |   map = rmap
  55 | 
  56 | public export
  57 | GenStrong ten p => GenStrong ten (Yoneda p) where
  58 |   strongl = propure . strongl {ten,p} . proextract
  59 |   strongr = propure . strongr {ten,p} . proextract
  60 | 
  61 | public export
  62 | GenCostrong ten p => GenCostrong ten (Yoneda p) where
  63 |   costrongl = propure . costrongl {ten,p} . proextract
  64 |   costrongr = propure . costrongr {ten,p} . proextract
  65 | 
  66 | public export
  67 | Closed p => Closed (Yoneda p) where
  68 |   closed = propure . closed . proextract
  69 | 
  70 | public export
  71 | Traversing p => Traversing (Yoneda p) where
  72 |   traverse' = propure . traverse' . proextract
  73 |   wander f = propure . wander f . proextract
  74 | 
  75 | public export
  76 | Mapping p => Mapping (Yoneda p) where
  77 |   map' = propure . map' . proextract
  78 |   roam f = propure . roam f . proextract
  79 | 
  80 | public export
  81 | Sieve p f => Sieve (Yoneda p) f where
  82 |   sieve = sieve . proextract
  83 | 
  84 | public export
  85 | Cosieve p f => Cosieve (Yoneda p) f where
  86 |   cosieve = cosieve . proextract
  87 | 
  88 | 
  89 | ------------------------------------------------------------------------------
  90 | -- Coyoneda
  91 | ------------------------------------------------------------------------------
  92 | 
  93 | 
  94 | ||| The free profunctor given a data constructor with two type parameters.
  95 | public export
  96 | data Coyoneda : (p : Type -> Type -> Type) -> Type -> Type -> Type where
  97 |   MkCoyoneda : (a -> x) -> (y -> b) -> p x y -> Coyoneda p a b
  98 | 
  99 | 
 100 | public export
 101 | Profunctor (Coyoneda p) where
 102 |   lmap f (MkCoyoneda l r p) = MkCoyoneda (l . f) r p
 103 |   rmap f (MkCoyoneda l r p) = MkCoyoneda l (f . r) p
 104 |   dimap f g (MkCoyoneda l r p) = MkCoyoneda (l . f) (g . r) p
 105 | 
 106 | public export
 107 | ProfunctorFunctor Coyoneda where
 108 |   promap f (MkCoyoneda l r p) = MkCoyoneda l r (f p)
 109 | 
 110 | public export
 111 | ProfunctorMonad Coyoneda where
 112 |   propure = MkCoyoneda id id
 113 |   projoin (MkCoyoneda l r p) = dimap l r p
 114 | 
 115 | public export
 116 | ProfunctorComonad Coyoneda where
 117 |   proextract (MkCoyoneda l r p) = dimap l r p
 118 |   produplicate = MkCoyoneda id id
 119 | 
 120 | ||| A witness that `Coyoneda p` and `p` are equivalent when `p` is a profunctor.
 121 | public export
 122 | coyonedaEqv : Profunctor p => p a b <=> Coyoneda p a b
 123 | coyonedaEqv = MkEquivalence propure proextract
 124 | 
 125 | public export
 126 | coyonedaIso : (Profunctor q, Profunctor r) => forall p. Profunctor p =>
 127 |               p (q a b) (r a' b') -> p (Coyoneda q a b) (Coyoneda r a' b')
 128 | coyonedaIso = dimap proextract propure
 129 | 
 130 | public export
 131 | Functor (Coyoneda p a) where
 132 |   map = rmap
 133 | 
 134 | public export
 135 | GenStrong ten p => GenStrong ten (Coyoneda p) where
 136 |   strongl = propure . strongl {ten,p} . proextract
 137 |   strongr = propure . strongr {ten,p} . proextract
 138 | 
 139 | public export
 140 | GenCostrong ten p => GenCostrong ten (Coyoneda p) where
 141 |   costrongl = propure . costrongl {ten,p} . proextract
 142 |   costrongr = propure . costrongr {ten,p} . proextract
 143 | 
 144 | public export
 145 | Closed p => Closed (Coyoneda p) where
 146 |   closed = propure . closed . proextract
 147 | 
 148 | public export
 149 | Traversing p => Traversing (Coyoneda p) where
 150 |   traverse' = propure . traverse' . proextract
 151 |   wander f = propure . wander f . proextract
 152 | 
 153 | public export
 154 | Mapping p => Mapping (Coyoneda p) where
 155 |   map' = propure . map' . proextract
 156 |   roam f = propure . roam f . proextract
 157 | 
 158 | public export
 159 | Sieve p f => Sieve (Coyoneda p) f where
 160 |   sieve = sieve . proextract
 161 | 
 162 | public export
 163 | Cosieve p f => Cosieve (Coyoneda p) f where
 164 |   cosieve = cosieve . proextract
 165 |