Prelude.Interfaces


   0 | module Prelude.Interfaces
   1 | 
   2 | import Builtin
   3 | import Prelude.Basics
   4 | import Prelude.EqOrd
   5 | import Prelude.Num
   6 | 
   7 | %default total
   8 | 
   9 | -------------
  10 | -- ALGEBRA --
  11 | -------------
  12 | 
  13 | ||| Sets equipped with a single binary operation that is associative.  Must
  14 | ||| satisfy the following laws:
  15 | |||
  16 | ||| + Associativity of `<+>`:
  17 | |||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
  18 | public export
  19 | interface Semigroup ty where
  20 |   constructor MkSemigroup
  21 |   (<+>) : ty -> ty -> ty
  22 | 
  23 | ||| Sets equipped with a single binary operation that is associative, along with
  24 | ||| a neutral element for that binary operation.  Must satisfy the following
  25 | ||| laws:
  26 | |||
  27 | ||| + Associativity of `<+>`:
  28 | |||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
  29 | ||| + Neutral for `<+>`:
  30 | |||     forall a, a <+> neutral == a
  31 | |||     forall a, neutral <+> a == a
  32 | public export
  33 | interface Semigroup ty => Monoid ty where
  34 |   constructor MkMonoid
  35 |   neutral : ty
  36 | 
  37 | public export
  38 | Semigroup () where
  39 |   _ <+> _ = ()
  40 | 
  41 | public export
  42 | Monoid () where
  43 |   neutral = ()
  44 | 
  45 | public export
  46 | Semigroup a => Semigroup b => Semigroup (a, b) where
  47 |   (x, y) <+> (v, w) = (x <+> v, y <+> w)
  48 | 
  49 | public export
  50 | Monoid a => Monoid b => Monoid (a, b) where
  51 |   neutral = (neutral, neutral)
  52 | 
  53 | public export
  54 | Semigroup Ordering where
  55 |   LT <+> _ = LT
  56 |   GT <+> _ = GT
  57 |   EQ <+> o =  o
  58 | 
  59 | public export
  60 | Monoid Ordering where
  61 |   neutral = EQ
  62 | 
  63 | public export
  64 | Semigroup b => Semigroup (a -> b) where
  65 |   (f <+> g) x = f x <+> g x
  66 | 
  67 | public export
  68 | Monoid b => Monoid (a -> b) where
  69 |   neutral _ = neutral
  70 | 
  71 | ---------------------------------------------------------
  72 | -- FUNCTOR, BIFUNCTOR, APPLICATIVE, ALTERNATIVE, MONAD --
  73 | ---------------------------------------------------------
  74 | 
  75 | ||| Functors allow a uniform action over a parameterised type.
  76 | ||| @ f a parameterised type
  77 | public export
  78 | interface Functor f where
  79 |   constructor MkFunctor
  80 |   ||| Apply a function across everything of type 'a' in a parameterised type
  81 |   ||| @ f the parameterised type
  82 |   ||| @ func the function to apply
  83 |   map : (func : a -> b) -> f a -> f b
  84 | 
  85 | ||| An infix alias for `map`, applying a function across everything of type 'a'
  86 | ||| in a parameterised type.
  87 | ||| @ f the parameterised type
  88 | ||| @ func the function to apply
  89 | %inline %tcinline public export
  90 | (<$>) : Functor f => (func : a -> b) -> f a -> f b
  91 | (<$>) func x = map func x
  92 | 
  93 | ||| Flipped version of `<$>`, an infix alias for `map`, applying a function across
  94 | ||| everything of type 'a' in a parameterised type.
  95 | ||| @ f the parameterised type
  96 | ||| @ func the function to apply
  97 | %inline %tcinline public export
  98 | (<&>) : Functor f => f a -> (func : a -> b) -> f b
  99 | (<&>) x func = map func x
 100 | 
 101 | ||| Run something for effects, replacing the return value with a given parameter.
 102 | %inline %tcinline public export
 103 | (<$) : Functor f => b -> f a -> f b
 104 | (<$) b = map (const b)
 105 | 
 106 | ||| Flipped version of `<$`.
 107 | %inline %tcinline public export
 108 | ($>) : Functor f => f a -> b -> f b
 109 | ($>) fa b = map (const b) fa
 110 | 
 111 | ||| Run something for effects, throwing away the return value.
 112 | %inline %tcinline public export
 113 | ignore : Functor f => f a -> f ()
 114 | ignore = map (const ())
 115 | 
 116 | namespace Functor
 117 |   ||| Composition of functors is a functor.
 118 |   public export
 119 |   [Compose] (l : Functor f) => (r : Functor g) => Functor (f . g) where
 120 |     map = map . map
 121 | 
 122 | ||| Bifunctors
 123 | ||| @f The action of the Bifunctor on pairs of objects
 124 | ||| A minimal definition includes either `bimap` or both `mapFst` and `mapSnd`.
 125 | public export
 126 | interface Bifunctor f where
 127 |   constructor MkBifunctor
 128 |   ||| The action of the Bifunctor on pairs of morphisms
 129 |   |||
 130 |   ||| ````idris example
 131 |   ||| bimap (\x => x + 1) reverse (1, "hello") == (2, "olleh")
 132 |   ||| ````
 133 |   |||
 134 |   total
 135 |   bimap : (a -> c) -> (b -> d) -> f a b -> f c d
 136 |   bimap f g = mapFst f . mapSnd g
 137 | 
 138 |   ||| The action of the Bifunctor on morphisms pertaining to the first object
 139 |   |||
 140 |   ||| ````idris example
 141 |   ||| mapFst (\x => x + 1) (1, "hello") == (2, "hello")
 142 |   ||| ````
 143 |   |||
 144 |   total
 145 |   mapFst : (a -> c) -> f a b -> f c b
 146 |   mapFst f = bimap f id
 147 | 
 148 |   ||| The action of the Bifunctor on morphisms pertaining to the second object
 149 |   |||
 150 |   ||| ````idris example
 151 |   ||| mapSnd reverse (1, "hello") == (1, "olleh")
 152 |   ||| ````
 153 |   |||
 154 |   total
 155 |   mapSnd : (b -> d) -> f a b -> f a d
 156 |   mapSnd = bimap id
 157 | 
 158 | public export %tcinline
 159 | mapHom : Bifunctor f => (a -> b) -> f a a -> f b b
 160 | mapHom f = bimap f f
 161 | 
 162 | namespace Bifunctor
 163 | 
 164 |   ||| Composition of a bifunctor and a functor is a bifunctor.
 165 |   public export %inline
 166 |   [Compose] (l : Functor f) => (r : Bifunctor g) => Bifunctor (f .: g) where
 167 |     bimap = map .: bimap
 168 |     mapFst = map . mapFst
 169 |     mapSnd = map . mapSnd
 170 | 
 171 | public export
 172 | interface Functor f => Applicative f where
 173 |   constructor MkApplicative
 174 |   pure : a -> f a
 175 |   (<*>) : f (a -> b) -> f a -> f b
 176 | 
 177 | public export %tcinline
 178 | (<*) : Applicative f => f a -> f b -> f a
 179 | a <* b = map const a <*> b
 180 | 
 181 | public export %tcinline
 182 | (*>) : Applicative f => f a -> f b -> f b
 183 | a *> b = map (const id) a <*> b
 184 | 
 185 | %allow_overloads pure
 186 | %allow_overloads (<*)
 187 | %allow_overloads (*>)
 188 | 
 189 | namespace Applicative
 190 |   ||| Composition of applicative functors is an applicative functor.
 191 |   public export
 192 |   [Compose] (l : Applicative f) => (r : Applicative g) => Applicative (f . g)
 193 |     using Functor.Compose where
 194 |       pure = pure . pure
 195 |       fun <*> x = [| fun <*> x |]
 196 | 
 197 | ||| An alternative functor has a notion of disjunction.
 198 | ||| @f is the underlying applicative functor
 199 | ||| We expect (f a, empty, (<|>)) to be a type family of monoids.
 200 | public export
 201 | interface Applicative f => Alternative f where
 202 |   constructor MkAlternative
 203 |   empty : f a
 204 |   (<|>) : f a -> Lazy (f a) -> f a
 205 | 
 206 | ||| Monad
 207 | ||| @m The underlying functor
 208 | ||| A minimal definition includes either `(>>=)` or `join`.
 209 | public export
 210 | interface Applicative m => Monad m where
 211 |   constructor MkMonad
 212 |   ||| Also called `bind`.
 213 |   total
 214 |   (>>=) : m a -> (a -> m b) -> m b
 215 | 
 216 |   ||| Also called `flatten` or mu.
 217 |   total
 218 |   join : m (m a) -> m a
 219 | 
 220 |   -- default implementations
 221 |   (>>=) x f = join (f <$> x)
 222 |   join x = x >>= id
 223 | 
 224 | %allow_overloads (>>=)
 225 | 
 226 | ||| Right-to-left monadic bind, flipped version of `>>=`.
 227 | %inline %tcinline public export
 228 | (=<<) : Monad m => (a -> m b) -> m a -> m b
 229 | (=<<) = flip (>>=)
 230 | 
 231 | ||| Sequencing of effectful composition
 232 | %inline %tcinline public export
 233 | (>>) : Monad m => m () -> Lazy (m b) -> m b
 234 | a >> b = a >>= \_ => b
 235 | 
 236 | ||| Left-to-right Kleisli composition of monads.
 237 | public export %tcinline
 238 | (>=>) : Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
 239 | (>=>) f g = \x => f x >>= g
 240 | 
 241 | ||| Right-to-left Kleisli composition of monads, flipped version of `>=>`.
 242 | public export %tcinline
 243 | (<=<) : Monad m => (b -> m c) -> (a -> m b) -> (a -> m c)
 244 | (<=<) = flip (>=>)
 245 | 
 246 | ||| `guard a` is `pure ()` if `a` is `True` and `empty` if `a` is `False`.
 247 | public export
 248 | guard : Alternative f => Bool -> f ()
 249 | guard x = if x then pure () else empty
 250 | 
 251 | ||| Conditionally execute an applicative expression when the boolean is true.
 252 | public export
 253 | when : Applicative f => Bool -> Lazy (f ()) -> f ()
 254 | when True f = f
 255 | when False f = pure ()
 256 | 
 257 | ||| Execute an applicative expression unless the boolean is true.
 258 | %inline %tcinline public export
 259 | unless : Applicative f => Bool -> Lazy (f ()) -> f ()
 260 | unless = when . not
 261 | 
 262 | ---------------------------
 263 | -- FOLDABLE, TRAVERSABLE --
 264 | ---------------------------
 265 | 
 266 | ||| The `Foldable` interface describes how you can iterate over the elements in
 267 | ||| a parameterised type and combine the elements together, using a provided
 268 | ||| function, into a single result.
 269 | ||| @ t The type of the 'Foldable' parameterised type.
 270 | ||| A minimal definition includes `foldr`
 271 | public export
 272 | interface Foldable t where
 273 |   constructor MkFoldable
 274 |   ||| Successively combine the elements in a parameterised type using the
 275 |   ||| provided function, starting with the element that is in the final position
 276 |   ||| i.e. the right-most position.
 277 |   ||| @ func  The function used to 'fold' an element into the accumulated result
 278 |   ||| @ init  The starting value the results are being combined into
 279 |   ||| @ input The parameterised type
 280 |   foldr : (func : elem -> acc -> acc) -> (init : acc) -> (input : t elem) -> acc
 281 | 
 282 |   ||| The same as `foldr` but begins the folding from the element at the initial
 283 |   ||| position in the data structure i.e. the left-most position.
 284 |   ||| @ func  The function used to 'fold' an element into the accumulated result
 285 |   ||| @ init  The starting value the results are being combined into
 286 |   ||| @ input The parameterised type
 287 |   foldl : (func : acc -> elem -> acc) -> (init : acc) -> (input : t elem) -> acc
 288 |   foldl f z t = foldr (flip (.) . flip f) id t z
 289 | 
 290 |   ||| Test whether the structure is empty.
 291 |   ||| @ acc The accumulator value which is specified to be lazy
 292 |   null : t elem -> Bool
 293 |   null xs = foldr {acc = Lazy Bool} (\ _,_ => False) True xs
 294 | 
 295 |   ||| Similar to `foldl`, but uses a function wrapping its result in a `Monad`.
 296 |   ||| Consequently, the final value is wrapped in the same `Monad`.
 297 |   foldlM : Monad m => (funcM : acc -> elem -> m acc) -> (init : acc) -> (input : t elem) -> m acc
 298 |   foldlM fm a0 = foldl (\ma, b => ma >>= flip fm b) (pure a0)
 299 | 
 300 |   ||| Produce a list of the elements contained in the parametrised type.
 301 |   toList : t elem -> List elem
 302 |   toList = foldr (::) []
 303 | 
 304 |   ||| Maps each element to a value and combine them.
 305 |   ||| For performance reasons, this should wherever
 306 |   ||| be implemented with tail recursion.
 307 |   ||| @ f The function to apply to each element.
 308 |   foldMap : Monoid m => (f : a -> m) -> t a -> m
 309 |   foldMap f = foldr ((<+>) . f) neutral
 310 | 
 311 | ||| Combine each element of a structure into a monoid.
 312 | %inline %tcinline public export
 313 | concat : Monoid a => Foldable t => t a -> a
 314 | concat = foldMap id
 315 | 
 316 | ||| Combine into a monoid the collective results of applying a function to each
 317 | ||| element of a structure.
 318 | %inline %tcinline public export
 319 | concatMap : Monoid m => Foldable t => (a -> m) -> t a -> m
 320 | concatMap = foldMap
 321 | 
 322 | namespace Bool.Lazy
 323 |   namespace Semigroup
 324 |     public export
 325 |     [Any] Semigroup (Lazy Bool) where
 326 |       x <+> y = force x || y
 327 | 
 328 |     public export
 329 |     [All] Semigroup (Lazy Bool) where
 330 |       x <+> y = force x && y
 331 | 
 332 |   namespace Monoid
 333 |     public export
 334 |     [Any] Monoid (Lazy Bool) using Semigroup.Any where
 335 |       neutral = delay False
 336 | 
 337 |     public export
 338 |     [All] Monoid (Lazy Bool) using Semigroup.All where
 339 |       neutral = delay True
 340 | 
 341 | ||| The conjunction of all elements of a structure containing lazy boolean
 342 | ||| values.  `and` short-circuits from left to right, evaluating until either an
 343 | ||| element is `False` or no elements remain.
 344 | public export %tcinline
 345 | and : Foldable t => t (Lazy Bool) -> Bool
 346 | and = force . concat @{All}
 347 | 
 348 | ||| The disjunction of all elements of a structure containing lazy boolean
 349 | ||| values.  `or` short-circuits from left to right, evaluating either until an
 350 | ||| element is `True` or no elements remain.
 351 | public export %tcinline
 352 | or : Foldable t => t (Lazy Bool) -> Bool
 353 | or = force . concat @{Any}
 354 | 
 355 | namespace Bool
 356 |   namespace Semigroup
 357 |     public export
 358 |     [Any] Semigroup Bool where
 359 |       x <+> y = x || delay y
 360 | 
 361 |     public export
 362 |     [All] Semigroup Bool where
 363 |       x <+> y = x && delay y
 364 | 
 365 |   namespace Monoid
 366 |     public export
 367 |     [Any] Monoid Bool using Bool.Semigroup.Any where
 368 |       neutral = False
 369 | 
 370 |     public export
 371 |     [All] Monoid Bool using Bool.Semigroup.All where
 372 |       neutral = True
 373 | 
 374 | ||| The disjunction of the collective results of applying a predicate to all
 375 | ||| elements of a structure.  `any` short-circuits from left to right.
 376 | %inline %tcinline public export
 377 | any : Foldable t => (a -> Bool) -> t a -> Bool
 378 | any = foldMap @{%search} @{Any}
 379 | 
 380 | ||| The conjunction of the collective results of applying a predicate to all
 381 | ||| elements of a structure.  `all` short-circuits from left to right.
 382 | %inline %tcinline public export
 383 | all : Foldable t => (a -> Bool) -> t a -> Bool
 384 | all = foldMap @{%search} @{All}
 385 | 
 386 | namespace Num
 387 |   namespace Semigroup
 388 |     public export
 389 |     [Additive] Num a => Semigroup a where
 390 |       (<+>) = (+)
 391 | 
 392 |     public export
 393 |     [Multiplicative] Num a => Semigroup a where
 394 |       (<+>) = (*)
 395 | 
 396 |   namespace Monoid
 397 |     public export
 398 |     [Additive] Num a => Monoid a using Semigroup.Additive where
 399 |       neutral = 0
 400 | 
 401 |     public export
 402 |     [Multiplicative] Num a => Monoid a using Semigroup.Multiplicative where
 403 |       neutral = 1
 404 | 
 405 | ||| Add together all the elements of a structure.
 406 | public export %tcinline
 407 | sum : Num a => Foldable t => t a -> a
 408 | sum = concat @{Additive}
 409 | 
 410 | ||| Add together all the elements of a structure.
 411 | ||| Same as `sum` but tail recursive.
 412 | export %tcinline
 413 | sum' : Num a => Foldable t => t a -> a
 414 | sum' = sum
 415 | 
 416 | ||| Multiply together all elements of a structure.
 417 | public export %tcinline
 418 | product : Num a => Foldable t => t a -> a
 419 | product = concat @{Multiplicative}
 420 | 
 421 | ||| Multiply together all elements of a structure.
 422 | ||| Same as `product` but tail recursive.
 423 | export %tcinline
 424 | product' : Num a => Foldable t => t a -> a
 425 | product' = product
 426 | 
 427 | ||| Map each element of a structure to a computation, evaluate those
 428 | ||| computations and discard the results.
 429 | public export %tcinline
 430 | traverse_ : Applicative f => Foldable t => (a -> f b) -> t a -> f ()
 431 | traverse_ f = foldr ((*>) . f) (pure ())
 432 | 
 433 | ||| Evaluate each computation in a structure and discard the results.
 434 | public export %tcinline
 435 | sequence_ : Applicative f => Foldable t => t (f a) -> f ()
 436 | sequence_ = foldr (*>) (pure ())
 437 | 
 438 | ||| Like `traverse_` but with the arguments flipped.
 439 | public export %tcinline
 440 | for_ : Applicative f => Foldable t => t a -> (a -> f b) -> f ()
 441 | for_ = flip traverse_
 442 | 
 443 | public export
 444 | [SemigroupApplicative] Applicative f => Semigroup a => Semigroup (f a) where
 445 |   x <+> y = [| x <+> y |]
 446 | 
 447 | public export
 448 | [MonoidApplicative] Applicative f => Monoid a => Monoid (f a) using SemigroupApplicative where
 449 |   neutral = pure neutral
 450 | 
 451 | namespace Lazy
 452 |   public export
 453 |   [SemigroupAlternative] Alternative f => Semigroup (Lazy (f a)) where
 454 |     x <+> y = force x <|> y
 455 | 
 456 |   public export
 457 |   [MonoidAlternative] Alternative f => Monoid (Lazy (f a)) using Lazy.SemigroupAlternative where
 458 |     neutral = delay empty
 459 | 
 460 | public export
 461 | [SemigroupAlternative] Alternative f => Semigroup (f a) where
 462 |   x <+> y = x <|> delay y
 463 | 
 464 | public export
 465 | [MonoidAlternative] Alternative f => Monoid (f a) using Interfaces.SemigroupAlternative where
 466 |   neutral = empty
 467 | 
 468 | ||| Fold using Alternative.
 469 | |||
 470 | ||| If you have a left-biased alternative operator `<|>`, then `choice` performs
 471 | ||| left-biased choice from a list of alternatives, which means that it
 472 | ||| evaluates to the left-most non-`empty` alternative.
 473 | |||
 474 | ||| If the list is empty, or all values in it are `empty`, then it evaluates to
 475 | ||| `empty`.
 476 | |||
 477 | ||| Example:
 478 | |||
 479 | ||| ```
 480 | ||| -- given a parser expression like:
 481 | ||| expr = literal <|> keyword <|> funcall
 482 | |||
 483 | ||| -- choice lets you write this as:
 484 | ||| expr = choice [literal, keyword, funcall]
 485 | ||| ```
 486 | |||
 487 | ||| Note: In Haskell, `choice` is called `asum`.
 488 | %inline %tcinline public export
 489 | choice : Alternative f => Foldable t => t (Lazy (f a)) -> f a
 490 | choice = force . concat @{Lazy.MonoidAlternative}
 491 | 
 492 | ||| A fused version of `choice` and `map`.
 493 | %inline %tcinline public export
 494 | choiceMap : Alternative f => Foldable t => (a -> f b) -> t a -> f b
 495 | choiceMap = foldMap @{%search} @{MonoidAlternative}
 496 | 
 497 | namespace Foldable
 498 |   ||| Composition of foldables is foldable.
 499 |   public export %tcinline
 500 |   [Compose] (l : Foldable t) => (r : Foldable f) => Foldable (t . f) where
 501 |     foldr = foldr . flip . foldr
 502 |     foldl = foldl . foldl
 503 |     null tf = null tf || all null tf
 504 |     foldMap = foldMap . foldMap
 505 | 
 506 | ||| `Bifoldable` identifies foldable structures with two different varieties
 507 | ||| of elements (as opposed to `Foldable`, which has one variety of element).
 508 | ||| Common examples are `Either` and `Pair`.
 509 | ||| A minimal definition includes `bifoldr`
 510 | public export
 511 | interface Bifoldable p where
 512 |   constructor MkBifoldable
 513 |   bifoldr : (a -> acc -> acc) -> (b -> acc -> acc) -> acc -> p a b -> acc
 514 | 
 515 |   bifoldl : (acc -> a -> acc) -> (acc -> b -> acc) -> acc -> p a b -> acc
 516 |   bifoldl f g z t = bifoldr (flip (.) . flip f) (flip (.) . flip g) id t z
 517 | 
 518 |   binull : p a b -> Bool
 519 |   binull t = bifoldr {acc = Lazy Bool} (\ _,_ => False) (\ _,_ => False) True t
 520 | 
 521 | ||| Analogous to `foldMap` but for `Bifoldable` structures
 522 | public export %tcinline
 523 | bifoldMap : Monoid acc => Bifoldable p => (a -> acc) -> (b -> acc) -> p a b -> acc
 524 | bifoldMap f g = bifoldr ((<+>) . f) ((<+>) . g) neutral
 525 | 
 526 | ||| Like Bifunctor's `mapFst` but for `Bifoldable` structures
 527 | public export %tcinline
 528 | bifoldMapFst : Monoid acc => Bifoldable p => (a -> acc) -> p a b -> acc
 529 | bifoldMapFst f = bifoldMap f (const neutral)
 530 | 
 531 | namespace Bifoldable
 532 | 
 533 |   ||| Composition of a bifoldable and a foldable is bifoldable.
 534 |   public export %tcinline
 535 |   [Compose] (l : Foldable f) => (r : Bifoldable p) => Bifoldable (f .: p) where
 536 |     bifoldr = foldr .: flip .: bifoldr
 537 |     bifoldl = foldl .: bifoldl
 538 |     binull fp = null fp || all binull fp
 539 | 
 540 | public export
 541 | interface (Functor t, Foldable t) => Traversable t where
 542 |   constructor MkTraversable
 543 |   ||| Map each element of a structure to a computation, evaluate those
 544 |   ||| computations and combine the results.
 545 |   traverse : Applicative f => (a -> f b) -> t a -> f (t b)
 546 | 
 547 | ||| Evaluate each computation in a structure and collect the results.
 548 | public export %tcinline
 549 | sequence : Applicative f => Traversable t => t (f a) -> f (t a)
 550 | sequence = traverse id
 551 | 
 552 | ||| Like `traverse` but with the arguments flipped.
 553 | %inline %tcinline public export
 554 | for : Applicative f => Traversable t => t a -> (a -> f b) -> f (t b)
 555 | for = flip traverse
 556 | 
 557 | public export
 558 | interface (Bifunctor p, Bifoldable p) => Bitraversable p where
 559 |   constructor MkBitraversable
 560 |   ||| Map each element of a structure to a computation, evaluate those
 561 |   ||| computations and combine the results.
 562 |   bitraverse : Applicative f => (a -> f c) -> (b -> f d) -> p a b -> f (p c d)
 563 | 
 564 | ||| Evaluate each computation in a structure and collect the results.
 565 | public export %tcinline
 566 | bisequence : Applicative f => Bitraversable p => p (f a) (f b) -> f (p a b)
 567 | bisequence = bitraverse id id
 568 | 
 569 | ||| Like `bitraverse` but with the arguments flipped.
 570 | public export %tcinline
 571 | bifor :  Applicative f => Bitraversable p
 572 |       => p a b
 573 |       -> (a -> f c)
 574 |       -> (b -> f d)
 575 |       -> f (p c d)
 576 | bifor t f g = bitraverse f g t
 577 | 
 578 | namespace Traversable
 579 |   ||| Composition of traversables is traversable.
 580 |   public export %tcinline
 581 |   [Compose] (l : Traversable t) => (r : Traversable f) => Traversable (t . f)
 582 |     using Foldable.Compose Functor.Compose where
 583 |       traverse = traverse . traverse
 584 | 
 585 | namespace Bitraversable
 586 |   ||| Composition of a bitraversable and a traversable is bitraversable.
 587 |   public export %tcinline
 588 |   [Compose] (l : Traversable t) => (r : Bitraversable p) => Bitraversable (t .: p)
 589 |     using Bifoldable.Compose Bifunctor.Compose where
 590 |       bitraverse = traverse .: bitraverse
 591 | 
 592 | namespace Monad
 593 |   ||| Composition of a traversable monad and a monad is a monad.
 594 |   public export %tcinline
 595 |   [Compose] (l : Monad m) => (r : Monad t) => (tr : Traversable t) => Monad (m . t)
 596 |     using Applicative.Compose where
 597 |       a >>= f = a >>= map join . traverse f
 598 |