index.html
1 <html> 2 <head> 3 <title>dhall-bhat</title> 4 <meta http-equiv="Content-Type" content="text/html; charset=utf-8"> 5 </head> 6 <body> 7 <h1>dhall-bhat</h1> 8 <h2 style="background-color: #bbb; width: 100%">.</h2> 9 <h2 style="background-color: #bbb; width: 100%">./State</h2> 10 <h3>monad (term)</h3> 11 <dl> 12 <dt>type</dt><dd><pre> 13 ∀(s : Type) 14 → { ap : 15 ∀(a : Type) 16 → ∀(b : Type) 17 → ∀(g : s → { state : s, val : a → b }) 18 → ∀(fa : s → { state : s, val : a }) 19 → ∀(new : s) 20 → { state : s, val : b } 21 , bind : 22 ∀(a : Type) 23 → ∀(b : Type) 24 → ∀(fa : s → { state : s, val : a }) 25 → ∀(k : a → s → { state : s, val : b }) 26 → ∀(new : s) 27 → { state : s, val : b } 28 , map : 29 ∀(a : Type) 30 → ∀(b : Type) 31 → ∀(f : a → b) 32 → ∀(fa : s → { state : s, val : a }) 33 → ∀(new : s) 34 → { state : s, val : b } 35 , pure : 36 ∀(a : Type) → ∀(x : a) → ∀(env : s) → { state : s, val : a } 37 } 38 </pre></dd> 39 </dl> 40 <h3>modify (term)</h3> 41 <dl> 42 <dt>type</dt><dd><pre> 43 ∀(s : Type) → ∀(f : s → s) → ∀(new : s) → { state : s, val : {} } 44 </pre></dd> 45 </dl> 46 <h3>applicative (term)</h3> 47 <dl> 48 <dt>type</dt><dd><pre> 49 ∀(s : Type) 50 → { ap : 51 ∀(a : Type) 52 → ∀(b : Type) 53 → ∀(g : s → { state : s, val : a → b }) 54 → ∀(fa : s → { state : s, val : a }) 55 → ∀(new : s) 56 → { state : s, val : b } 57 , map : 58 ∀(a : Type) 59 → ∀(b : Type) 60 → ∀(f : a → b) 61 → ∀(fa : s → { state : s, val : a }) 62 → ∀(new : s) 63 → { state : s, val : b } 64 , pure : 65 ∀(a : Type) → ∀(x : a) → ∀(env : s) → { state : s, val : a } 66 } 67 </pre></dd> 68 </dl> 69 <h3>eval (term)</h3> 70 <dl> 71 <dt>type</dt><dd><pre> 72 ∀(s : Type) 73 → ∀(a : Type) 74 → ∀(state : s → { state : s, val : a }) 75 → ∀(env : s) 76 → a 77 </pre></dd> 78 </dl> 79 <h3>exec (term)</h3> 80 <dl> 81 <dt>type</dt><dd><pre> 82 ∀(s : Type) 83 → ∀(a : Type) 84 → ∀(state : s → { state : s, val : a }) 85 → ∀(env : s) 86 → s 87 </pre></dd> 88 </dl> 89 <h3>Type (type)</h3> 90 <dl> 91 <dt>kind</dt><dd><pre> 92 ∀(s : Type) → ∀(a : Type) → Type 93 </pre></dd> 94 <dt>type</dt><dd><pre> 95 λ(s : Type) → λ(a : Type) → s → { state : s, val : a } 96 </pre></dd> 97 </dl> 98 <h3>get (term)</h3> 99 <dl> 100 <dt>type</dt><dd><pre> 101 ∀(s : Type) → ∀(env : s) → { state : s, val : s } 102 </pre></dd> 103 </dl> 104 <h3>put (term)</h3> 105 <dl> 106 <dt>type</dt><dd><pre> 107 ∀(s : Type) → ∀(new : s) → ∀(env : s) → { state : s, val : {} } 108 </pre></dd> 109 </dl> 110 <h3>withState (term)</h3> 111 <dl> 112 <dt>type</dt><dd><pre> 113 ∀(s : Type) 114 → ∀(a : Type) 115 → ∀(f : s → s) 116 → ∀(state : s → { state : s, val : a }) 117 → ∀(new : s) 118 → { state : s, val : a } 119 </pre></dd> 120 </dl> 121 <h3>gets (term)</h3> 122 <dl> 123 <dt>type</dt><dd><pre> 124 ∀(s : Type) → ∀(a : Type) → ∀(f : s → a) → ∀(new : s) → { state : s, val : a } 125 </pre></dd> 126 </dl> 127 <h3>package.dhall (term)</h3> 128 <dl> 129 <dt>type</dt><dd><pre> 130 ∀(s : Type) 131 → { ap : 132 ∀(a : Type) 133 → ∀(b : Type) 134 → ∀(g : s → { state : s, val : a → b }) 135 → ∀(fa : s → { state : s, val : a }) 136 → ∀(new : s) 137 → { state : s, val : b } 138 , bind : 139 ∀(a : Type) 140 → ∀(b : Type) 141 → ∀(fa : s → { state : s, val : a }) 142 → ∀(k : a → s → { state : s, val : b }) 143 → ∀(new : s) 144 → { state : s, val : b } 145 , eval : 146 ∀(a : Type) → ∀(state : s → { state : s, val : a }) → ∀(env : s) → a 147 , exec : 148 ∀(a : Type) → ∀(state : s → { state : s, val : a }) → ∀(env : s) → s 149 , get : 150 ∀(a : Type) → ∀(env : s) → { state : s, val : s } 151 , map : 152 ∀(a : Type) 153 → ∀(b : Type) 154 → ∀(f : a → b) 155 → ∀(fa : s → { state : s, val : a }) 156 → ∀(new : s) 157 → { state : s, val : b } 158 , modify : 159 ∀(f : s → s) → ∀(new : s) → { state : s, val : {} } 160 , pure : 161 ∀(a : Type) → ∀(x : a) → ∀(env : s) → { state : s, val : a } 162 , put : 163 ∀(new : s) → ∀(env : s) → { state : s, val : {} } 164 , withState : 165 ∀(a : Type) 166 → ∀(f : s → s) 167 → ∀(state : s → { state : s, val : a }) 168 → ∀(new : s) 169 → { state : s, val : a } 170 } 171 </pre></dd> 172 </dl> 173 <h3>functor (term)</h3> 174 <dl> 175 <dt>type</dt><dd><pre> 176 ∀(s : Type) 177 → { map : 178 ∀(a : Type) 179 → ∀(b : Type) 180 → ∀(f : a → b) 181 → ∀(fa : s → { state : s, val : a }) 182 → ∀(new : s) 183 → { state : s, val : b } 184 } 185 </pre></dd> 186 </dl> 187 <h2 style="background-color: #bbb; width: 100%">./Compose</h2> 188 <h3>applicative (term)</h3> 189 <dl> 190 <dt>type</dt><dd><pre> 191 ∀(f : Type → Type) 192 → ∀(g : Type → Type) 193 → ∀ ( fApplicative 194 : { ap : 195 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 196 , map : 197 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 198 , pure : 199 ∀(a : Type) → a → f a 200 } 201 ) 202 → ∀ ( gApplicative 203 : { ap : 204 ∀(a : Type) → ∀(b : Type) → ∀(g : g (a → b)) → ∀(fa : g@1 a) → g@1 b 205 , map : 206 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : g@1 a) → g@1 b 207 , pure : 208 ∀(a : Type) → a → g a 209 } 210 ) 211 → { ap : 212 ∀(a : Type) 213 → ∀(b : Type) 214 → ∀(k : f (g (a → b))) 215 → ∀(fa : f (g a)) 216 → f (g b) 217 , map : 218 ∀(a : Type) → ∀(b : Type) → ∀(k : a → b) → ∀(fa : f (g a)) → f (g b) 219 , pure : 220 ∀(a : Type) → ∀(x : a) → f (g a) 221 } 222 </pre></dd> 223 </dl> 224 <h3>traversable (term)</h3> 225 <dl> 226 <dt>type</dt><dd><pre> 227 ∀(f : Type → Type) 228 → ∀(g : Type → Type) 229 → ∀ ( fTraversable 230 : { fold : 231 ∀(a : Type) 232 → ∀(ts : f a) 233 → ∀(b : Type) 234 → ∀(f : a → b → b) 235 → ∀(z : b) 236 → b 237 , map : 238 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 239 , traverse : 240 ∀(f : Type → Type) 241 → ∀ ( applicative 242 : { ap : 243 ∀(a : Type) 244 → ∀(b : Type) 245 → ∀(g : f (a → b)) 246 → ∀(fa : f a) 247 → f b 248 , map : 249 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 250 , pure : 251 ∀(a : Type) → a → f a 252 } 253 ) 254 → ∀(a : Type) 255 → ∀(b : Type) 256 → (a → f b) 257 → f@1 a 258 → f (f@1 b) 259 } 260 ) 261 → ∀ ( gTraversable 262 : { fold : 263 ∀(a : Type) 264 → ∀(ts : g a) 265 → ∀(b : Type) 266 → ∀(f : a → b → b) 267 → ∀(z : b) 268 → b 269 , map : 270 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : g@1 a) → g@1 b 271 , traverse : 272 ∀(f : Type → Type) 273 → ∀ ( applicative 274 : { ap : 275 ∀(a : Type) 276 → ∀(b : Type) 277 → ∀(g : f (a → b)) 278 → ∀(fa : f a) 279 → f b 280 , map : 281 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 282 , pure : 283 ∀(a : Type) → a → f a 284 } 285 ) 286 → ∀(a : Type) 287 → ∀(b : Type) 288 → (a → f b) 289 → g a 290 → f (g b) 291 } 292 ) 293 → { fold : 294 ∀(a : Type) 295 → ∀(compose : f (g a)) 296 → ∀(b : Type) 297 → ∀(k : a → b → b) 298 → ∀(z : b) 299 → b 300 , map : 301 ∀(a : Type) → ∀(b : Type) → ∀(k : a → b) → ∀(fa : f (g a)) → f (g b) 302 , traverse : 303 ∀(fA : Type → Type) 304 → ∀ ( applicative 305 : { ap : 306 ∀(a : Type) 307 → ∀(b : Type) 308 → ∀(g : fA (a → b)) 309 → ∀(fa : fA a) 310 → fA b 311 , map : 312 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : fA a) → fA b 313 , pure : 314 ∀(a : Type) → a → fA a 315 } 316 ) 317 → ∀(a : Type) 318 → ∀(b : Type) 319 → ∀(k : a → fA b) 320 → f (g a) 321 → fA (f (g b)) 322 } 323 </pre></dd> 324 </dl> 325 <h3>Type (type)</h3> 326 <dl> 327 <dt>kind</dt><dd><pre> 328 ∀(f : Type → Type) → ∀(g : Type → Type) → ∀(a : Type) → Type 329 </pre></dd> 330 <dt>type</dt><dd><pre> 331 λ(f : Type → Type) → λ(g : Type → Type) → λ(a : Type) → f (g a) 332 </pre></dd> 333 </dl> 334 <h3>functor (term)</h3> 335 <dl> 336 <dt>type</dt><dd><pre> 337 ∀(f : Type → Type) 338 → ∀(g : Type → Type) 339 → ∀ ( fFunctor 340 : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b } 341 ) 342 → ∀ ( gFunctor 343 : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : g@1 a) → g@1 b } 344 ) 345 → { map : ∀(a : Type) → ∀(b : Type) → ∀(k : a → b) → ∀(fa : f (g a)) → f (g b) } 346 </pre></dd> 347 </dl> 348 <h3>foldable (term)</h3> 349 <dl> 350 <dt>type</dt><dd><pre> 351 ∀(f : Type → Type) 352 → ∀(g : Type → Type) 353 → ∀ ( fFoldable 354 : { fold : 355 ∀(a : Type) 356 → ∀(ts : f a) 357 → ∀(b : Type) 358 → ∀(f : a → b → b) 359 → ∀(z : b) 360 → b 361 } 362 ) 363 → ∀ ( gFoldable 364 : { fold : 365 ∀(a : Type) 366 → ∀(ts : g a) 367 → ∀(b : Type) 368 → ∀(f : a → b → b) 369 → ∀(z : b) 370 → b 371 } 372 ) 373 → { fold : 374 ∀(a : Type) 375 → ∀(compose : f (g a)) 376 → ∀(b : Type) 377 → ∀(k : a → b → b) 378 → ∀(z : b) 379 → b 380 } 381 </pre></dd> 382 </dl> 383 <h2 style="background-color: #bbb; width: 100%">./Ran</h2> 384 <h3>lift (term)</h3> 385 <dl> 386 <dt>type</dt><dd><pre> 387 ∀(h : Type → Type) 388 → ∀ ( functor 389 : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : h a) → h b } 390 ) 391 → ∀(f : Type → Type) 392 → ∀(g : Type → Type) 393 → ∀(join : ∀(b : Type) → h (f b) → g b) 394 → ∀(a : Type) 395 → ∀(x : h a) 396 → ∀(b : Type) 397 → ∀(k : a → f b) 398 → g b 399 </pre></dd> 400 </dl> 401 <h3>Type (type)</h3> 402 <dl> 403 <dt>kind</dt><dd><pre> 404 ∀(f : Type → Type) → ∀(g : Type → Type) → ∀(a : Type) → Type 405 </pre></dd> 406 <dt>type</dt><dd><pre> 407 λ(f : Type → Type) 408 → λ(g : Type → Type) 409 → λ(a : Type) 410 → ∀(b : Type) → (a → f b) → g b 411 </pre></dd> 412 </dl> 413 <h3>lower (term)</h3> 414 <dl> 415 <dt>type</dt><dd><pre> 416 ∀(f : Type → Type) 417 → ∀(g : Type → Type) 418 → ∀ ( applicative 419 : { ap : 420 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 421 , map : 422 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 423 , pure : 424 ∀(a : Type) → a → f a 425 } 426 ) 427 → ∀(a : Type) 428 → ∀(ran : ∀(b : Type) → (a → f b) → g b) 429 → g a 430 </pre></dd> 431 </dl> 432 <h3>functor (term)</h3> 433 <dl> 434 <dt>type</dt><dd><pre> 435 ∀(f : Type → Type) 436 → ∀(g : Type → Type) 437 → { map : 438 ∀(a : Type) 439 → ∀(b : Type) 440 → ∀(h : a → b) 441 → ∀(ran : ∀(b : Type) → (a → f b) → g b) 442 → ∀(c : Type) 443 → ∀(k : b → f c) 444 → g c 445 } 446 </pre></dd> 447 </dl> 448 <h2 style="background-color: #bbb; width: 100%">./Profunctor</h2> 449 <h3>fromDimap (term)</h3> 450 <dl> 451 <dt>type</dt><dd><pre> 452 ∀(f : Type → Type → Type) 453 → ∀ ( dimap 454 : ∀(a : Type) 455 → ∀(b : Type) 456 → ∀(c : Type) 457 → ∀(d : Type) 458 → (a → b) 459 → (c → d) 460 → f b c 461 → f a d 462 ) 463 → { dimap : 464 ∀(a : Type) 465 → ∀(b : Type) 466 → ∀(c : Type) 467 → ∀(d : Type) 468 → (a → b) 469 → (c → d) 470 → f b c 471 → f a d 472 , lmap : 473 ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → ∀(fn : a → b) → f b c → f a c 474 , rmap : 475 ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (b → c) → f a b → f a c 476 } 477 </pre></dd> 478 </dl> 479 <h3>Type (type)</h3> 480 <dl> 481 <dt>kind</dt><dd><pre> 482 ∀(f : Type → Type → Type) → Type 483 </pre></dd> 484 <dt>type</dt><dd><pre> 485 λ(f : Type → Type → Type) 486 → { dimap : 487 ∀(a : Type) 488 → ∀(b : Type) 489 → ∀(c : Type) 490 → ∀(d : Type) 491 → (a → b) 492 → (c → d) 493 → f b c 494 → f a d 495 , lmap : 496 ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (a → b) → f b c → f a c 497 , rmap : 498 ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (b → c) → f a b → f a c 499 } 500 </pre></dd> 501 </dl> 502 <h2 style="background-color: #bbb; width: 100%">./Semigroup</h2> 503 <h3>Type (type)</h3> 504 <dl> 505 <dt>kind</dt><dd><pre> 506 ∀(m : Type) → Type 507 </pre></dd> 508 <dt>type</dt><dd><pre> 509 λ(m : Type) → { op : ∀(x : m) → ∀(y : m) → m } 510 </pre></dd> 511 </dl> 512 <h2 style="background-color: #bbb; width: 100%">./Bifunctor</h2> 513 <h3>first (term)</h3> 514 <dl> 515 <dt>type</dt><dd><pre> 516 ∀(p : Type → Type → Type) 517 → ∀ ( bifunctor 518 : { bimap : 519 ∀(a : Type) 520 → ∀(b : Type) 521 → ∀(c : Type) 522 → ∀(d : Type) 523 → (a → c) 524 → (b → d) 525 → p a b 526 → p c d 527 } 528 ) 529 → ∀(a : Type) 530 → ∀(b : Type) 531 → ∀(c : Type) 532 → ∀(f : a → c) 533 → p a b 534 → p c b 535 </pre></dd> 536 </dl> 537 <h3>second (term)</h3> 538 <dl> 539 <dt>type</dt><dd><pre> 540 ∀(p : Type → Type → Type) 541 → ∀ ( bifunctor 542 : { bimap : 543 ∀(a : Type) 544 → ∀(b : Type) 545 → ∀(c : Type) 546 → ∀(d : Type) 547 → (a → c) 548 → (b → d) 549 → p a b 550 → p c d 551 } 552 ) 553 → ∀(a : Type) 554 → ∀(b : Type) 555 → ∀(d : Type) 556 → (b → d) 557 → p a b 558 → p a d 559 </pre></dd> 560 </dl> 561 <h3>Type (type)</h3> 562 <dl> 563 <dt>kind</dt><dd><pre> 564 ∀(p : Type → Type → Type) → Type 565 </pre></dd> 566 <dt>type</dt><dd><pre> 567 λ(p : Type → Type → Type) 568 → { bimap : 569 ∀(a : Type) 570 → ∀(b : Type) 571 → ∀(c : Type) 572 → ∀(d : Type) 573 → (a → c) 574 → (b → d) 575 → p a b 576 → p c d 577 } 578 </pre></dd> 579 </dl> 580 <h3>package.dhall (term)</h3> 581 <dl> 582 <dt>type</dt><dd><pre> 583 ∀(p : Type → Type → Type) 584 → ∀ ( bifunctor 585 : { bimap : 586 ∀(a : Type) 587 → ∀(b : Type) 588 → ∀(c : Type) 589 → ∀(d : Type) 590 → (a → c) 591 → (b → d) 592 → p a b 593 → p c d 594 } 595 ) 596 → { bimap : 597 ∀(a : Type) 598 → ∀(b : Type) 599 → ∀(c : Type) 600 → ∀(d : Type) 601 → (a → c) 602 → (b → d) 603 → p a b 604 → p c d 605 , first : 606 ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → ∀(f : a → c) → p a b → p c b 607 , second : 608 ∀(a : Type) → ∀(b : Type) → ∀(d : Type) → (b → d) → p a b → p a d 609 } 610 </pre></dd> 611 </dl> 612 <h2 style="background-color: #bbb; width: 100%">./Transformer</h2> 613 <h3>Type (type)</h3> 614 <dl> 615 <dt>kind</dt><dd><pre> 616 ∀(t : (Type → Type) → Type → Type) → Type 617 </pre></dd> 618 <dt>type</dt><dd><pre> 619 λ(t : (Type → Type) → Type → Type) 620 → { lift : 621 ∀(m : Type → Type) 622 → ∀ ( monad 623 : { ap : 624 ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b 625 , bind : 626 ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b 627 , map : 628 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b 629 , pure : 630 ∀(a : Type) → a → m a 631 } 632 ) 633 → ∀(a : Type) 634 → m a 635 → t m a 636 } 637 </pre></dd> 638 </dl> 639 <h2 style="background-color: #bbb; width: 100%">./Identity</h2> 640 <h3>monad (term)</h3> 641 <dl> 642 <dt>type</dt><dd><pre> 643 { ap : 644 ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → a → b 645 , bind : 646 ∀(a : Type) → ∀(b : Type) → ∀(fa : a) → ∀(k : a → b) → b 647 , map : 648 ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → a → b 649 , pure : 650 ∀(a : Type) → ∀(x : a) → a 651 } 652 </pre></dd> 653 </dl> 654 <h3>applicative (term)</h3> 655 <dl> 656 <dt>type</dt><dd><pre> 657 { ap : 658 ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → a → b 659 , map : 660 ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → a → b 661 , pure : 662 ∀(a : Type) → ∀(x : a) → a 663 } 664 </pre></dd> 665 </dl> 666 <h3>Type (type)</h3> 667 <dl> 668 <dt>kind</dt><dd><pre> 669 ∀(a : Type) → Type 670 </pre></dd> 671 <dt>type</dt><dd><pre> 672 λ(a : Type) → a 673 </pre></dd> 674 </dl> 675 <h3>comonad (term)</h3> 676 <dl> 677 <dt>type</dt><dd><pre> 678 { duplicate : 679 ∀(a : Type) → ∀(x : a) → a 680 , extend : 681 ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → ∀(x : a) → b 682 , extract : 683 ∀(a : Type) → ∀(x : a) → a 684 , map : 685 ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → ∀(x : a) → b 686 } 687 </pre></dd> 688 </dl> 689 <h3>functor (term)</h3> 690 <dl> 691 <dt>type</dt><dd><pre> 692 { map : ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → a → b } 693 </pre></dd> 694 </dl> 695 <h2 style="background-color: #bbb; width: 100%">./StateT</h2> 696 <h3>monad (term)</h3> 697 <dl> 698 <dt>type</dt><dd><pre> 699 ∀(s : Type) 700 → ∀(m : Type → Type) 701 → ∀ ( monad 702 : { ap : 703 ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b 704 , bind : 705 ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b 706 , map : 707 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b 708 , pure : 709 ∀(a : Type) → a → m a 710 } 711 ) 712 → { ap : 713 ∀(a : Type) 714 → ∀(b : Type) 715 → ∀(g : s → m { state : s, val : a → b }) 716 → ∀(fa : s → m { state : s, val : a }) 717 → ∀(new : s) 718 → m { state : s, val : b } 719 , bind : 720 ∀(a : Type) 721 → ∀(b : Type) 722 → ∀(fa : s → m { state : s, val : a }) 723 → ∀(k : a → s → m { state : s, val : b }) 724 → ∀(new : s) 725 → m { state : s, val : b } 726 , map : 727 ∀(a : Type) 728 → ∀(b : Type) 729 → ∀(f : a → b) 730 → ∀(fa : s → m { state : s, val : a }) 731 → ∀(new : s) 732 → m { state : s, val : b } 733 , pure : 734 ∀(a : Type) → ∀(x : a) → ∀(env : s) → m { state : s, val : a } 735 } 736 </pre></dd> 737 </dl> 738 <h3>modify (term)</h3> 739 <dl> 740 <dt>type</dt><dd><pre> 741 ∀(s : Type) 742 → ∀(m : Type → Type) 743 → ∀ ( monad 744 : { ap : 745 ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b 746 , bind : 747 ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b 748 , map : 749 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b 750 , pure : 751 ∀(a : Type) → a → m a 752 } 753 ) 754 → ∀(f : s → s) 755 → ∀(new : s) 756 → m { state : s, val : {} } 757 </pre></dd> 758 </dl> 759 <h3>applicative (term)</h3> 760 <dl> 761 <dt>type</dt><dd><pre> 762 ∀(s : Type) 763 → ∀(m : Type → Type) 764 → ∀ ( monad 765 : { ap : 766 ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b 767 , bind : 768 ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b 769 , map : 770 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b 771 , pure : 772 ∀(a : Type) → a → m a 773 } 774 ) 775 → { ap : 776 ∀(a : Type) 777 → ∀(b : Type) 778 → ∀(g : s → m { state : s, val : a → b }) 779 → ∀(fa : s → m { state : s, val : a }) 780 → ∀(new : s) 781 → m { state : s, val : b } 782 , map : 783 ∀(a : Type) 784 → ∀(b : Type) 785 → ∀(f : a → b) 786 → ∀(fa : s → m { state : s, val : a }) 787 → ∀(new : s) 788 → m { state : s, val : b } 789 , pure : 790 ∀(a : Type) → ∀(x : a) → ∀(env : s) → m { state : s, val : a } 791 } 792 </pre></dd> 793 </dl> 794 <h3>eval (term)</h3> 795 <dl> 796 <dt>type</dt><dd><pre> 797 ∀(s : Type) 798 → ∀(m : Type → Type) 799 → ∀ ( monad 800 : { ap : 801 ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b 802 , bind : 803 ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b 804 , map : 805 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b 806 , pure : 807 ∀(a : Type) → a → m a 808 } 809 ) 810 → ∀(a : Type) 811 → ∀(state : s → m { state : s, val : a }) 812 → ∀(env : s) 813 → m a 814 </pre></dd> 815 </dl> 816 <h3>exec (term)</h3> 817 <dl> 818 <dt>type</dt><dd><pre> 819 ∀(s : Type) 820 → ∀(m : Type → Type) 821 → ∀ ( monad 822 : { ap : 823 ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b 824 , bind : 825 ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b 826 , map : 827 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b 828 , pure : 829 ∀(a : Type) → a → m a 830 } 831 ) 832 → ∀(a : Type) 833 → ∀(state : s → m { state : s, val : a }) 834 → ∀(env : s) 835 → m s 836 </pre></dd> 837 </dl> 838 <h3>Type (type)</h3> 839 <dl> 840 <dt>kind</dt><dd><pre> 841 ∀(s : Type) → ∀(m : Type → Type) → ∀(a : Type) → Type 842 </pre></dd> 843 <dt>type</dt><dd><pre> 844 λ(s : Type) → λ(m : Type → Type) → λ(a : Type) → s → m { state : s, val : a } 845 </pre></dd> 846 </dl> 847 <h3>get (term)</h3> 848 <dl> 849 <dt>type</dt><dd><pre> 850 ∀(s : Type) 851 → ∀(m : Type → Type) 852 → ∀ ( monad 853 : { ap : 854 ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b 855 , bind : 856 ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b 857 , map : 858 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b 859 , pure : 860 ∀(a : Type) → a → m a 861 } 862 ) 863 → ∀(env : s) 864 → m { state : s, val : s } 865 </pre></dd> 866 </dl> 867 <h3>put (term)</h3> 868 <dl> 869 <dt>type</dt><dd><pre> 870 ∀(s : Type) 871 → ∀(m : Type → Type) 872 → ∀ ( monad 873 : { ap : 874 ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b 875 , bind : 876 ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b 877 , map : 878 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b 879 , pure : 880 ∀(a : Type) → a → m a 881 } 882 ) 883 → ∀(new : s) 884 → ∀(env : s) 885 → m { state : s, val : {} } 886 </pre></dd> 887 </dl> 888 <h3>withState (term)</h3> 889 <dl> 890 <dt>type</dt><dd><pre> 891 ∀(s : Type) 892 → ∀(m : Type → Type) 893 → ∀(a : Type) 894 → ∀(f : s → s) 895 → ∀(state : s → m { state : s, val : a }) 896 → ∀(new : s) 897 → m { state : s, val : a } 898 </pre></dd> 899 </dl> 900 <h3>gets (term)</h3> 901 <dl> 902 <dt>type</dt><dd><pre> 903 ∀(s : Type) 904 → ∀(m : Type → Type) 905 → ∀ ( monad 906 : { ap : 907 ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b 908 , bind : 909 ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b 910 , map : 911 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b 912 , pure : 913 ∀(a : Type) → a → m a 914 } 915 ) 916 → ∀(a : Type) 917 → ∀(f : s → a) 918 → ∀(new : s) 919 → m { state : s, val : a } 920 </pre></dd> 921 </dl> 922 <h3>package.dhall (term)</h3> 923 <dl> 924 <dt>type</dt><dd><pre> 925 ∀(s : Type) 926 → ∀(m : Type → Type) 927 → ∀ ( monad 928 : { ap : 929 ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b 930 , bind : 931 ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b 932 , map : 933 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b 934 , pure : 935 ∀(a : Type) → a → m a 936 } 937 ) 938 → { ap : 939 ∀(a : Type) 940 → ∀(b : Type) 941 → ∀(g : s → m { state : s, val : a → b }) 942 → ∀(fa : s → m { state : s, val : a }) 943 → ∀(new : s) 944 → m { state : s, val : b } 945 , bind : 946 ∀(a : Type) 947 → ∀(b : Type) 948 → ∀(fa : s → m { state : s, val : a }) 949 → ∀(k : a → s → m { state : s, val : b }) 950 → ∀(new : s) 951 → m { state : s, val : b } 952 , eval : 953 ∀(a : Type) → ∀(state : s → m { state : s, val : a }) → ∀(env : s) → m a 954 , exec : 955 ∀(a : Type) → ∀(state : s → m { state : s, val : a }) → ∀(env : s) → m s 956 , get : 957 ∀(env : s) → m { state : s, val : s } 958 , gets : 959 ∀(a : Type) → ∀(f : s → a) → ∀(new : s) → m { state : s, val : a } 960 , lift : 961 ∀(a : Type) → ∀(ma : m a) → ∀(env : s) → m { state : s, val : a } 962 , map : 963 ∀(a : Type) 964 → ∀(b : Type) 965 → ∀(f : a → b) 966 → ∀(fa : s → m { state : s, val : a }) 967 → ∀(new : s) 968 → m { state : s, val : b } 969 , modify : 970 ∀(a : Type) → ∀(f : s → s) → ∀(new : s) → m { state : s, val : {} } 971 , pure : 972 ∀(a : Type) → ∀(x : a) → ∀(env : s) → m { state : s, val : a } 973 , put : 974 ∀(a : Type) → ∀(new : s) → ∀(env : s) → m { state : s, val : {} } 975 } 976 </pre></dd> 977 </dl> 978 <h3>functor (term)</h3> 979 <dl> 980 <dt>type</dt><dd><pre> 981 ∀(s : Type) 982 → ∀(m : Type → Type) 983 → ∀ ( functor 984 : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b } 985 ) 986 → { map : 987 ∀(a : Type) 988 → ∀(b : Type) 989 → ∀(f : a → b) 990 → ∀(fa : s → m { state : s, val : a }) 991 → ∀(new : s) 992 → m { state : s, val : b } 993 } 994 </pre></dd> 995 </dl> 996 <h3>transformer (term)</h3> 997 <dl> 998 <dt>type</dt><dd><pre> 999 ∀(s : Type) 1000 → { lift : 1001 ∀(m : Type → Type) 1002 → ∀ ( monad 1003 : { ap : 1004 ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b 1005 , bind : 1006 ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b 1007 , map : 1008 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b 1009 , pure : 1010 ∀(a : Type) → a → m a 1011 } 1012 ) 1013 → ∀(a : Type) 1014 → ∀(ma : m a) 1015 → ∀(env : s) 1016 → m { state : s, val : a } 1017 } 1018 </pre></dd> 1019 </dl> 1020 <h2 style="background-color: #bbb; width: 100%">./Applicative</h2> 1021 <h3>extractFunctor (term)</h3> 1022 <dl> 1023 <dt>type</dt><dd><pre> 1024 ∀(f : Type → Type) 1025 → ∀ ( t 1026 : { ap : 1027 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 1028 , map : 1029 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 1030 , pure : 1031 ∀(a : Type) → a → f a 1032 } 1033 ) 1034 → { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b } 1035 </pre></dd> 1036 </dl> 1037 <h3>liftA2 (term)</h3> 1038 <dl> 1039 <dt>type</dt><dd><pre> 1040 ∀(f : Type → Type) 1041 → ∀ ( app 1042 : { ap : 1043 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 1044 , map : 1045 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 1046 , pure : 1047 ∀(a : Type) → a → f a 1048 } 1049 ) 1050 → ∀(a : Type) 1051 → ∀(b : Type) 1052 → ∀(c : Type) 1053 → ∀(g : a → b → c) 1054 → ∀(fa : f a) 1055 → ∀(fb : f b) 1056 → f c 1057 </pre></dd> 1058 </dl> 1059 <h3>rightApConst (term)</h3> 1060 <dl> 1061 <dt>type</dt><dd><pre> 1062 ∀(f : Type → Type) 1063 → ∀ ( app 1064 : { ap : 1065 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 1066 , map : 1067 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 1068 , pure : 1069 ∀(a : Type) → a → f a 1070 } 1071 ) 1072 → ∀(a : Type) 1073 → ∀(b : Type) 1074 → ∀(fa : f a) 1075 → ∀(fb : f b) 1076 → f b 1077 </pre></dd> 1078 </dl> 1079 <h3>Type (type)</h3> 1080 <dl> 1081 <dt>kind</dt><dd><pre> 1082 ∀(f : Type → Type) → Type 1083 </pre></dd> 1084 <dt>type</dt><dd><pre> 1085 λ(f : Type → Type) 1086 → { ap : 1087 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 1088 , map : 1089 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 1090 , pure : 1091 ∀(a : Type) → a → f a 1092 } 1093 </pre></dd> 1094 </dl> 1095 <h3>leftApConst (term)</h3> 1096 <dl> 1097 <dt>type</dt><dd><pre> 1098 ∀(f : Type → Type) 1099 → ∀ ( app 1100 : { ap : 1101 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 1102 , map : 1103 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 1104 , pure : 1105 ∀(a : Type) → a → f a 1106 } 1107 ) 1108 → ∀(a : Type) 1109 → ∀(b : Type) 1110 → ∀(fa : f a) 1111 → ∀(fb : f b) 1112 → f a 1113 </pre></dd> 1114 </dl> 1115 <h3>package.dhall (term)</h3> 1116 <dl> 1117 <dt>type</dt><dd><pre> 1118 ∀(f : Type → Type) 1119 → ∀ ( applicative 1120 : { ap : 1121 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 1122 , map : 1123 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 1124 , pure : 1125 ∀(a : Type) → a → f a 1126 } 1127 ) 1128 → { ap : 1129 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 1130 , leftApConst : 1131 ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(fb : f b) → f a 1132 , liftA2 : 1133 ∀(a : Type) 1134 → ∀(b : Type) 1135 → ∀(c : Type) 1136 → ∀(g : a → b → c) 1137 → ∀(fa : f a) 1138 → ∀(fb : f b) 1139 → f c 1140 , map : 1141 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 1142 , pure : 1143 ∀(a : Type) → a → f a 1144 , rightApConst : 1145 ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(fb : f b) → f b 1146 } 1147 </pre></dd> 1148 </dl> 1149 <h2 style="background-color: #bbb; width: 100%">./Either</h2> 1150 <h3>partition (term)</h3> 1151 <dl> 1152 <dt>type</dt><dd><pre> 1153 ∀(a : Type) 1154 → ∀(b : Type) 1155 → ∀(eithers : List < Left : a | Right : b >) 1156 → { lefts : List a, rights : List b } 1157 </pre></dd> 1158 </dl> 1159 <h3>monad (term)</h3> 1160 <dl> 1161 <dt>type</dt><dd><pre> 1162 ∀(a : Type) 1163 → { ap : 1164 ∀(a : Type) 1165 → ∀(b : Type) 1166 → ∀(k : < Left : a@1 | Right : a → b >) 1167 → ∀(fa : < Left : a@1 | Right : a >) 1168 → < Left : a@1 | Right : b > 1169 , bind : 1170 ∀(b : Type) 1171 → ∀(c : Type) 1172 → ∀(fa : < Left : a | Right : b >) 1173 → ∀(k : b → < Left : a | Right : c >) 1174 → < Left : a | Right : c > 1175 , map : 1176 ∀(a : Type) 1177 → ∀(b : Type) 1178 → ∀(k : a → b) 1179 → ∀(fa : < Left : a@1 | Right : a >) 1180 → < Left : a@1 | Right : b > 1181 , pure : 1182 ∀(b : Type) → ∀(x : b) → < Left : a | Right : b > 1183 } 1184 </pre></dd> 1185 </dl> 1186 <h3>isLeft (term)</h3> 1187 <dl> 1188 <dt>type</dt><dd><pre> 1189 ∀(a : Type) → ∀(b : Type) → ∀(e : < Left : a | Right : b >) → Bool 1190 </pre></dd> 1191 </dl> 1192 <h3>mapBoth (term)</h3> 1193 <dl> 1194 <dt>type</dt><dd><pre> 1195 ∀(a : Type) 1196 → ∀(b : Type) 1197 → ∀(c : Type) 1198 → ∀(d : Type) 1199 → ∀(f : a → c) 1200 → ∀(g : b → d) 1201 → ∀(e : < Left : a | Right : b >) 1202 → < Left : c | Right : d > 1203 </pre></dd> 1204 </dl> 1205 <h3>bifunctor (term)</h3> 1206 <dl> 1207 <dt>type</dt><dd><pre> 1208 { bimap : 1209 ∀(a : Type) 1210 → ∀(b : Type) 1211 → ∀(c : Type) 1212 → ∀(d : Type) 1213 → ∀(f : a → c) 1214 → ∀(g : b → d) 1215 → ∀(e : < Left : a | Right : b >) 1216 → < Left : c | Right : d > 1217 } 1218 </pre></dd> 1219 </dl> 1220 <h2 style="background-color: #bbb; width: 100%">./Either/applicative</h2> 1221 <h3>parallel (term)</h3> 1222 <dl> 1223 <dt>type</dt><dd><pre> 1224 ∀(a : Type) 1225 → ∀(semi : { op : ∀(x : a) → ∀(y : a) → a }) 1226 → { ap : 1227 ∀(b : Type) 1228 → ∀(c : Type) 1229 → ∀(g : < Left : a | Right : b → c >) 1230 → ∀(fa : < Left : a | Right : b >) 1231 → < Left : a | Right : c > 1232 , map : 1233 ∀(b : Type) 1234 → ∀(c : Type) 1235 → ∀(f : b → c) 1236 → ∀(either : < Left : a | Right : b >) 1237 → < Left : a | Right : c > 1238 , pure : 1239 ∀(b : Type) → ∀(x : b) → < Left : a | Right : b > 1240 } 1241 </pre></dd> 1242 </dl> 1243 <h3>sequential (term)</h3> 1244 <dl> 1245 <dt>type</dt><dd><pre> 1246 ∀(a : Type) 1247 → { ap : 1248 ∀(a : Type) 1249 → ∀(b : Type) 1250 → ∀(k : < Left : a@1 | Right : a → b >) 1251 → ∀(fa : < Left : a@1 | Right : a >) 1252 → < Left : a@1 | Right : b > 1253 , map : 1254 ∀(a : Type) 1255 → ∀(b : Type) 1256 → ∀(k : a → b) 1257 → ∀(fa : < Left : a@1 | Right : a >) 1258 → < Left : a@1 | Right : b > 1259 , pure : 1260 ∀(b : Type) → ∀(x : b) → < Left : a | Right : b > 1261 } 1262 </pre></dd> 1263 </dl> 1264 <h3>lefts (term)</h3> 1265 <dl> 1266 <dt>type</dt><dd><pre> 1267 ∀(a : Type) → ∀(b : Type) → ∀(eithers : List < Left : a | Right : b >) → List a 1268 </pre></dd> 1269 </dl> 1270 <h3>fromLeft (term)</h3> 1271 <dl> 1272 <dt>type</dt><dd><pre> 1273 ∀(a : Type) → ∀(b : Type) → ∀(def : a) → ∀(e : < Left : a | Right : b >) → a 1274 </pre></dd> 1275 </dl> 1276 <h3>traversable (term)</h3> 1277 <dl> 1278 <dt>type</dt><dd><pre> 1279 ∀(a : Type) 1280 → { fold : 1281 ∀(b : Type) 1282 → ∀(either : < Left : a | Right : b >) 1283 → ∀(c : Type) 1284 → ∀(f : b → c → c) 1285 → ∀(z : c) 1286 → c 1287 , map : 1288 ∀(b : Type) 1289 → ∀(c : Type) 1290 → ∀(f : b → c) 1291 → ∀(either : < Left : a | Right : b >) 1292 → < Left : a | Right : c > 1293 , traverse : 1294 ∀(f : Type → Type) 1295 → ∀ ( applicative 1296 : { ap : 1297 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 1298 , map : 1299 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 1300 , pure : 1301 ∀(a : Type) → a → f a 1302 } 1303 ) 1304 → ∀(b : Type) 1305 → ∀(c : Type) 1306 → ∀(g : b → f c) 1307 → ∀(ts : < Left : a | Right : b >) 1308 → f < Left : a | Right : c > 1309 } 1310 </pre></dd> 1311 </dl> 1312 <h3>mapLeft (term)</h3> 1313 <dl> 1314 <dt>type</dt><dd><pre> 1315 ∀(a : Type) 1316 → ∀(b : Type) 1317 → ∀(c : Type) 1318 → ∀(f : a → c) 1319 → ∀(e : < Left : a | Right : b >) 1320 → < Left : c | Right : b > 1321 </pre></dd> 1322 </dl> 1323 <h3>Type (type)</h3> 1324 <dl> 1325 <dt>kind</dt><dd><pre> 1326 ∀(a : Type) → ∀(b : Type) → Type 1327 </pre></dd> 1328 <dt>type</dt><dd><pre> 1329 λ(a : Type) → λ(b : Type) → < Left : a | Right : b > 1330 </pre></dd> 1331 </dl> 1332 <h3>mapRight (term)</h3> 1333 <dl> 1334 <dt>type</dt><dd><pre> 1335 ∀(a : Type) 1336 → ∀(b : Type) 1337 → ∀(d : Type) 1338 → ∀(f : b → d) 1339 → ∀(e : < Left : a | Right : b >) 1340 → < Left : a | Right : d > 1341 </pre></dd> 1342 </dl> 1343 <h3>isRight (term)</h3> 1344 <dl> 1345 <dt>type</dt><dd><pre> 1346 ∀(a : Type) → ∀(b : Type) → ∀(e : < Left : a | Right : b >) → Bool 1347 </pre></dd> 1348 </dl> 1349 <h3>rights (term)</h3> 1350 <dl> 1351 <dt>type</dt><dd><pre> 1352 ∀(a : Type) → ∀(b : Type) → ∀(eithers : List < Left : a | Right : b >) → List b 1353 </pre></dd> 1354 </dl> 1355 <h3>package.dhall (term)</h3> 1356 <dl> 1357 <dt>type</dt><dd><pre> 1358 ∀(a : Type) 1359 → ∀(b : Type) 1360 → { Left : 1361 ∀(Left : a) → < Left : a | Right : b > 1362 , Right : 1363 ∀(Right : b) → < Left : a | Right : b > 1364 , ap : 1365 ∀(a : Type) 1366 → ∀(b : Type) 1367 → ∀(k : < Left : a@1 | Right : a → b >) 1368 → ∀(fa : < Left : a@1 | Right : a >) 1369 → < Left : a@1 | Right : b > 1370 , bimap : 1371 ∀(a : Type) 1372 → ∀(b : Type) 1373 → ∀(c : Type) 1374 → ∀(d : Type) 1375 → ∀(f : a → c) 1376 → ∀(g : b → d) 1377 → ∀(e : < Left : a | Right : b >) 1378 → < Left : c | Right : d > 1379 , bind : 1380 ∀(b : Type) 1381 → ∀(c : Type) 1382 → ∀(fa : < Left : a | Right : b >) 1383 → ∀(k : b → < Left : a | Right : c >) 1384 → < Left : a | Right : c > 1385 , fold : 1386 ∀(b : Type) 1387 → ∀(either : < Left : a | Right : b >) 1388 → ∀(c : Type) 1389 → ∀(f : b → c → c) 1390 → ∀(z : c) 1391 → c 1392 , fromLeft : 1393 ∀(def : a) → ∀(e : < Left : a | Right : b >) → a 1394 , fromRight : 1395 ∀(def : b) → ∀(e : < Left : a | Right : b >) → b 1396 , isLeft : 1397 ∀(e : < Left : a | Right : b >) → Bool 1398 , isRight : 1399 ∀(e : < Left : a | Right : b >) → Bool 1400 , lefts : 1401 ∀(eithers : List < Left : a | Right : b >) → List a 1402 , map : 1403 ∀(b : Type) 1404 → ∀(c : Type) 1405 → ∀(f : b → c) 1406 → ∀(either : < Left : a | Right : b >) 1407 → < Left : a | Right : c > 1408 , mapBoth : 1409 ∀(c : Type) 1410 → ∀(d : Type) 1411 → ∀(f : a → c) 1412 → ∀(g : b → d) 1413 → ∀(e : < Left : a | Right : b >) 1414 → < Left : c | Right : d > 1415 , mapLeft : 1416 ∀(c : Type) 1417 → ∀(f : a → c) 1418 → ∀(e : < Left : a | Right : b >) 1419 → < Left : c | Right : b > 1420 , mapRight : 1421 ∀(d : Type) 1422 → ∀(f : b → d) 1423 → ∀(e : < Left : a | Right : b >) 1424 → < Left : a | Right : d > 1425 , partition : 1426 ∀(eithers : List < Left : a | Right : b >) 1427 → { lefts : List a, rights : List b } 1428 , pure : 1429 ∀(b : Type) → ∀(x : b) → < Left : a | Right : b > 1430 , rights : 1431 ∀(eithers : List < Left : a | Right : b >) → List b 1432 , traverse : 1433 ∀(f : Type → Type) 1434 → ∀ ( applicative 1435 : { ap : 1436 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 1437 , map : 1438 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 1439 , pure : 1440 ∀(a : Type) → a → f a 1441 } 1442 ) 1443 → ∀(b : Type) 1444 → ∀(c : Type) 1445 → ∀(g : b → f c) 1446 → ∀(ts : < Left : a | Right : b >) 1447 → f < Left : a | Right : c > 1448 } 1449 </pre></dd> 1450 </dl> 1451 <h3>functor (term)</h3> 1452 <dl> 1453 <dt>type</dt><dd><pre> 1454 ∀(a : Type) 1455 → { map : 1456 ∀(b : Type) 1457 → ∀(c : Type) 1458 → ∀(f : b → c) 1459 → ∀(either : < Left : a | Right : b >) 1460 → < Left : a | Right : c > 1461 } 1462 </pre></dd> 1463 </dl> 1464 <h3>foldable (term)</h3> 1465 <dl> 1466 <dt>type</dt><dd><pre> 1467 ∀(a : Type) 1468 → { fold : 1469 ∀(b : Type) 1470 → ∀(either : < Left : a | Right : b >) 1471 → ∀(c : Type) 1472 → ∀(f : b → c → c) 1473 → ∀(z : c) 1474 → c 1475 } 1476 </pre></dd> 1477 </dl> 1478 <h3>fold (term)</h3> 1479 <dl> 1480 <dt>type</dt><dd><pre> 1481 ∀(a : Type) 1482 → ∀(b : Type) 1483 → ∀(c : Type) 1484 → ∀(f : a → c) 1485 → ∀(g : b → c) 1486 → ∀(e : < Left : a | Right : b >) 1487 → c 1488 </pre></dd> 1489 </dl> 1490 <h3>fromRight (term)</h3> 1491 <dl> 1492 <dt>type</dt><dd><pre> 1493 ∀(a : Type) → ∀(b : Type) → ∀(def : b) → ∀(e : < Left : a | Right : b >) → b 1494 </pre></dd> 1495 </dl> 1496 <h2 style="background-color: #bbb; width: 100%">./Yoneda</h2> 1497 <h3>monad (term)</h3> 1498 <dl> 1499 <dt>type</dt><dd><pre> 1500 ∀(f : Type → Type) 1501 → ∀ ( monad 1502 : { ap : 1503 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 1504 , bind : 1505 ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(k : a → f b) → f b 1506 , map : 1507 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 1508 , pure : 1509 ∀(a : Type) → a → f a 1510 } 1511 ) 1512 → { ap : 1513 ∀(a : Type) 1514 → ∀(b : Type) 1515 → ∀(m : ∀(b : Type) → ((a → b@1) → b) → f b) 1516 → ∀(n : ∀(b : Type) → (a → b) → f b) 1517 → ∀(c : Type) 1518 → ∀(k : b → c) 1519 → f c 1520 , bind : 1521 ∀(a : Type) 1522 → ∀(b : Type) 1523 → ∀(yoneda : ∀(b : Type) → (a → b) → f b) 1524 → ∀(k : a → ∀(b : Type) → (b@1 → b) → f b) 1525 → ∀(c : Type) 1526 → ∀(l : b → c) 1527 → f c 1528 , map : 1529 ∀(a : Type) 1530 → ∀(b : Type) 1531 → ∀(h : a → b) 1532 → ∀(ran : ∀(b : Type) → (a → b) → f b) 1533 → ∀(c : Type) 1534 → ∀(k : b → c) 1535 → f c 1536 , pure : 1537 ∀(a : Type) → ∀(x : a) → ∀(b : Type) → ∀(f : a → b) → f@1 b 1538 } 1539 </pre></dd> 1540 </dl> 1541 <h3>applicative (term)</h3> 1542 <dl> 1543 <dt>type</dt><dd><pre> 1544 ∀(f : Type → Type) 1545 → ∀ ( applicative 1546 : { ap : 1547 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 1548 , map : 1549 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 1550 , pure : 1551 ∀(a : Type) → a → f a 1552 } 1553 ) 1554 → { ap : 1555 ∀(a : Type) 1556 → ∀(b : Type) 1557 → ∀(m : ∀(b : Type) → ((a → b@1) → b) → f b) 1558 → ∀(n : ∀(b : Type) → (a → b) → f b) 1559 → ∀(c : Type) 1560 → ∀(k : b → c) 1561 → f c 1562 , map : 1563 ∀(a : Type) 1564 → ∀(b : Type) 1565 → ∀(h : a → b) 1566 → ∀(ran : ∀(b : Type) → (a → b) → f b) 1567 → ∀(c : Type) 1568 → ∀(k : b → c) 1569 → f c 1570 , pure : 1571 ∀(a : Type) → ∀(x : a) → ∀(b : Type) → ∀(f : a → b) → f@1 b 1572 } 1573 </pre></dd> 1574 </dl> 1575 <h3>traversable (term)</h3> 1576 <dl> 1577 <dt>type</dt><dd><pre> 1578 ∀(f : Type → Type) 1579 → ∀ ( traversable 1580 : { fold : 1581 ∀(a : Type) 1582 → ∀(ts : f a) 1583 → ∀(b : Type) 1584 → ∀(f : a → b → b) 1585 → ∀(z : b) 1586 → b 1587 , map : 1588 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 1589 , traverse : 1590 ∀(f : Type → Type) 1591 → ∀ ( applicative 1592 : { ap : 1593 ∀(a : Type) 1594 → ∀(b : Type) 1595 → ∀(g : f (a → b)) 1596 → ∀(fa : f a) 1597 → f b 1598 , map : 1599 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 1600 , pure : 1601 ∀(a : Type) → a → f a 1602 } 1603 ) 1604 → ∀(a : Type) 1605 → ∀(b : Type) 1606 → (a → f b) 1607 → f@1 a 1608 → f (f@1 b) 1609 } 1610 ) 1611 → { fold : 1612 ∀(a : Type) 1613 → ∀(yoneda : ∀(b : Type) → (a → b) → f b) 1614 → ∀(b : Type) 1615 → ∀(k : a → b → b) 1616 → ∀(z : b) 1617 → b 1618 , map : 1619 ∀(a : Type) 1620 → ∀(b : Type) 1621 → ∀(h : a → b) 1622 → ∀(ran : ∀(b : Type) → (a → b) → f b) 1623 → ∀(c : Type) 1624 → ∀(k : b → c) 1625 → f c 1626 , traverse : 1627 ∀(g : Type → Type) 1628 → ∀ ( applicative 1629 : { ap : 1630 ∀(a : Type) 1631 → ∀(b : Type) 1632 → ∀(g : g (a → b)) 1633 → ∀(fa : g@1 a) 1634 → g@1 b 1635 , map : 1636 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : g@1 a) → g@1 b 1637 , pure : 1638 ∀(a : Type) → a → g a 1639 } 1640 ) 1641 → ∀(a : Type) 1642 → ∀(b : Type) 1643 → ∀(k : a → g b) 1644 → ∀(yoneda : ∀(b : Type) → (a → b) → f b) 1645 → g (∀(b : Type) → (b@1 → b) → f b) 1646 } 1647 </pre></dd> 1648 </dl> 1649 <h3>lift (term)</h3> 1650 <dl> 1651 <dt>type</dt><dd><pre> 1652 ∀(f : Type → Type) 1653 → ∀ ( functor 1654 : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b } 1655 ) 1656 → ∀(a : Type) 1657 → ∀(x : f a) 1658 → ∀(b : Type) 1659 → ∀(k : a → b) 1660 → f b 1661 </pre></dd> 1662 </dl> 1663 <h3>Type (type)</h3> 1664 <dl> 1665 <dt>kind</dt><dd><pre> 1666 ∀(g : Type → Type) → ∀(a : Type) → Type 1667 </pre></dd> 1668 <dt>type</dt><dd><pre> 1669 λ(g : Type → Type) → λ(a : Type) → ∀(b : Type) → (a → b) → g b 1670 </pre></dd> 1671 </dl> 1672 <h3>lower (term)</h3> 1673 <dl> 1674 <dt>type</dt><dd><pre> 1675 ∀(f : Type → Type) → ∀(a : Type) → ∀(ran : ∀(b : Type) → (a → b) → f b) → f a 1676 </pre></dd> 1677 </dl> 1678 <h3>functor (term)</h3> 1679 <dl> 1680 <dt>type</dt><dd><pre> 1681 ∀(f : Type → Type) 1682 → { map : 1683 ∀(a : Type) 1684 → ∀(b : Type) 1685 → ∀(h : a → b) 1686 → ∀(ran : ∀(b : Type) → (a → b) → f b) 1687 → ∀(c : Type) 1688 → ∀(k : b → c) 1689 → f c 1690 } 1691 </pre></dd> 1692 </dl> 1693 <h3>foldable (term)</h3> 1694 <dl> 1695 <dt>type</dt><dd><pre> 1696 ∀(f : Type → Type) 1697 → ∀ ( foldable 1698 : { fold : 1699 ∀(a : Type) 1700 → ∀(ts : f a) 1701 → ∀(b : Type) 1702 → ∀(f : a → b → b) 1703 → ∀(z : b) 1704 → b 1705 } 1706 ) 1707 → { fold : 1708 ∀(a : Type) 1709 → ∀(yoneda : ∀(b : Type) → (a → b) → f b) 1710 → ∀(b : Type) 1711 → ∀(k : a → b → b) 1712 → ∀(z : b) 1713 → b 1714 } 1715 </pre></dd> 1716 </dl> 1717 <h2 style="background-color: #bbb; width: 100%">./List</h2> 1718 <h3>monad (term)</h3> 1719 <dl> 1720 <dt>type</dt><dd><pre> 1721 { ap : 1722 ∀(a : Type) → ∀(b : Type) → ∀(g : List (a → b)) → ∀(fa : List a) → List b 1723 , bind : 1724 ∀(a : Type) → ∀(b : Type) → ∀(fa : List a) → ∀(k : a → List b) → List b 1725 , map : 1726 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(list : List a) → List b 1727 , pure : 1728 ∀(a : Type) → ∀(x : a) → List a 1729 } 1730 </pre></dd> 1731 </dl> 1732 <h3>applicative (term)</h3> 1733 <dl> 1734 <dt>type</dt><dd><pre> 1735 { ap : 1736 ∀(a : Type) → ∀(b : Type) → ∀(g : List (a → b)) → ∀(fa : List a) → List b 1737 , map : 1738 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(list : List a) → List b 1739 , pure : 1740 ∀(a : Type) → ∀(x : a) → List a 1741 } 1742 </pre></dd> 1743 </dl> 1744 <h3>semigroup (term)</h3> 1745 <dl> 1746 <dt>type</dt><dd><pre> 1747 ∀(a : Type) → { op : ∀(xs : List a) → ∀(ys : List a) → List a } 1748 </pre></dd> 1749 </dl> 1750 <h3>traversable (term)</h3> 1751 <dl> 1752 <dt>type</dt><dd><pre> 1753 { fold : 1754 ∀(a : Type) 1755 → List a 1756 → ∀(list : Type) 1757 → ∀(cons : a → list → list) 1758 → ∀(nil : list) 1759 → list 1760 , map : 1761 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(list : List a) → List b 1762 , traverse : 1763 ∀(f : Type → Type) 1764 → ∀ ( applicative 1765 : { ap : 1766 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 1767 , map : 1768 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 1769 , pure : 1770 ∀(a : Type) → a → f a 1771 } 1772 ) 1773 → ∀(a : Type) 1774 → ∀(b : Type) 1775 → ∀(g : a → f b) 1776 → ∀(ts : List a) 1777 → f (List b) 1778 } 1779 </pre></dd> 1780 </dl> 1781 <h3>monoid (term)</h3> 1782 <dl> 1783 <dt>type</dt><dd><pre> 1784 ∀(a : Type) → { op : ∀(xs : List a) → ∀(ys : List a) → List a, unit : List a } 1785 </pre></dd> 1786 </dl> 1787 <h3>functor (term)</h3> 1788 <dl> 1789 <dt>type</dt><dd><pre> 1790 { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(list : List a) → List b } 1791 </pre></dd> 1792 </dl> 1793 <h3>foldable (term)</h3> 1794 <dl> 1795 <dt>type</dt><dd><pre> 1796 { fold : 1797 ∀(a : Type) 1798 → List a 1799 → ∀(list : Type) 1800 → ∀(cons : a → list → list) 1801 → ∀(nil : list) 1802 → list 1803 } 1804 </pre></dd> 1805 </dl> 1806 <h2 style="background-color: #bbb; width: 100%">./NonEmptyList</h2> 1807 <h3>applicative (term)</h3> 1808 <dl> 1809 <dt>type</dt><dd><pre> 1810 { ap : 1811 ∀(a : Type) 1812 → ∀(b : Type) 1813 → ∀(nelF : { head : a → b, tail : List (a → b) }) 1814 → ∀(nel : { head : a, tail : List a }) 1815 → { head : b, tail : List b } 1816 , map : 1817 ∀(a : Type) 1818 → ∀(b : Type) 1819 → ∀(k : a → b) 1820 → ∀(nel : { head : a, tail : List a }) 1821 → { head : b, tail : List b } 1822 , pure : 1823 ∀(a : Type) → ∀(x : a) → { head : a, tail : List a } 1824 } 1825 </pre></dd> 1826 </dl> 1827 <h3>semigroup (term)</h3> 1828 <dl> 1829 <dt>type</dt><dd><pre> 1830 ∀(a : Type) 1831 → { op : 1832 ∀(x : { head : a, tail : List a }) 1833 → ∀(y : { head : a, tail : List a }) 1834 → { head : a, tail : List a } 1835 } 1836 </pre></dd> 1837 </dl> 1838 <h3>traversable (term)</h3> 1839 <dl> 1840 <dt>type</dt><dd><pre> 1841 { fold : 1842 ∀(a : Type) 1843 → ∀(ts : { head : a, tail : List a }) 1844 → ∀(b : Type) 1845 → ∀(f : a → b → b) 1846 → ∀(z : b) 1847 → b 1848 , map : 1849 ∀(a : Type) 1850 → ∀(b : Type) 1851 → ∀(k : a → b) 1852 → ∀(nel : { head : a, tail : List a }) 1853 → { head : b, tail : List b } 1854 , traverse : 1855 ∀(f : Type → Type) 1856 → ∀ ( applicative 1857 : { ap : 1858 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 1859 , map : 1860 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 1861 , pure : 1862 ∀(a : Type) → a → f a 1863 } 1864 ) 1865 → ∀(a : Type) 1866 → ∀(b : Type) 1867 → ∀(k : a → f b) 1868 → ∀(nel : { head : a, tail : List a }) 1869 → f { head : b, tail : List b } 1870 } 1871 </pre></dd> 1872 </dl> 1873 <h3>Type (type)</h3> 1874 <dl> 1875 <dt>kind</dt><dd><pre> 1876 ∀(a : Type) → Type 1877 </pre></dd> 1878 <dt>type</dt><dd><pre> 1879 λ(a : Type) → { head : a, tail : List a } 1880 </pre></dd> 1881 </dl> 1882 <h3>comonad (term)</h3> 1883 <dl> 1884 <dt>type</dt><dd><pre> 1885 { duplicate : 1886 ∀(a : Type) 1887 → ∀(nel : { head : a, tail : List a }) 1888 → { head : 1889 { head : a, tail : List a } 1890 , tail : 1891 List { head : a, tail : List a } 1892 } 1893 , extend : 1894 ∀(a : Type) 1895 → ∀(b : Type) 1896 → ∀(f : { head : a, tail : List a } → b) 1897 → ∀(nel : { head : a, tail : List a }) 1898 → { head : b, tail : List b } 1899 , extract : 1900 ∀(a : Type) → ∀(nel : { head : a, tail : List a }) → a 1901 , map : 1902 ∀(a : Type) 1903 → ∀(b : Type) 1904 → ∀(f : a → b) 1905 → ∀(nel : { head : a, tail : List a }) 1906 → { head : b, tail : List b } 1907 } 1908 </pre></dd> 1909 </dl> 1910 <h3>functor (term)</h3> 1911 <dl> 1912 <dt>type</dt><dd><pre> 1913 { map : 1914 ∀(a : Type) 1915 → ∀(b : Type) 1916 → ∀(k : a → b) 1917 → ∀(nel : { head : a, tail : List a }) 1918 → { head : b, tail : List b } 1919 } 1920 </pre></dd> 1921 </dl> 1922 <h3>foldable (term)</h3> 1923 <dl> 1924 <dt>type</dt><dd><pre> 1925 { fold : 1926 ∀(a : Type) 1927 → ∀(ts : { head : a, tail : List a }) 1928 → ∀(b : Type) 1929 → ∀(f : a → b → b) 1930 → ∀(z : b) 1931 → b 1932 } 1933 </pre></dd> 1934 </dl> 1935 <h3>toList (term)</h3> 1936 <dl> 1937 <dt>type</dt><dd><pre> 1938 ∀(a : Type) → ∀(nel : { head : a, tail : List a }) → List a 1939 </pre></dd> 1940 </dl> 1941 <h2 style="background-color: #bbb; width: 100%">./scripts</h2> 1942 <h2 style="background-color: #bbb; width: 100%">./Lan</h2> 1943 <h3>lift (term)</h3> 1944 <dl> 1945 <dt>type</dt><dd><pre> 1946 ∀(f : Type → Type) 1947 → ∀ ( comonad 1948 : { duplicate : 1949 ∀(a : Type) → f a → f (f a) 1950 , extend : 1951 ∀(a : Type) → ∀(b : Type) → ∀(f : f a → b) → f@1 a → f@1 b 1952 , extract : 1953 ∀(a : Type) → f a → a 1954 , map : 1955 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 1956 } 1957 ) 1958 → ∀(g : Type → Type) 1959 → ∀(a : Type) 1960 → ∀(x : g a) 1961 → ∀(r : Type) 1962 → ∀(k : ∀(b : Type) → (f b → a) → g b → r) 1963 → r 1964 </pre></dd> 1965 </dl> 1966 <h3>Type (type)</h3> 1967 <dl> 1968 <dt>kind</dt><dd><pre> 1969 ∀(f : Type → Type) → ∀(g : Type → Type) → ∀(a : Type) → Type 1970 </pre></dd> 1971 <dt>type</dt><dd><pre> 1972 λ(f : Type → Type) 1973 → λ(g : Type → Type) 1974 → λ(a : Type) 1975 → ∀(r : Type) → (∀(b : Type) → (f b → a) → g b → r) → r 1976 </pre></dd> 1977 </dl> 1978 <h3>lower (term)</h3> 1979 <dl> 1980 <dt>type</dt><dd><pre> 1981 ∀(h : Type → Type) 1982 → ∀ ( functor 1983 : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : h a) → h b } 1984 ) 1985 → ∀(f : Type → Type) 1986 → ∀(g : Type → Type) 1987 → ∀(duplicate : ∀(b : Type) → g b → h (f b)) 1988 → ∀(a : Type) 1989 → ∀(lan : ∀(r : Type) → (∀(b : Type) → (f b → a) → g b → r) → r) 1990 → h a 1991 </pre></dd> 1992 </dl> 1993 <h3>functor (term)</h3> 1994 <dl> 1995 <dt>type</dt><dd><pre> 1996 ∀(f : Type → Type) 1997 → ∀(g : Type → Type) 1998 → { map : 1999 ∀(a : Type) 2000 → ∀(b : Type) 2001 → ∀(h : a → b) 2002 → ∀(lan : ∀(r : Type) → (∀(b : Type) → (f b → a) → g b → r) → r) 2003 → ∀(r : Type) 2004 → ∀(k : ∀(c : Type) → (f c → b) → g c → r) 2005 → r 2006 } 2007 </pre></dd> 2008 </dl> 2009 <h2 style="background-color: #bbb; width: 100%">./Reader</h2> 2010 <h3>monad (term)</h3> 2011 <dl> 2012 <dt>type</dt><dd><pre> 2013 ∀(r : Type) 2014 → { ap : 2015 ∀(a : Type) 2016 → ∀(b : Type) 2017 → ∀(k : r → a → b) 2018 → ∀(fa : r → a) 2019 → ∀(env : r) 2020 → b 2021 , bind : 2022 ∀(a : Type) 2023 → ∀(b : Type) 2024 → ∀(fa : r → a) 2025 → ∀(k : a → r → b) 2026 → ∀(env : r) 2027 → b 2028 , map : 2029 ∀(a : Type) 2030 → ∀(b : Type) 2031 → ∀(k : a → b) 2032 → ∀(reader : r → a) 2033 → ∀(rr : r) 2034 → b 2035 , pure : 2036 ∀(a : Type) → ∀(x : a) → ∀(env : r) → a 2037 } 2038 </pre></dd> 2039 </dl> 2040 <h3>withReader (term)</h3> 2041 <dl> 2042 <dt>type</dt><dd><pre> 2043 ∀(r : Type) 2044 → ∀(a : Type) 2045 → ∀(rPrime : Type) 2046 → ∀(f : rPrime → r) 2047 → ∀(reader : r → a) 2048 → ∀(newR : rPrime) 2049 → a 2050 </pre></dd> 2051 </dl> 2052 <h3>applicative (term)</h3> 2053 <dl> 2054 <dt>type</dt><dd><pre> 2055 ∀(r : Type) 2056 → { ap : 2057 ∀(a : Type) 2058 → ∀(b : Type) 2059 → ∀(g : r → a → b) 2060 → ∀(fa : r → a) 2061 → ∀(env : r) 2062 → b 2063 , map : 2064 ∀(a : Type) 2065 → ∀(b : Type) 2066 → ∀(g : a → b) 2067 → ∀(reader : r → a) 2068 → ∀(rr : r) 2069 → b 2070 , pure : 2071 ∀(a : Type) → ∀(x : a) → ∀(env : r) → a 2072 } 2073 </pre></dd> 2074 </dl> 2075 <h3>local (term)</h3> 2076 <dl> 2077 <dt>type</dt><dd><pre> 2078 ∀(r : Type) → ∀(a : Type) → ∀(f : r → r) → ∀(reader : r → a) → ∀(env : r) → a 2079 </pre></dd> 2080 </dl> 2081 <h3>Type (type)</h3> 2082 <dl> 2083 <dt>kind</dt><dd><pre> 2084 ∀(r : Type) → ∀(a : Type) → Type 2085 </pre></dd> 2086 <dt>type</dt><dd><pre> 2087 λ(r : Type) → λ(a : Type) → r → a 2088 </pre></dd> 2089 </dl> 2090 <h3>asks (term)</h3> 2091 <dl> 2092 <dt>type</dt><dd><pre> 2093 ∀(r : Type) → ∀(a : Type) → ∀(f : r → a) → ∀(env : r) → a 2094 </pre></dd> 2095 </dl> 2096 <h3>package.dhall (term)</h3> 2097 <dl> 2098 <dt>type</dt><dd><pre> 2099 ∀(r : Type) 2100 → { ap : 2101 ∀(a : Type) 2102 → ∀(b : Type) 2103 → ∀(k : r → a → b) 2104 → ∀(fa : r → a) 2105 → ∀(env : r) 2106 → b 2107 , bind : 2108 ∀(a : Type) 2109 → ∀(b : Type) 2110 → ∀(fa : r → a) 2111 → ∀(k : a → r → b) 2112 → ∀(env : r) 2113 → b 2114 , map : 2115 ∀(a : Type) 2116 → ∀(b : Type) 2117 → ∀(k : a → b) 2118 → ∀(reader : r → a) 2119 → ∀(rr : r) 2120 → b 2121 , pure : 2122 ∀(a : Type) → ∀(x : a) → ∀(env : r) → a 2123 , withReader : 2124 ∀(a : Type) 2125 → ∀(rPrime : Type) 2126 → ∀(f : rPrime → r) 2127 → ∀(reader : r → a) 2128 → ∀(newR : rPrime) 2129 → a 2130 } 2131 </pre></dd> 2132 </dl> 2133 <h3>ask (term)</h3> 2134 <dl> 2135 <dt>type</dt><dd><pre> 2136 ∀(r : Type) → ∀(env : r) → r 2137 </pre></dd> 2138 </dl> 2139 <h3>functor (term)</h3> 2140 <dl> 2141 <dt>type</dt><dd><pre> 2142 ∀(r : Type) 2143 → { map : 2144 ∀(a : Type) 2145 → ∀(b : Type) 2146 → ∀(g : a → b) 2147 → ∀(reader : r → a) 2148 → ∀(rr : r) 2149 → b 2150 } 2151 </pre></dd> 2152 </dl> 2153 <h2 style="background-color: #bbb; width: 100%">./Comonad</h2> 2154 <h3>extractFunctor (term)</h3> 2155 <dl> 2156 <dt>type</dt><dd><pre> 2157 ∀(w : Type → Type) 2158 → ∀ ( comonad 2159 : { duplicate : 2160 ∀(a : Type) → w a → w (w a) 2161 , extend : 2162 ∀(a : Type) → ∀(b : Type) → ∀(f : w a → b) → w a → w b 2163 , extract : 2164 ∀(a : Type) → w a → a 2165 , map : 2166 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : w a) → w b 2167 } 2168 ) 2169 → { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : w a) → w b } 2170 </pre></dd> 2171 </dl> 2172 <h3>Type (type)</h3> 2173 <dl> 2174 <dt>kind</dt><dd><pre> 2175 ∀(w : Type → Type) → Type 2176 </pre></dd> 2177 <dt>type</dt><dd><pre> 2178 λ(w : Type → Type) 2179 → { duplicate : 2180 ∀(a : Type) → w a → w (w a) 2181 , extend : 2182 ∀(a : Type) → ∀(b : Type) → ∀(f : w a → b) → w a → w b 2183 , extract : 2184 ∀(a : Type) → w a → a 2185 , map : 2186 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : w a) → w b 2187 } 2188 </pre></dd> 2189 </dl> 2190 <h3>fromExtractExtend (term)</h3> 2191 <dl> 2192 <dt>type</dt><dd><pre> 2193 ∀(w : Type → Type) 2194 → ∀(extract : ∀(a : Type) → w a → a) 2195 → ∀(extend : ∀(a : Type) → ∀(b : Type) → ∀(f : w a → b) → w a → w b) 2196 → { duplicate : 2197 ∀(a : Type) → w a → w (w a) 2198 , extend : 2199 ∀(a : Type) → ∀(b : Type) → ∀(f : w a → b) → w a → w b 2200 , extract : 2201 ∀(a : Type) → w a → a 2202 , map : 2203 ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → w a → w b 2204 } 2205 </pre></dd> 2206 </dl> 2207 <h2 style="background-color: #bbb; width: 100%">./Traversable</h2> 2208 <h3>extractFunctor (term)</h3> 2209 <dl> 2210 <dt>type</dt><dd><pre> 2211 ∀(f : Type → Type) 2212 → ∀ ( t 2213 : { fold : 2214 ∀(a : Type) 2215 → ∀(ts : f a) 2216 → ∀(b : Type) 2217 → ∀(f : a → b → b) 2218 → ∀(z : b) 2219 → b 2220 , map : 2221 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 2222 , traverse : 2223 ∀(f : Type → Type) 2224 → ∀ ( applicative 2225 : { ap : 2226 ∀(a : Type) 2227 → ∀(b : Type) 2228 → ∀(g : f (a → b)) 2229 → ∀(fa : f a) 2230 → f b 2231 , map : 2232 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 2233 , pure : 2234 ∀(a : Type) → a → f a 2235 } 2236 ) 2237 → ∀(a : Type) 2238 → ∀(b : Type) 2239 → (a → f b) 2240 → f@1 a 2241 → f (f@1 b) 2242 } 2243 ) 2244 → { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b } 2245 </pre></dd> 2246 </dl> 2247 <h3>fromTraverse (term)</h3> 2248 <dl> 2249 <dt>type</dt><dd><pre> 2250 ∀(t : Type → Type) 2251 → ∀ ( traverse 2252 : ∀(f : Type → Type) 2253 → ∀ ( applicative 2254 : { ap : 2255 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 2256 , map : 2257 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 2258 , pure : 2259 ∀(a : Type) → a → f a 2260 } 2261 ) 2262 → ∀(a : Type) 2263 → ∀(b : Type) 2264 → ∀(g : a → f b) 2265 → ∀(ts : t a) 2266 → f (t b) 2267 ) 2268 → { fold : 2269 ∀(a : Type) → ∀(ts : t a) → ∀(b : Type) → ∀(f : a → b → b) → ∀(z : b) → b 2270 , map : 2271 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(ts : t a) → t b 2272 , traverse : 2273 ∀(f : Type → Type) 2274 → ∀ ( applicative 2275 : { ap : 2276 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 2277 , map : 2278 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 2279 , pure : 2280 ∀(a : Type) → a → f a 2281 } 2282 ) 2283 → ∀(a : Type) 2284 → ∀(b : Type) 2285 → ∀(g : a → f b) 2286 → ∀(ts : t a) 2287 → f (t b) 2288 } 2289 </pre></dd> 2290 </dl> 2291 <h3>Type (type)</h3> 2292 <dl> 2293 <dt>kind</dt><dd><pre> 2294 ∀(t : Type → Type) → Type 2295 </pre></dd> 2296 <dt>type</dt><dd><pre> 2297 λ(t : Type → Type) 2298 → { fold : 2299 ∀(a : Type) → ∀(ts : t a) → ∀(b : Type) → ∀(f : a → b → b) → ∀(z : b) → b 2300 , map : 2301 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : t a) → t b 2302 , traverse : 2303 ∀(f : Type → Type) 2304 → ∀ ( applicative 2305 : { ap : 2306 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 2307 , map : 2308 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 2309 , pure : 2310 ∀(a : Type) → a → f a 2311 } 2312 ) 2313 → ∀(a : Type) 2314 → ∀(b : Type) 2315 → (a → f b) 2316 → t a 2317 → f (t b) 2318 } 2319 </pre></dd> 2320 </dl> 2321 <h3>sequence (term)</h3> 2322 <dl> 2323 <dt>type</dt><dd><pre> 2324 ∀(t : Type → Type) 2325 → ∀ ( traversable 2326 : { fold : 2327 ∀(a : Type) 2328 → ∀(ts : t a) 2329 → ∀(b : Type) 2330 → ∀(f : a → b → b) 2331 → ∀(z : b) 2332 → b 2333 , map : 2334 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : t a) → t b 2335 , traverse : 2336 ∀(f : Type → Type) 2337 → ∀ ( applicative 2338 : { ap : 2339 ∀(a : Type) 2340 → ∀(b : Type) 2341 → ∀(g : f (a → b)) 2342 → ∀(fa : f a) 2343 → f b 2344 , map : 2345 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 2346 , pure : 2347 ∀(a : Type) → a → f a 2348 } 2349 ) 2350 → ∀(a : Type) 2351 → ∀(b : Type) 2352 → (a → f b) 2353 → t a 2354 → f (t b) 2355 } 2356 ) 2357 → ∀(f : Type → Type) 2358 → ∀ ( applicative 2359 : { ap : 2360 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 2361 , map : 2362 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 2363 , pure : 2364 ∀(a : Type) → a → f a 2365 } 2366 ) 2367 → ∀(a : Type) 2368 → ∀(ts : t (f a)) 2369 → f (t a) 2370 </pre></dd> 2371 </dl> 2372 <h3>extractFoldable (term)</h3> 2373 <dl> 2374 <dt>type</dt><dd><pre> 2375 ∀(f : Type → Type) 2376 → ∀ ( t 2377 : { fold : 2378 ∀(a : Type) 2379 → ∀(ts : f a) 2380 → ∀(b : Type) 2381 → ∀(f : a → b → b) 2382 → ∀(z : b) 2383 → b 2384 , map : 2385 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 2386 , traverse : 2387 ∀(f : Type → Type) 2388 → ∀ ( applicative 2389 : { ap : 2390 ∀(a : Type) 2391 → ∀(b : Type) 2392 → ∀(g : f (a → b)) 2393 → ∀(fa : f a) 2394 → f b 2395 , map : 2396 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 2397 , pure : 2398 ∀(a : Type) → a → f a 2399 } 2400 ) 2401 → ∀(a : Type) 2402 → ∀(b : Type) 2403 → (a → f b) 2404 → f@1 a 2405 → f (f@1 b) 2406 } 2407 ) 2408 → { fold : 2409 ∀(a : Type) → ∀(ts : f a) → ∀(b : Type) → ∀(f : a → b → b) → ∀(z : b) → b 2410 } 2411 </pre></dd> 2412 </dl> 2413 <h2 style="background-color: #bbb; width: 100%">./Monoid</h2> 2414 <h3>Type (type)</h3> 2415 <dl> 2416 <dt>kind</dt><dd><pre> 2417 ∀(m : Type) → Type 2418 </pre></dd> 2419 <dt>type</dt><dd><pre> 2420 λ(m : Type) → { op : ∀(x : m) → ∀(y : m) → m, unit : m } 2421 </pre></dd> 2422 </dl> 2423 <h3>extractSemigroup (term)</h3> 2424 <dl> 2425 <dt>type</dt><dd><pre> 2426 ∀(m : Type) 2427 → ∀(t : { op : ∀(x : m) → ∀(y : m) → m, unit : m }) 2428 → { op : ∀(x : m) → ∀(y : m) → m } 2429 </pre></dd> 2430 </dl> 2431 <h2 style="background-color: #bbb; width: 100%">./Category</h2> 2432 <h3>extractSemigroupoid (term)</h3> 2433 <dl> 2434 <dt>type</dt><dd><pre> 2435 ∀(f : Type → Type → Type) 2436 → ∀ ( category 2437 : { compose : 2438 ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → f b c → f a b → f a c 2439 , identity : 2440 ∀(a : Type) → f a a 2441 } 2442 ) 2443 → { compose : ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → f b c → f a b → f a c } 2444 </pre></dd> 2445 </dl> 2446 <h3>Type (type)</h3> 2447 <dl> 2448 <dt>kind</dt><dd><pre> 2449 ∀(f : Type → Type → Type) → Type 2450 </pre></dd> 2451 <dt>type</dt><dd><pre> 2452 λ(f : Type → Type → Type) 2453 → { compose : 2454 ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → f b c → f a b → f a c 2455 , identity : 2456 ∀(a : Type) → f a a 2457 } 2458 </pre></dd> 2459 </dl> 2460 <h2 style="background-color: #bbb; width: 100%">./DifferenceList</h2> 2461 <h3>monad (term)</h3> 2462 <dl> 2463 <dt>type</dt><dd><pre> 2464 { ap : 2465 ∀(a : Type) 2466 → ∀(b : Type) 2467 → ∀(k : List (a → b) → List (a → b)) 2468 → ∀(fa : List a → List a) 2469 → List b 2470 → List b 2471 , bind : 2472 ∀(a : Type) 2473 → ∀(b : Type) 2474 → ∀(f : List a → List a) 2475 → ∀(k : a → List b → List b) 2476 → List b 2477 → List b 2478 , map : 2479 ∀(a : Type) 2480 → ∀(b : Type) 2481 → ∀(k : a → b) 2482 → ∀(fa : List a → List a) 2483 → List b 2484 → List b 2485 , pure : 2486 ∀(a : Type) → ∀(x : a) → ∀(l : List a) → List a 2487 } 2488 </pre></dd> 2489 </dl> 2490 <h3>applicative (term)</h3> 2491 <dl> 2492 <dt>type</dt><dd><pre> 2493 { ap : 2494 ∀(a : Type) 2495 → ∀(b : Type) 2496 → ∀(k : List (a → b) → List (a → b)) 2497 → ∀(fa : List a → List a) 2498 → List b 2499 → List b 2500 , map : 2501 ∀(a : Type) 2502 → ∀(b : Type) 2503 → ∀(k : a → b) 2504 → ∀(fa : List a → List a) 2505 → List b 2506 → List b 2507 , pure : 2508 ∀(a : Type) → ∀(x : a) → ∀(l : List a) → List a 2509 } 2510 </pre></dd> 2511 </dl> 2512 <h3>semigroup (term)</h3> 2513 <dl> 2514 <dt>type</dt><dd><pre> 2515 ∀(a : Type) 2516 → { op : 2517 ∀(f : List a → List a) → ∀(g : List a → List a) → ∀(x : List a) → List a 2518 } 2519 </pre></dd> 2520 </dl> 2521 <h3>monoid (term)</h3> 2522 <dl> 2523 <dt>type</dt><dd><pre> 2524 ∀(a : Type) 2525 → { op : 2526 ∀(f : List a → List a) → ∀(g : List a → List a) → ∀(x : List a) → List a 2527 , unit : 2528 ∀(x : List a) → List a 2529 } 2530 </pre></dd> 2531 </dl> 2532 <h3>Type (type)</h3> 2533 <dl> 2534 <dt>kind</dt><dd><pre> 2535 ∀(a : Type) → Type 2536 </pre></dd> 2537 <dt>type</dt><dd><pre> 2538 λ(a : Type) → List a → List a 2539 </pre></dd> 2540 </dl> 2541 <h3>append (term)</h3> 2542 <dl> 2543 <dt>type</dt><dd><pre> 2544 ∀(a : Type) 2545 → ∀(f : List a → List a) 2546 → ∀(g : List a → List a) 2547 → ∀(x : List a) 2548 → List a 2549 </pre></dd> 2550 </dl> 2551 <h3>snoc (term)</h3> 2552 <dl> 2553 <dt>type</dt><dd><pre> 2554 ∀(a : Type) → ∀(xs : List a → List a) → ∀(y : a) → ∀(x : List a) → List a 2555 </pre></dd> 2556 </dl> 2557 <h3>cons (term)</h3> 2558 <dl> 2559 <dt>type</dt><dd><pre> 2560 ∀(a : Type) → ∀(y : a) → ∀(xs : List a → List a) → ∀(x : List a) → List a 2561 </pre></dd> 2562 </dl> 2563 <h3>empty (term)</h3> 2564 <dl> 2565 <dt>type</dt><dd><pre> 2566 ∀(a : Type) → ∀(x : List a) → List a 2567 </pre></dd> 2568 </dl> 2569 <h3>singleton (term)</h3> 2570 <dl> 2571 <dt>type</dt><dd><pre> 2572 ∀(a : Type) → ∀(x : a) → ∀(l : List a) → List a 2573 </pre></dd> 2574 </dl> 2575 <h3>functor (term)</h3> 2576 <dl> 2577 <dt>type</dt><dd><pre> 2578 { map : 2579 ∀(a : Type) 2580 → ∀(b : Type) 2581 → ∀(k : a → b) 2582 → ∀(fa : List a → List a) 2583 → List b 2584 → List b 2585 } 2586 </pre></dd> 2587 </dl> 2588 <h3>foldable (term)</h3> 2589 <dl> 2590 <dt>type</dt><dd><pre> 2591 { fold : 2592 ∀(a : Type) 2593 → ∀(ts : List a → List a) 2594 → ∀(b : Type) 2595 → ∀(f : a → b → b) 2596 → ∀(z : b) 2597 → b 2598 } 2599 </pre></dd> 2600 </dl> 2601 <h3>toList (term)</h3> 2602 <dl> 2603 <dt>type</dt><dd><pre> 2604 ∀(a : Type) → ∀(xs : List a → List a) → List a 2605 </pre></dd> 2606 </dl> 2607 <h2 style="background-color: #bbb; width: 100%">./Functor</h2> 2608 <h3>rightConst (term)</h3> 2609 <dl> 2610 <dt>type</dt><dd><pre> 2611 ∀(f : Type → Type) 2612 → ∀ ( functor 2613 : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b } 2614 ) 2615 → ∀(a : Type) 2616 → ∀(b : Type) 2617 → ∀(fa : f a) 2618 → ∀(val : b) 2619 → f b 2620 </pre></dd> 2621 </dl> 2622 <h3>Type (type)</h3> 2623 <dl> 2624 <dt>kind</dt><dd><pre> 2625 ∀(f : Type → Type) → Type 2626 </pre></dd> 2627 <dt>type</dt><dd><pre> 2628 λ(f : Type → Type) 2629 → { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b } 2630 </pre></dd> 2631 </dl> 2632 <h3>leftConst (term)</h3> 2633 <dl> 2634 <dt>type</dt><dd><pre> 2635 ∀(f : Type → Type) 2636 → ∀ ( functor 2637 : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b } 2638 ) 2639 → ∀(a : Type) 2640 → ∀(b : Type) 2641 → ∀(val : a) 2642 → ∀(fb : f b) 2643 → f a 2644 </pre></dd> 2645 </dl> 2646 <h3>fromTraversable (term)</h3> 2647 <dl> 2648 <dt>type</dt><dd><pre> 2649 ∀(f : Type → Type) 2650 → ∀ ( t 2651 : { fold : 2652 ∀(a : Type) 2653 → ∀(ts : f a) 2654 → ∀(b : Type) 2655 → ∀(f : a → b → b) 2656 → ∀(z : b) 2657 → b 2658 , map : 2659 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 2660 , traverse : 2661 ∀(f : Type → Type) 2662 → ∀ ( applicative 2663 : { ap : 2664 ∀(a : Type) 2665 → ∀(b : Type) 2666 → ∀(g : f (a → b)) 2667 → ∀(fa : f a) 2668 → f b 2669 , map : 2670 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 2671 , pure : 2672 ∀(a : Type) → a → f a 2673 } 2674 ) 2675 → ∀(a : Type) 2676 → ∀(b : Type) 2677 → (a → f b) 2678 → f@1 a 2679 → f (f@1 b) 2680 } 2681 ) 2682 → { map : ∀(a : Type) → ∀(b : Type) → (a → b) → f a → f b } 2683 </pre></dd> 2684 </dl> 2685 <h3>package.dhall (term)</h3> 2686 <dl> 2687 <dt>type</dt><dd><pre> 2688 ∀(f : Type → Type) 2689 → ∀ ( functor 2690 : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b } 2691 ) 2692 → { leftConst : 2693 ∀(a : Type) → ∀(b : Type) → ∀(val : a) → ∀(fb : f b) → f a 2694 , map : 2695 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 2696 , rightConst : 2697 ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(val : b) → f b 2698 , void : 2699 ∀(a : Type) → ∀(fa : f a) → f {} 2700 } 2701 </pre></dd> 2702 </dl> 2703 <h3>void (term)</h3> 2704 <dl> 2705 <dt>type</dt><dd><pre> 2706 ∀(f : Type → Type) 2707 → ∀ ( functor 2708 : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b } 2709 ) 2710 → ∀(a : Type) 2711 → ∀(fa : f a) 2712 → f {} 2713 </pre></dd> 2714 </dl> 2715 <h2 style="background-color: #bbb; width: 100%">./Arrow</h2> 2716 <h3>Type (type)</h3> 2717 <dl> 2718 <dt>kind</dt><dd><pre> 2719 ∀(f : Type → Type → Type) → Type 2720 </pre></dd> 2721 <dt>type</dt><dd><pre> 2722 λ(f : Type → Type → Type) 2723 → { arr : 2724 ∀(a : Type) → ∀(b : Type) → (a → b) → f a b 2725 , compose : 2726 ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → f b c → f a b → f a c 2727 , dimap : 2728 ∀(a : Type) 2729 → ∀(b : Type) 2730 → ∀(c : Type) 2731 → ∀(d : Type) 2732 → (a → b) 2733 → (c → d) 2734 → f b c 2735 → f a d 2736 , fanout : 2737 ∀(a : Type) 2738 → ∀(b : Type) 2739 → ∀(c : Type) 2740 → f a b 2741 → f a c 2742 → f a { _1 : b, _2 : c } 2743 , first : 2744 ∀(a : Type) 2745 → ∀(b : Type) 2746 → ∀(c : Type) 2747 → f a b 2748 → f { _1 : a, _2 : c } { _1 : b, _2 : c } 2749 , identity : 2750 ∀(a : Type) → f a a 2751 , lmap : 2752 ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (a → b) → f b c → f a c 2753 , rmap : 2754 ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (b → c) → f a b → f a c 2755 , second : 2756 ∀(a : Type) 2757 → ∀(b : Type) 2758 → ∀(c : Type) 2759 → f b c 2760 → f { _1 : a, _2 : b } { _1 : a, _2 : c } 2761 , split : 2762 ∀(a : Type) 2763 → ∀(b : Type) 2764 → ∀(c : Type) 2765 → ∀(d : Type) 2766 → f a b 2767 → f c d 2768 → f { _1 : a, _2 : c } { _1 : b, _2 : d } 2769 } 2770 </pre></dd> 2771 </dl> 2772 <h2 style="background-color: #bbb; width: 100%">./Coyoneda</h2> 2773 <h3>lift (term)</h3> 2774 <dl> 2775 <dt>type</dt><dd><pre> 2776 ∀(g : Type → Type) 2777 → ∀(a : Type) 2778 → ∀(x : g a) 2779 → ∀(r : Type) 2780 → ∀(k : ∀(b : Type) → (b → a) → g b → r) 2781 → r 2782 </pre></dd> 2783 </dl> 2784 <h3>Type (type)</h3> 2785 <dl> 2786 <dt>kind</dt><dd><pre> 2787 ∀(g : Type → Type) → ∀(a : Type) → Type 2788 </pre></dd> 2789 <dt>type</dt><dd><pre> 2790 λ(g : Type → Type) 2791 → λ(a : Type) 2792 → ∀(r : Type) → (∀(b : Type) → (b → a) → g b → r) → r 2793 </pre></dd> 2794 </dl> 2795 <h3>lower (term)</h3> 2796 <dl> 2797 <dt>type</dt><dd><pre> 2798 ∀(f : Type → Type) 2799 → ∀ ( functor 2800 : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b } 2801 ) 2802 → ∀(a : Type) 2803 → ∀(lan : ∀(r : Type) → (∀(b : Type) → (b → a) → f b → r) → r) 2804 → f a 2805 </pre></dd> 2806 </dl> 2807 <h3>functor (term)</h3> 2808 <dl> 2809 <dt>type</dt><dd><pre> 2810 ∀(g : Type → Type) 2811 → { map : 2812 ∀(a : Type) 2813 → ∀(b : Type) 2814 → ∀(h : a → b) 2815 → ∀(lan : ∀(r : Type) → (∀(b : Type) → (b → a) → g b → r) → r) 2816 → ∀(r : Type) 2817 → ∀(k : ∀(c : Type) → (c → b) → g c → r) 2818 → r 2819 } 2820 </pre></dd> 2821 </dl> 2822 <h2 style="background-color: #bbb; width: 100%">./Density</h2> 2823 <h3>lift (term)</h3> 2824 <dl> 2825 <dt>type</dt><dd><pre> 2826 ∀(f : Type → Type) 2827 → ∀ ( comonad 2828 : { duplicate : 2829 ∀(a : Type) → f a → f (f a) 2830 , extend : 2831 ∀(a : Type) → ∀(b : Type) → ∀(f : f a → b) → f@1 a → f@1 b 2832 , extract : 2833 ∀(a : Type) → f a → a 2834 , map : 2835 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 2836 } 2837 ) 2838 → ∀(a : Type) 2839 → ∀(x : f a) 2840 → ∀(r : Type) 2841 → ∀(k : ∀(b : Type) → (f b → a) → f b → r) 2842 → r 2843 </pre></dd> 2844 </dl> 2845 <h3>Type (type)</h3> 2846 <dl> 2847 <dt>kind</dt><dd><pre> 2848 ∀(f : Type → Type) → ∀(a : Type) → Type 2849 </pre></dd> 2850 <dt>type</dt><dd><pre> 2851 λ(f : Type → Type) 2852 → λ(a : Type) 2853 → ∀(r : Type) → (∀(b : Type) → (f b → a) → f b → r) → r 2854 </pre></dd> 2855 </dl> 2856 <h3>lower (term)</h3> 2857 <dl> 2858 <dt>type</dt><dd><pre> 2859 ∀(f : Type → Type) 2860 → ∀ ( comonad 2861 : { duplicate : 2862 ∀(a : Type) → f a → f (f a) 2863 , extend : 2864 ∀(a : Type) → ∀(b : Type) → ∀(f : f a → b) → f@1 a → f@1 b 2865 , extract : 2866 ∀(a : Type) → f a → a 2867 , map : 2868 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 2869 } 2870 ) 2871 → ∀(a : Type) 2872 → ∀(lan : ∀(r : Type) → (∀(b : Type) → (f b → a) → f b → r) → r) 2873 → f a 2874 </pre></dd> 2875 </dl> 2876 <h3>functor (term)</h3> 2877 <dl> 2878 <dt>type</dt><dd><pre> 2879 ∀(f : Type → Type) 2880 → { map : 2881 ∀(a : Type) 2882 → ∀(b : Type) 2883 → ∀(h : a → b) 2884 → ∀(lan : ∀(r : Type) → (∀(b : Type) → (f b → a) → f b → r) → r) 2885 → ∀(r : Type) 2886 → ∀(k : ∀(c : Type) → (f c → b) → f c → r) 2887 → r 2888 } 2889 </pre></dd> 2890 </dl> 2891 <h2 style="background-color: #bbb; width: 100%">./Strong</h2> 2892 <h3>Type (type)</h3> 2893 <dl> 2894 <dt>kind</dt><dd><pre> 2895 ∀(f : Type → Type → Type) → Type 2896 </pre></dd> 2897 <dt>type</dt><dd><pre> 2898 λ(f : Type → Type → Type) 2899 → { dimap : 2900 ∀(a : Type) 2901 → ∀(b : Type) 2902 → ∀(c : Type) 2903 → ∀(d : Type) 2904 → (a → b) 2905 → (c → d) 2906 → f b c 2907 → f a d 2908 , first : 2909 ∀(a : Type) 2910 → ∀(b : Type) 2911 → ∀(c : Type) 2912 → f a b 2913 → f { _1 : a, _2 : c } { _1 : b, _2 : c } 2914 , lmap : 2915 ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (a → b) → f b c → f a c 2916 , rmap : 2917 ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (b → c) → f a b → f a c 2918 , second : 2919 ∀(a : Type) 2920 → ∀(b : Type) 2921 → ∀(c : Type) 2922 → f b c 2923 → f { _1 : a, _2 : b } { _1 : a, _2 : c } 2924 } 2925 </pre></dd> 2926 </dl> 2927 <h2 style="background-color: #bbb; width: 100%">./Monad</h2> 2928 <h3>extractFunctor (term)</h3> 2929 <dl> 2930 <dt>type</dt><dd><pre> 2931 ∀(f : Type → Type) 2932 → ∀ ( t 2933 : { ap : 2934 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 2935 , bind : 2936 ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(k : a → f b) → f b 2937 , map : 2938 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 2939 , pure : 2940 ∀(a : Type) → a → f a 2941 } 2942 ) 2943 → { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b } 2944 </pre></dd> 2945 </dl> 2946 <h3>Type (type)</h3> 2947 <dl> 2948 <dt>kind</dt><dd><pre> 2949 ∀(f : Type → Type) → Type 2950 </pre></dd> 2951 <dt>type</dt><dd><pre> 2952 λ(f : Type → Type) 2953 → { ap : 2954 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 2955 , bind : 2956 ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(k : a → f b) → f b 2957 , map : 2958 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 2959 , pure : 2960 ∀(a : Type) → a → f a 2961 } 2962 </pre></dd> 2963 </dl> 2964 <h3>extractApplicative (term)</h3> 2965 <dl> 2966 <dt>type</dt><dd><pre> 2967 ∀(f : Type → Type) 2968 → ∀ ( t 2969 : { ap : 2970 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 2971 , bind : 2972 ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(k : a → f b) → f b 2973 , map : 2974 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 2975 , pure : 2976 ∀(a : Type) → a → f a 2977 } 2978 ) 2979 → { ap : 2980 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 2981 , map : 2982 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 2983 , pure : 2984 ∀(a : Type) → a → f a 2985 } 2986 </pre></dd> 2987 </dl> 2988 <h3>fromPureBind (term)</h3> 2989 <dl> 2990 <dt>type</dt><dd><pre> 2991 ∀(f : Type → Type) 2992 → ∀(pure : ∀(a : Type) → a → f a) 2993 → ∀(bind : ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(k : a → f b) → f b) 2994 → { ap : 2995 ∀(a : Type) → ∀(b : Type) → ∀(k : f (a → b)) → ∀(fa : f a) → f b 2996 , bind : 2997 ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(k : a → f b) → f b 2998 , map : 2999 ∀(a : Type) → ∀(b : Type) → ∀(k : a → b) → ∀(fa : f a) → f b 3000 , pure : 3001 ∀(a : Type) → a → f a 3002 } 3003 </pre></dd> 3004 </dl> 3005 <h3>package.dhall (term)</h3> 3006 <dl> 3007 <dt>type</dt><dd><pre> 3008 ∀(f : Type → Type) 3009 → ∀ ( monad 3010 : { ap : 3011 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 3012 , bind : 3013 ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(k : a → f b) → f b 3014 , map : 3015 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 3016 , pure : 3017 ∀(a : Type) → a → f a 3018 } 3019 ) 3020 → { ap : 3021 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 3022 , bind : 3023 ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(k : a → f b) → f b 3024 , join : 3025 ∀(a : Type) → ∀(ffa : f (f a)) → f a 3026 , map : 3027 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 3028 , pure : 3029 ∀(a : Type) → a → f a 3030 } 3031 </pre></dd> 3032 </dl> 3033 <h2 style="background-color: #bbb; width: 100%">./Kleisli</h2> 3034 <h3>semigroupoid (term)</h3> 3035 <dl> 3036 <dt>type</dt><dd><pre> 3037 ∀(m : Type → Type) 3038 → ∀ ( monad 3039 : { ap : 3040 ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b 3041 , bind : 3042 ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b 3043 , map : 3044 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b 3045 , pure : 3046 ∀(a : Type) → a → m a 3047 } 3048 ) 3049 → { compose : 3050 ∀(a : Type) 3051 → ∀(b : Type) 3052 → ∀(c : Type) 3053 → ∀(g : b → m c) 3054 → ∀(f : a → m b) 3055 → ∀(x : a) 3056 → m c 3057 } 3058 </pre></dd> 3059 </dl> 3060 <h3>Type (type)</h3> 3061 <dl> 3062 <dt>kind</dt><dd><pre> 3063 ∀(m : Type → Type) → ∀(a : Type) → ∀(b : Type) → Type 3064 </pre></dd> 3065 <dt>type</dt><dd><pre> 3066 λ(m : Type → Type) → λ(a : Type) → λ(b : Type) → a → m b 3067 </pre></dd> 3068 </dl> 3069 <h3>category (term)</h3> 3070 <dl> 3071 <dt>type</dt><dd><pre> 3072 ∀(m : Type → Type) 3073 → ∀ ( monad 3074 : { ap : 3075 ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b 3076 , bind : 3077 ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b 3078 , map : 3079 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b 3080 , pure : 3081 ∀(a : Type) → a → m a 3082 } 3083 ) 3084 → { compose : 3085 ∀(a : Type) 3086 → ∀(b : Type) 3087 → ∀(c : Type) 3088 → ∀(g : b → m c) 3089 → ∀(f : a → m b) 3090 → ∀(x : a) 3091 → m c 3092 , identity : 3093 ∀(a : Type) → a → m a 3094 } 3095 </pre></dd> 3096 </dl> 3097 <h2 style="background-color: #bbb; width: 100%">./ReaderT</h2> 3098 <h3>monad (term)</h3> 3099 <dl> 3100 <dt>type</dt><dd><pre> 3101 ∀(r : Type) 3102 → ∀(m : Type → Type) 3103 → ∀ ( monad 3104 : { ap : 3105 ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b 3106 , bind : 3107 ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b 3108 , map : 3109 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b 3110 , pure : 3111 ∀(a : Type) → a → m a 3112 } 3113 ) 3114 → { ap : 3115 ∀(a : Type) 3116 → ∀(b : Type) 3117 → ∀(k : r → m (a → b)) 3118 → ∀(fa : r → m a) 3119 → ∀(env : r) 3120 → m b 3121 , bind : 3122 ∀(a : Type) 3123 → ∀(b : Type) 3124 → ∀(fa : r → m a) 3125 → ∀(k : a → r → m b) 3126 → ∀(env : r) 3127 → m b 3128 , map : 3129 ∀(a : Type) 3130 → ∀(b : Type) 3131 → ∀(k : a → b) 3132 → ∀(reader : r → m a) 3133 → ∀(rr : r) 3134 → m b 3135 , pure : 3136 ∀(a : Type) → ∀(x : a) → ∀(env : r) → m a 3137 } 3138 </pre></dd> 3139 </dl> 3140 <h3>withReader (term)</h3> 3141 <dl> 3142 <dt>type</dt><dd><pre> 3143 ∀(r : Type) 3144 → ∀(m : Type → Type) 3145 → ∀(a : Type) 3146 → ∀(rPrime : Type) 3147 → ∀(f : rPrime → r) 3148 → ∀(reader : r → m a) 3149 → ∀(newR : rPrime) 3150 → m a 3151 </pre></dd> 3152 </dl> 3153 <h3>applicative (term)</h3> 3154 <dl> 3155 <dt>type</dt><dd><pre> 3156 ∀(r : Type) 3157 → ∀(m : Type → Type) 3158 → ∀ ( applicative 3159 : { ap : 3160 ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b 3161 , map : 3162 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b 3163 , pure : 3164 ∀(a : Type) → a → m a 3165 } 3166 ) 3167 → { ap : 3168 ∀(a : Type) 3169 → ∀(b : Type) 3170 → ∀(k : r → m (a → b)) 3171 → ∀(fa : r → m a) 3172 → ∀(env : r) 3173 → m b 3174 , map : 3175 ∀(a : Type) 3176 → ∀(b : Type) 3177 → ∀(k : a → b) 3178 → ∀(reader : r → m a) 3179 → ∀(rr : r) 3180 → m b 3181 , pure : 3182 ∀(a : Type) → ∀(x : a) → ∀(env : r) → m a 3183 } 3184 </pre></dd> 3185 </dl> 3186 <h3>local (term)</h3> 3187 <dl> 3188 <dt>type</dt><dd><pre> 3189 ∀(r : Type) 3190 → ∀(m : Type → Type) 3191 → ∀(a : Type) 3192 → ∀(f : r → r) 3193 → ∀(reader : r → m a) 3194 → ∀(env : r) 3195 → m a 3196 </pre></dd> 3197 </dl> 3198 <h3>Type (type)</h3> 3199 <dl> 3200 <dt>kind</dt><dd><pre> 3201 ∀(r : Type) → ∀(m : Type → Type) → ∀(a : Type) → Type 3202 </pre></dd> 3203 <dt>type</dt><dd><pre> 3204 λ(r : Type) → λ(m : Type → Type) → λ(a : Type) → r → m a 3205 </pre></dd> 3206 </dl> 3207 <h3>asks (term)</h3> 3208 <dl> 3209 <dt>type</dt><dd><pre> 3210 ∀(r : Type) 3211 → ∀(m : Type → Type) 3212 → ∀ ( applicative 3213 : { ap : 3214 ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b 3215 , map : 3216 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b 3217 , pure : 3218 ∀(a : Type) → a → m a 3219 } 3220 ) 3221 → ∀(a : Type) 3222 → ∀(f : r → a) 3223 → ∀(env : r) 3224 → m a 3225 </pre></dd> 3226 </dl> 3227 <h3>package.dhall (term)</h3> 3228 <dl> 3229 <dt>type</dt><dd><pre> 3230 ∀(r : Type) 3231 → ∀(m : Type → Type) 3232 → ∀ ( monad 3233 : { ap : 3234 ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b 3235 , bind : 3236 ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b 3237 , map : 3238 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b 3239 , pure : 3240 ∀(a : Type) → a → m a 3241 } 3242 ) 3243 → { ap : 3244 ∀(a : Type) 3245 → ∀(b : Type) 3246 → ∀(k : r → m (a → b)) 3247 → ∀(fa : r → m a) 3248 → ∀(env : r) 3249 → m b 3250 , ask : 3251 ∀(env : r) → m r 3252 , asks : 3253 ∀(a : Type) → ∀(f : r → a) → ∀(env : r) → m a 3254 , bind : 3255 ∀(a : Type) 3256 → ∀(b : Type) 3257 → ∀(fa : r → m a) 3258 → ∀(k : a → r → m b) 3259 → ∀(env : r) 3260 → m b 3261 , lift : 3262 ∀(a : Type) → ∀(ma : m a) → ∀(env : r) → m a 3263 , local : 3264 ∀(a : Type) → ∀(f : r → r) → ∀(reader : r → m a) → ∀(env : r) → m a 3265 , map : 3266 ∀(a : Type) 3267 → ∀(b : Type) 3268 → ∀(k : a → b) 3269 → ∀(reader : r → m a) 3270 → ∀(rr : r) 3271 → m b 3272 , pure : 3273 ∀(a : Type) → ∀(x : a) → ∀(env : r) → m a 3274 } 3275 </pre></dd> 3276 </dl> 3277 <h3>ask (term)</h3> 3278 <dl> 3279 <dt>type</dt><dd><pre> 3280 ∀(r : Type) 3281 → ∀(m : Type → Type) 3282 → ∀ ( applicative 3283 : { ap : 3284 ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b 3285 , map : 3286 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b 3287 , pure : 3288 ∀(a : Type) → a → m a 3289 } 3290 ) 3291 → ∀(env : r) 3292 → m r 3293 </pre></dd> 3294 </dl> 3295 <h3>functor (term)</h3> 3296 <dl> 3297 <dt>type</dt><dd><pre> 3298 ∀(r : Type) 3299 → ∀(m : Type → Type) 3300 → ∀ ( functor 3301 : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b } 3302 ) 3303 → { map : 3304 ∀(a : Type) 3305 → ∀(b : Type) 3306 → ∀(k : a → b) 3307 → ∀(reader : r → m a) 3308 → ∀(rr : r) 3309 → m b 3310 } 3311 </pre></dd> 3312 </dl> 3313 <h3>transformer (term)</h3> 3314 <dl> 3315 <dt>type</dt><dd><pre> 3316 ∀(r : Type) 3317 → { lift : 3318 ∀(m : Type → Type) 3319 → ∀ ( monad 3320 : { ap : 3321 ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b 3322 , bind : 3323 ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b 3324 , map : 3325 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b 3326 , pure : 3327 ∀(a : Type) → a → m a 3328 } 3329 ) 3330 → ∀(a : Type) 3331 → ∀(ma : m a) 3332 → ∀(env : r) 3333 → m a 3334 } 3335 </pre></dd> 3336 </dl> 3337 <h2 style="background-color: #bbb; width: 100%">./Foldable</h2> 3338 <h3>Type (type)</h3> 3339 <dl> 3340 <dt>kind</dt><dd><pre> 3341 ∀(t : Type → Type) → Type 3342 </pre></dd> 3343 <dt>type</dt><dd><pre> 3344 λ(t : Type → Type) 3345 → { fold : 3346 ∀(a : Type) → ∀(ts : t a) → ∀(b : Type) → ∀(f : a → b → b) → ∀(z : b) → b 3347 } 3348 </pre></dd> 3349 </dl> 3350 <h3>foldMap (term)</h3> 3351 <dl> 3352 <dt>type</dt><dd><pre> 3353 ∀(m : Type) 3354 → ∀(monoid : { op : ∀(x : m) → ∀(y : m) → m, unit : m }) 3355 → ∀(t : Type → Type) 3356 → ∀ ( foldable 3357 : { fold : 3358 ∀(a : Type) 3359 → ∀(ts : t a) 3360 → ∀(b : Type) 3361 → ∀(f : a → b → b) 3362 → ∀(z : b) 3363 → b 3364 } 3365 ) 3366 → ∀(a : Type) 3367 → ∀(f : a → m) 3368 → ∀(ts : t a) 3369 → m 3370 </pre></dd> 3371 </dl> 3372 <h2 style="background-color: #bbb; width: 100%">./EitherT</h2> 3373 <h3>monad (term)</h3> 3374 <dl> 3375 <dt>type</dt><dd><pre> 3376 ∀(a : Type) 3377 → ∀(m : Type → Type) 3378 → ∀ ( monad 3379 : { ap : 3380 ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b 3381 , bind : 3382 ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b 3383 , map : 3384 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b 3385 , pure : 3386 ∀(a : Type) → a → m a 3387 } 3388 ) 3389 → { ap : 3390 ∀(a : Type) 3391 → ∀(b : Type) 3392 → ∀(k : m < Left : a@1 | Right : a → b >) 3393 → ∀(fa : m < Left : a@1 | Right : a >) 3394 → m < Left : a@1 | Right : b > 3395 , bind : 3396 ∀(b : Type) 3397 → ∀(c : Type) 3398 → ∀(fa : m < Left : a | Right : b >) 3399 → ∀(k : b → m < Left : a | Right : c >) 3400 → m < Left : a | Right : c > 3401 , map : 3402 ∀(a : Type) 3403 → ∀(b : Type) 3404 → ∀(k : a → b) 3405 → ∀(fa : m < Left : a@1 | Right : a >) 3406 → m < Left : a@1 | Right : b > 3407 , pure : 3408 ∀(a : Type) → ∀(x : a) → m < Left : a@1 | Right : a > 3409 } 3410 </pre></dd> 3411 </dl> 3412 <h2 style="background-color: #bbb; width: 100%">./EitherT/applicative</h2> 3413 <h3>parallel (term)</h3> 3414 <dl> 3415 <dt>type</dt><dd><pre> 3416 ∀(a : Type) 3417 → ∀(semi : { op : ∀(x : a) → ∀(y : a) → a }) 3418 → ∀(m : Type → Type) 3419 → ∀ ( applicative 3420 : { ap : 3421 ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b 3422 , map : 3423 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b 3424 , pure : 3425 ∀(a : Type) → a → m a 3426 } 3427 ) 3428 → { ap : 3429 ∀(a : Type) 3430 → ∀(b : Type) 3431 → ∀(k : m < Left : a@1 | Right : a → b >) 3432 → ∀(fa : m < Left : a@1 | Right : a >) 3433 → m < Left : a@1 | Right : b > 3434 , map : 3435 ∀(a : Type) 3436 → ∀(b : Type) 3437 → ∀(k : a → b) 3438 → ∀(fa : m < Left : a@1 | Right : a >) 3439 → m < Left : a@1 | Right : b > 3440 , pure : 3441 ∀(a : Type) → ∀(x : a) → m < Left : a@1 | Right : a > 3442 } 3443 </pre></dd> 3444 </dl> 3445 <h3>sequential (term)</h3> 3446 <dl> 3447 <dt>type</dt><dd><pre> 3448 ∀(a : Type) 3449 → ∀(m : Type → Type) 3450 → ∀ ( applicative 3451 : { ap : 3452 ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b 3453 , map : 3454 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b 3455 , pure : 3456 ∀(a : Type) → a → m a 3457 } 3458 ) 3459 → { ap : 3460 ∀(a : Type) 3461 → ∀(b : Type) 3462 → ∀(k : m < Left : a@1 | Right : a → b >) 3463 → ∀(fa : m < Left : a@1 | Right : a >) 3464 → m < Left : a@1 | Right : b > 3465 , map : 3466 ∀(a : Type) 3467 → ∀(b : Type) 3468 → ∀(k : a → b) 3469 → ∀(fa : m < Left : a@1 | Right : a >) 3470 → m < Left : a@1 | Right : b > 3471 , pure : 3472 ∀(a : Type) → ∀(x : a) → m < Left : a@1 | Right : a > 3473 } 3474 </pre></dd> 3475 </dl> 3476 <h3>Type (type)</h3> 3477 <dl> 3478 <dt>kind</dt><dd><pre> 3479 ∀(a : Type) → ∀(m : Type → Type) → ∀(b : Type) → Type 3480 </pre></dd> 3481 <dt>type</dt><dd><pre> 3482 λ(a : Type) → λ(m : Type → Type) → λ(b : Type) → m < Left : a | Right : b > 3483 </pre></dd> 3484 </dl> 3485 <h3>functor (term)</h3> 3486 <dl> 3487 <dt>type</dt><dd><pre> 3488 ∀(a : Type) 3489 → ∀(m : Type → Type) 3490 → ∀ ( functor 3491 : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b } 3492 ) 3493 → { map : 3494 ∀(a : Type) 3495 → ∀(b : Type) 3496 → ∀(k : a → b) 3497 → ∀(fa : m < Left : a@1 | Right : a >) 3498 → m < Left : a@1 | Right : b > 3499 } 3500 </pre></dd> 3501 </dl> 3502 <h3>transformer (term)</h3> 3503 <dl> 3504 <dt>type</dt><dd><pre> 3505 ∀(a : Type) 3506 → { lift : 3507 ∀(m : Type → Type) 3508 → ∀ ( monad 3509 : { ap : 3510 ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b 3511 , bind : 3512 ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b 3513 , map : 3514 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b 3515 , pure : 3516 ∀(a : Type) → a → m a 3517 } 3518 ) 3519 → ∀(b : Type) 3520 → ∀(ma : m b) 3521 → m < Left : a | Right : b > 3522 } 3523 </pre></dd> 3524 </dl> 3525 <h2 style="background-color: #bbb; width: 100%">./Semigroupoid</h2> 3526 <h3>Type (type)</h3> 3527 <dl> 3528 <dt>kind</dt><dd><pre> 3529 ∀(f : Type → Type → Type) → Type 3530 </pre></dd> 3531 <dt>type</dt><dd><pre> 3532 λ(f : Type → Type → Type) 3533 → { compose : ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → f b c → f a b → f a c } 3534 </pre></dd> 3535 </dl> 3536 <h2 style="background-color: #bbb; width: 100%">./Function</h2> 3537 <h3>semigroupoid (term)</h3> 3538 <dl> 3539 <dt>type</dt><dd><pre> 3540 { compose : 3541 ∀(a : Type) 3542 → ∀(b : Type) 3543 → ∀(c : Type) 3544 → ∀(f : b → c) 3545 → ∀(g : a → b) 3546 → ∀(x : a) 3547 → c 3548 } 3549 </pre></dd> 3550 </dl> 3551 <h3>strong (term)</h3> 3552 <dl> 3553 <dt>type</dt><dd><pre> 3554 { dimap : 3555 ∀(a : Type) 3556 → ∀(b : Type) 3557 → ∀(c : Type) 3558 → ∀(d : Type) 3559 → ∀(f : a → b) 3560 → ∀(g : c → d) 3561 → ∀(fn : b → c) 3562 → ∀(x : a) 3563 → d 3564 , first : 3565 ∀(a : Type) 3566 → ∀(b : Type) 3567 → ∀(c : Type) 3568 → ∀(f : a → b) 3569 → ∀(p : { _1 : a, _2 : c }) 3570 → { _1 : b, _2 : c } 3571 , lmap : 3572 ∀(a : Type) 3573 → ∀(b : Type) 3574 → ∀(c : Type) 3575 → ∀(fn : a → b) 3576 → ∀(fn : b → c) 3577 → ∀(x : a) 3578 → c 3579 , rmap : 3580 ∀(a : Type) 3581 → ∀(b : Type) 3582 → ∀(c : Type) 3583 → ∀(g : b → c) 3584 → ∀(fn : a → b) 3585 → ∀(x : a) 3586 → c 3587 , second : 3588 ∀(a : Type) 3589 → ∀(b : Type) 3590 → ∀(c : Type) 3591 → ∀(f : b → c) 3592 → ∀(p : { _1 : a, _2 : b }) 3593 → { _1 : a, _2 : c } 3594 } 3595 </pre></dd> 3596 </dl> 3597 <h3>Type (type)</h3> 3598 <dl> 3599 <dt>kind</dt><dd><pre> 3600 ∀(a : Type) → ∀(b : Type) → Type 3601 </pre></dd> 3602 <dt>type</dt><dd><pre> 3603 λ(a : Type) → λ(b : Type) → a → b 3604 </pre></dd> 3605 </dl> 3606 <h3>arrow (term)</h3> 3607 <dl> 3608 <dt>type</dt><dd><pre> 3609 { arr : 3610 ∀(a : Type) → ∀(b : Type) → ∀(x : a → b) → a → b 3611 , compose : 3612 ∀(a : Type) 3613 → ∀(b : Type) 3614 → ∀(c : Type) 3615 → ∀(f : b → c) 3616 → ∀(g : a → b) 3617 → ∀(x : a) 3618 → c 3619 , dimap : 3620 ∀(a : Type) 3621 → ∀(b : Type) 3622 → ∀(c : Type) 3623 → ∀(d : Type) 3624 → ∀(f : a → b) 3625 → ∀(g : c → d) 3626 → ∀(fn : b → c) 3627 → ∀(x : a) 3628 → d 3629 , fanout : 3630 ∀(a : Type) 3631 → ∀(b : Type) 3632 → ∀(c : Type) 3633 → ∀(f : a → b) 3634 → ∀(g : a → c) 3635 → ∀(x : a) 3636 → { _1 : b, _2 : c } 3637 , first : 3638 ∀(a : Type) 3639 → ∀(b : Type) 3640 → ∀(c : Type) 3641 → ∀(f : a → b) 3642 → ∀(p : { _1 : a, _2 : c }) 3643 → { _1 : b, _2 : c } 3644 , identity : 3645 ∀(a : Type) → ∀(x : a) → a 3646 , lmap : 3647 ∀(a : Type) 3648 → ∀(b : Type) 3649 → ∀(c : Type) 3650 → ∀(fn : a → b) 3651 → ∀(fn : b → c) 3652 → ∀(x : a) 3653 → c 3654 , rmap : 3655 ∀(a : Type) 3656 → ∀(b : Type) 3657 → ∀(c : Type) 3658 → ∀(g : b → c) 3659 → ∀(fn : a → b) 3660 → ∀(x : a) 3661 → c 3662 , second : 3663 ∀(a : Type) 3664 → ∀(b : Type) 3665 → ∀(c : Type) 3666 → ∀(f : b → c) 3667 → ∀(p : { _1 : a, _2 : b }) 3668 → { _1 : a, _2 : c } 3669 , split : 3670 ∀(a : Type) 3671 → ∀(b : Type) 3672 → ∀(c : Type) 3673 → ∀(d : Type) 3674 → ∀(f : a → b) 3675 → ∀(g : c → d) 3676 → ∀(p : { _1 : a, _2 : c }) 3677 → { _1 : b, _2 : d } 3678 } 3679 </pre></dd> 3680 </dl> 3681 <h3>profunctor (term)</h3> 3682 <dl> 3683 <dt>type</dt><dd><pre> 3684 { dimap : 3685 ∀(a : Type) 3686 → ∀(b : Type) 3687 → ∀(c : Type) 3688 → ∀(d : Type) 3689 → ∀(f : a → b) 3690 → ∀(g : c → d) 3691 → ∀(fn : b → c) 3692 → ∀(x : a) 3693 → d 3694 , lmap : 3695 ∀(a : Type) 3696 → ∀(b : Type) 3697 → ∀(c : Type) 3698 → ∀(fn : a → b) 3699 → ∀(fn : b → c) 3700 → ∀(x : a) 3701 → c 3702 , rmap : 3703 ∀(a : Type) 3704 → ∀(b : Type) 3705 → ∀(c : Type) 3706 → ∀(g : b → c) 3707 → ∀(fn : a → b) 3708 → ∀(x : a) 3709 → c 3710 } 3711 </pre></dd> 3712 </dl> 3713 <h3>category (term)</h3> 3714 <dl> 3715 <dt>type</dt><dd><pre> 3716 { compose : 3717 ∀(a : Type) 3718 → ∀(b : Type) 3719 → ∀(c : Type) 3720 → ∀(f : b → c) 3721 → ∀(g : a → b) 3722 → ∀(x : a) 3723 → c 3724 , identity : 3725 ∀(a : Type) → ∀(x : a) → a 3726 } 3727 </pre></dd> 3728 </dl> 3729 <h2 style="background-color: #bbb; width: 100%">./Optional</h2> 3730 <h3>monad (term)</h3> 3731 <dl> 3732 <dt>type</dt><dd><pre> 3733 { ap : 3734 ∀(a : Type) 3735 → ∀(b : Type) 3736 → ∀(g : Optional (a → b)) 3737 → ∀(fa : Optional a) 3738 → Optional b 3739 , bind : 3740 ∀(a : Type) 3741 → ∀(b : Type) 3742 → ∀(fa : Optional a) 3743 → ∀(k : a → Optional b) 3744 → Optional b 3745 , map : 3746 ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → ∀(o : Optional a) → Optional b 3747 , pure : 3748 ∀(a : Type) → ∀(x : a) → Optional a 3749 } 3750 </pre></dd> 3751 </dl> 3752 <h3>applicative (term)</h3> 3753 <dl> 3754 <dt>type</dt><dd><pre> 3755 { ap : 3756 ∀(a : Type) 3757 → ∀(b : Type) 3758 → ∀(g : Optional (a → b)) 3759 → ∀(fa : Optional a) 3760 → Optional b 3761 , map : 3762 ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → ∀(o : Optional a) → Optional b 3763 , pure : 3764 ∀(a : Type) → ∀(x : a) → Optional a 3765 } 3766 </pre></dd> 3767 </dl> 3768 <h3>traversable (term)</h3> 3769 <dl> 3770 <dt>type</dt><dd><pre> 3771 { fold : 3772 ∀(a : Type) 3773 → ∀(ts : Optional a) 3774 → ∀(b : Type) 3775 → ∀(f : a → b → b) 3776 → ∀(z : b) 3777 → b 3778 , map : 3779 ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → ∀(o : Optional a) → Optional b 3780 , traverse : 3781 ∀(f : Type → Type) 3782 → ∀ ( applicative 3783 : { ap : 3784 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 3785 , map : 3786 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 3787 , pure : 3788 ∀(a : Type) → a → f a 3789 } 3790 ) 3791 → ∀(a : Type) 3792 → ∀(b : Type) 3793 → ∀(g : a → f b) 3794 → ∀(ts : Optional a) 3795 → f (Optional b) 3796 } 3797 </pre></dd> 3798 </dl> 3799 <h3>functor (term)</h3> 3800 <dl> 3801 <dt>type</dt><dd><pre> 3802 { map : 3803 ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → ∀(o : Optional a) → Optional b 3804 } 3805 </pre></dd> 3806 </dl> 3807 <h3>foldable (term)</h3> 3808 <dl> 3809 <dt>type</dt><dd><pre> 3810 { fold : 3811 ∀(a : Type) 3812 → ∀(ts : Optional a) 3813 → ∀(b : Type) 3814 → ∀(f : a → b → b) 3815 → ∀(z : b) 3816 → b 3817 } 3818 </pre></dd> 3819 </dl> 3820 <h2 style="background-color: #bbb; width: 100%">./docs</h2> 3821 <h2 style="background-color: #bbb; width: 100%">./Tuple</h2> 3822 <h3>Type (type)</h3> 3823 <dl> 3824 <dt>kind</dt><dd><pre> 3825 ∀(a : Type) → ∀(b : Type) → Type 3826 </pre></dd> 3827 <dt>type</dt><dd><pre> 3828 λ(a : Type) → λ(b : Type) → { _1 : a, _2 : b } 3829 </pre></dd> 3830 </dl> 3831 <h3>comonad (term)</h3> 3832 <dl> 3833 <dt>type</dt><dd><pre> 3834 ∀(a : Type) 3835 → { duplicate : 3836 ∀(a : Type) 3837 → ∀(tup : { _1 : a@1, _2 : a }) 3838 → { _1 : a@1, _2 : { _1 : a@1, _2 : a } } 3839 , extend : 3840 ∀(b : Type) 3841 → ∀(c : Type) 3842 → ∀(f : { _1 : a, _2 : b } → c) 3843 → ∀(tup : { _1 : a, _2 : b }) 3844 → { _1 : a, _2 : c } 3845 , extract : 3846 ∀(b : Type) → ∀(tup : { _1 : a, _2 : b }) → b 3847 , map : 3848 ∀(a : Type) 3849 → ∀(b : Type) 3850 → ∀(f : a → b) 3851 → ∀(tup : { _1 : a@1, _2 : a }) 3852 → { _1 : a@1, _2 : b } 3853 } 3854 </pre></dd> 3855 </dl> 3856 <h3>functor (term)</h3> 3857 <dl> 3858 <dt>type</dt><dd><pre> 3859 ∀(a : Type) 3860 → ∀ ( comonad 3861 : { duplicate : 3862 ∀(a : Type) 3863 → { _1 : a@1, _2 : a } 3864 → { _1 : a@1, _2 : { _1 : a@1, _2 : a } } 3865 , extend : 3866 ∀(a : Type) 3867 → ∀(b : Type) 3868 → ∀(f : { _1 : a@1, _2 : a } → b) 3869 → { _1 : a@1, _2 : a } 3870 → { _1 : a@1, _2 : b } 3871 , extract : 3872 ∀(a : Type) → { _1 : a@1, _2 : a } → a 3873 , map : 3874 ∀(a : Type) 3875 → ∀(b : Type) 3876 → ∀(g : a → b) 3877 → ∀(fa : { _1 : a@1, _2 : a }) 3878 → { _1 : a@1, _2 : b } 3879 } 3880 ) 3881 → { map : 3882 ∀(a : Type) 3883 → ∀(b : Type) 3884 → ∀(g : a → b) 3885 → ∀(fa : { _1 : a@1, _2 : a }) 3886 → { _1 : a@1, _2 : b } 3887 } 3888 </pre></dd> 3889 </dl> 3890 <h2 style="background-color: #bbb; width: 100%">./Codensity</h2> 3891 <h3>monad (term)</h3> 3892 <dl> 3893 <dt>type</dt><dd><pre> 3894 ∀(m : Type → Type) 3895 → { ap : 3896 ∀(a : Type) 3897 → ∀(b : Type) 3898 → ∀(f : ∀(b : Type) → ((a → b@1) → m b) → m b) 3899 → ∀(g : ∀(b : Type) → (a → m b) → m b) 3900 → ∀(c : Type) 3901 → ∀(k : b → m c) 3902 → m c 3903 , bind : 3904 ∀(a : Type) 3905 → ∀(b : Type) 3906 → ∀(codensity : ∀(b : Type) → (a → m b) → m b) 3907 → ∀(k : a → ∀(b : Type) → (b@1 → m b) → m b) 3908 → ∀(c : Type) 3909 → ∀(l : b → m c) 3910 → m c 3911 , map : 3912 ∀(a : Type) 3913 → ∀(b : Type) 3914 → ∀(h : a → b) 3915 → ∀(ran : ∀(b : Type) → (a → m b) → m b) 3916 → ∀(c : Type) 3917 → ∀(k : b → m c) 3918 → m c 3919 , pure : 3920 ∀(a : Type) → ∀(x : a) → ∀(b : Type) → ∀(k : a → m b) → m b 3921 } 3922 </pre></dd> 3923 </dl> 3924 <h3>applicative (term)</h3> 3925 <dl> 3926 <dt>type</dt><dd><pre> 3927 ∀(m : Type → Type) 3928 → { ap : 3929 ∀(a : Type) 3930 → ∀(b : Type) 3931 → ∀(f : ∀(b : Type) → ((a → b@1) → m b) → m b) 3932 → ∀(g : ∀(b : Type) → (a → m b) → m b) 3933 → ∀(c : Type) 3934 → ∀(k : b → m c) 3935 → m c 3936 , map : 3937 ∀(a : Type) 3938 → ∀(b : Type) 3939 → ∀(h : a → b) 3940 → ∀(ran : ∀(b : Type) → (a → m b) → m b) 3941 → ∀(c : Type) 3942 → ∀(k : b → m c) 3943 → m c 3944 , pure : 3945 ∀(a : Type) → ∀(x : a) → ∀(b : Type) → ∀(k : a → m b) → m b 3946 } 3947 </pre></dd> 3948 </dl> 3949 <h3>lift (term)</h3> 3950 <dl> 3951 <dt>type</dt><dd><pre> 3952 ∀(f : Type → Type) 3953 → ∀ ( monad 3954 : { ap : 3955 ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b 3956 , bind : 3957 ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(k : a → f b) → f b 3958 , map : 3959 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b 3960 , pure : 3961 ∀(a : Type) → a → f a 3962 } 3963 ) 3964 → ∀(a : Type) 3965 → ∀(x : f a) 3966 → ∀(b : Type) 3967 → ∀(k : a → f b) 3968 → f b 3969 </pre></dd> 3970 </dl> 3971 <h3>Type (type)</h3> 3972 <dl> 3973 <dt>kind</dt><dd><pre> 3974 ∀(m : Type → Type) → ∀(a : Type) → Type 3975 </pre></dd> 3976 <dt>type</dt><dd><pre> 3977 λ(m : Type → Type) → λ(a : Type) → ∀(b : Type) → (a → m b) → m b 3978 </pre></dd> 3979 </dl> 3980 <h3>lower (term)</h3> 3981 <dl> 3982 <dt>type</dt><dd><pre> 3983 ∀(m : Type → Type) 3984 → ∀ ( applicative 3985 : { ap : 3986 ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b 3987 , map : 3988 ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b 3989 , pure : 3990 ∀(a : Type) → a → m a 3991 } 3992 ) 3993 → ∀(a : Type) 3994 → ∀(ran : ∀(b : Type) → (a → m b) → m b) 3995 → m a 3996 </pre></dd> 3997 </dl> 3998 <h3>functor (term)</h3> 3999 <dl> 4000 <dt>type</dt><dd><pre> 4001 ∀(m : Type → Type) 4002 → { map : 4003 ∀(a : Type) 4004 → ∀(b : Type) 4005 → ∀(h : a → b) 4006 → ∀(ran : ∀(b : Type) → (a → m b) → m b) 4007 → ∀(c : Type) 4008 → ∀(k : b → m c) 4009 → m c 4010 } 4011 </pre></dd> 4012 </dl> 4013 </body></html>