
   0 | ||| This module contains the Profunctor interface itself, along with a few
   1 | ||| examples of profunctors.
   2 | module Data.Profunctor.Types
   3 | 
   4 | import Data.Contravariant
   5 | import Data.Morphisms
   6 | 
   7 | %default total
   8 | 
   9 | 
  10 | ------------------------------------------------------------------------------
  11 | -- Profunctor interface
  12 | ------------------------------------------------------------------------------
  13 | 
  14 | 
  15 | ||| An interface for (self-enriched) profunctors `Idr -/-> Idr`.
  16 | |||
  17 | ||| Formally, a profunctor is a binary functor that is contravariant in its
  18 | ||| first argument and covariant in its second. A common example of a profunctor
  19 | ||| is the (non-dependent) function type.
  20 | |||
  21 | ||| Implementations can be defined by specifying either `dimap` or both `lmap`
  22 | ||| and `rmap`.
  23 | |||
  24 | ||| Laws:
  25 | ||| * `dimap id id = id`
  26 | ||| * `dimap (f . g) (h . i) = dimap g h . dimap f i`
  27 | public export
  28 | interface Profunctor p where
  29 | 
  30 |   ||| Map over both parameters of a profunctor at the same time, with the
  31 |   ||| left function argument mapping contravariantly.
  32 |   dimap : (a -> b) -> (c -> d) -> p b c -> p a d
  33 |   dimap f g = lmap f . rmap g
  34 | 
  35 |   ||| Map contravariantly over the first parameter of a profunctor.
  36 |   lmap : (a -> b) -> p b c -> p a c
  37 |   lmap f = dimap f id
  38 | 
  39 |   ||| Map covariantly over the second parameter of a profunctor.
  40 |   rmap : (b -> c) -> p a b -> p a c
  41 |   rmap = dimap id
  42 | 
  43 | 
  44 | infix 0 :->
  45 | ||| A transformation between profunctors that preserves their type parameters.
  46 | |||
  47 | ||| Formally, this is a natural transformation of functors `Idrᵒᵖ * Idr => Idr`.
  48 | |||
  49 | ||| If the transformation is `tr`, then we have the following law:
  50 | ||| * `tr . dimap f g = dimap f g . tr`
  51 | public export
  52 | 0 (:->) : (p, q : k -> k' -> Type) -> Type
  53 | p :-> q = forall a, b. p a b -> q a b
  54 | 
  55 | 
  56 | ------------------------------------------------------------------------------
  57 | -- Implementations for existing types
  58 | ------------------------------------------------------------------------------
  59 | 
  60 | 
  61 | public export
  62 | Profunctor Morphism where
  63 |   dimap f g (Mor h) = Mor (g . h . f)
  64 |   lmap f (Mor g) = Mor (g . f)
  65 |   rmap = map
  66 | 
  67 | namespace Profunctor
  68 |   ||| A named implementation of `Profunctor` for function types.
  69 |   ||| Use this to avoid having to use a type wrapper like `Morphism`.
  70 |   public export
  71 |   [Function] Profunctor (\a,b => a -> b) where
  72 |     dimap f g h = g . h . f
  73 |     lmap = flip (.)
  74 |     rmap = (.)
  75 | 
  76 | public export
  77 | Functor f => Profunctor (Kleislimorphism f) where
  78 |   dimap f g (Kleisli h) = Kleisli (map g . h . f)
  79 |   lmap f (Kleisli g) = Kleisli (g . f)
  80 |   rmap = map
  81 | 
  82 | 
  83 | ------------------------------------------------------------------------------
  84 | -- New profunctor types
  85 | ------------------------------------------------------------------------------
  86 | 
  87 | 
  88 | ||| Lift a functor into a profunctor in the return type.
  89 | |||
  90 | ||| This type is equivalent to `Kleislimorphism` except for the polymorphic type
  91 | ||| of `b`.
  92 | public export
  93 | record Star {0 k : Type} (f : k -> Type) a (b : k) where
  94 |   constructor MkStar
  95 |   applyStar : a -> f b
  96 | 
  97 | public export
  98 | Functor f => Functor (Star f a) where
  99 |   map f (MkStar g) = MkStar (map f . g)
 100 | 
 101 | public export
 102 | Applicative f => Applicative (Star f a) where
 103 |   pure = MkStar . const . pure
 104 |   MkStar f <*> MkStar g = MkStar (\x => f x <*> g x)
 105 | 
 106 | public export
 107 | Monad f => Monad (Star f a) where
 108 |   MkStar f >>= g = MkStar $ \x => do
 109 |     a <- f x
 110 |     applyStar (g a) x
 111 | 
 112 | public export
 113 | Contravariant f => Contravariant (Star f a) where
 114 |   contramap f (MkStar g) = MkStar (contramap f . g)
 115 | 
 116 | 
 117 | public export
 118 | Functor f => Profunctor (Star f) where
 119 |   dimap f g (MkStar h) = MkStar (map g . h . f)
 120 |   lmap f (MkStar g) = MkStar (g . f)
 121 |   rmap f (MkStar g) = MkStar (map f . g)
 122 | 
 123 | 
 124 | ||| Lift a functor into a profunctor in the argument type.
 125 | public export
 126 | record Costar {0 k : Type} (f : k -> Type) (a : k) b where
 127 |   constructor MkCostar
 128 |   applyCostar : f a -> b
 129 | 
 130 | public export
 131 | Functor (Costar f a) where
 132 |   map f (MkCostar g) = MkCostar (f . g)
 133 | 
 134 | public export
 135 | Applicative (Costar f a) where
 136 |   pure = MkCostar . const
 137 |   MkCostar f <*> MkCostar g = MkCostar (\x => f x (g x))
 138 | 
 139 | public export
 140 | Monad (Costar f a) where
 141 |   MkCostar f >>= g = MkCostar (\x => applyCostar (g (f x)) x)
 142 | 
 143 | public export
 144 | Functor f => Profunctor (Costar f) where
 145 |   dimap f g (MkCostar h) = MkCostar (g . h . map f)
 146 |   lmap f (MkCostar g) = MkCostar (g . map f)
 147 |   rmap f (MkCostar g) = MkCostar (f . g)
 148 | 
 149 | 
 150 | ||| The profunctor that ignores its argument type.
 151 | ||| Equivalent to `const id` up to isomorphism.
 152 | public export
 153 | record Tagged {0 k : Type} (a : k) b where
 154 |   constructor Tag
 155 |   runTagged : b
 156 | 
 157 | ||| Retag the value with a different type-level parameter.
 158 | public export
 159 | retag : Tagged a c -> Tagged b c
 160 | retag (Tag x) = Tag x
 161 | 
 162 | public export
 163 | Functor (Tagged a) where
 164 |   map f (Tag x) = Tag (f x)
 165 | 
 166 | public export
 167 | Applicative (Tagged a) where
 168 |   pure = Tag
 169 |   Tag f <*> Tag x = Tag (f x)
 170 | 
 171 | public export
 172 | Monad (Tagged a) where
 173 |   join = runTagged
 174 |   Tag x >>= f = f x
 175 | 
 176 | public export
 177 | Foldable (Tagged a) where
 178 |   foldr f x (Tag y) = f y x
 179 |   foldl f x (Tag y) = f x y
 180 |   null = const False
 181 |   foldlM f x (Tag y) = f x y
 182 |   toList (Tag x) = [x]
 183 |   foldMap f (Tag x) = f x
 184 | 
 185 | public export
 186 | Traversable (Tagged a) where
 187 |   traverse f (Tag x) = map Tag (f x)
 188 | 
 189 | public export
 190 | Profunctor Tagged where
 191 |   dimap _ f (Tag x) = Tag (f x)
 192 |   lmap = const retag
 193 |   rmap f (Tag x) = Tag (f x)
 194 | 
 195 | 
 196 | ||| `Forget r` is equivalent to `Star (Const r)`.
 197 | public export
 198 | record Forget {0 k : Type} r a (b : k) where
 199 |   constructor MkForget
 200 |   runForget : a -> r
 201 | 
 202 | public export
 203 | reforget : Forget r a b -> Forget r a c
 204 | reforget (MkForget k) = MkForget k
 205 | 
 206 | public export
 207 | Functor (Forget r a) where
 208 |   map _ = reforget
 209 | 
 210 | public export
 211 | Contravariant (Forget {k=Type} r a) where
 212 |   contramap _ = reforget
 213 | 
 214 | public export
 215 | Monoid r => Applicative (Forget r a) where
 216 |   pure _ = MkForget (const neutral)
 217 |   MkForget f <*> MkForget g = MkForget (f <+> g)
 218 | 
 219 | public export
 220 | Monoid r => Monad (Forget {k=Type} r a) where
 221 |   join = reforget
 222 |   (>>=) = reforget .: const
 223 | 
 224 | public export
 225 | Foldable (Forget r a) where
 226 |   foldr _ x _ = x
 227 |   foldl _ x _ = x
 228 |   null = const True
 229 |   foldlM _ x _ = pure x
 230 |   toList _ = []
 231 |   foldMap _ _ = neutral
 232 | 
 233 | public export
 234 | Traversable (Forget r a) where
 235 |   traverse _ = pure . reforget
 236 | 
 237 | public export
 238 | Profunctor (Forget r) where
 239 |   dimap f _ (MkForget k) = MkForget (k . f)
 240 |   lmap f (MkForget k) = MkForget (k . f)
 241 |   rmap = map
 242 | 
 243 | 
 244 | ||| `Coforget r` is equivalent to `Costar (Const r)`.
 245 | public export
 246 | record Coforget {0 k : Type} r (a : k) b where
 247 |   constructor MkCoforget
 248 |   runCoforget : r -> b
 249 | 
 250 | public export
 251 | recoforget : Coforget r a c -> Coforget r b c
 252 | recoforget (MkCoforget k) = MkCoforget k
 253 | 
 254 | public export
 255 | Functor (Coforget r a) where
 256 |   map f (MkCoforget k) = MkCoforget (f . k)
 257 | 
 258 | public export
 259 | Bifunctor (Coforget r) where
 260 |   bimap _ f (MkCoforget k) = MkCoforget (f . k)
 261 |   mapFst _ = recoforget
 262 |   mapSnd = map
 263 | 
 264 | public export
 265 | Applicative (Coforget r a) where
 266 |   pure = MkCoforget . const
 267 |   MkCoforget f <*> MkCoforget g = MkCoforget (\r => f r (g r))
 268 | 
 269 | public export
 270 | Monad (Coforget r a) where
 271 |   MkCoforget k >>= f = MkCoforget (\r => runCoforget (f $ k r) r)
 272 | 
 273 | public export
 274 | Profunctor (Coforget r) where
 275 |   dimap _ f (MkCoforget k) = MkCoforget (f . k)
 276 |   lmap _ = recoforget
 277 |   rmap = map
 278 | 
 279 | 
 280 | ------------------------------------------------------------------------------
 281 | -- Identity functor
 282 | ------------------------------------------------------------------------------
 283 | 
 284 | -- A few convenience definitions for use in other modules.
 285 | 
 286 | public export
 287 | [FunctorId] Functor Prelude.id where
 288 |   map = id
 289 | 
 290 | public export
 291 | [ApplicativeId] Applicative Prelude.id using FunctorId where
 292 |   pure = id
 293 |   (<*>) = id
 294 | 
 295 | public export
 296 | [MonadId] Monad Prelude.id using ApplicativeId where
 297 |   join = id
 298 |   (>>=) = flip id
 299 | 
 300 | public export
 301 | [FoldableId] Foldable Prelude.id where
 302 |   foldr = flip
 303 |   foldl = id
 304 |   null _ = False
 305 |   foldlM = id
 306 |   toList = pure
 307 |   foldMap = id
 308 | 
 309 | public export
 310 | [TraversableId] Traversable Prelude.id using FunctorId FoldableId where
 311 |   traverse = id
 312 |