dhall-bhat/Compactable/bindEither at 598e210a5688b049a8f081386b62db0d18a6a718 · FormationAI/dhall-bhat · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
{-

bindEither binds to a `f` of Optional over the `f a` and `separate`s `Left`s and `Right`s.

Examples:

```
    let replicate =
          https://raw.githubusercontent.com/dhall-lang/dhall-lang/master/Prelude/List/replicate

in  let Either = ./Either/Type

in  let E = constructors (Either Natural Natural)

in  ./Compactable/bindEither
    List
    ./List/compactable
    ./List/monad
    Natural
    Natural
    (   λ(n : Natural)
      →       if Natural/even n

        then  replicate n (Either Natural Natural) (E.Left n)

        else  replicate n (Either Natural Natural) (E.Right n)
    )
    [ 0, 1, 2, 3, 4, 5 ]
= { _1 = [ 2, 2, 4, 4, 4, 4 ], _2 = [ 1, 3, 3, 3, 5, 5, 5, 5, 5 ] }
```

-}
    let Monad = ./../Monad/Type

in  let Either = ./../Either/Type

in    λ(f : Type → Type)
    → λ(c : ./Type f)
    → λ(monad : Monad f)
    → λ(a : Type)
    → λ(b : Type)
    → λ(k : a → f (Either a b))
    → λ(fa : f a)
    → ./separate f c a b (monad.bind a (Either a b) fa k)