Post History

> when I look at the type signatures, it is not supposed to work.

The types work because they're parameterized. The types of the combinators involved are (renaming all parameters to be unique for clarity):

```
id : 'a -> 'a
switch : ('b -> 'c) -> 'b -> Result<'c, 'err>
(>=>) :
  ('d -> Result<'e, 'err>) ->
  ('e -> Result<'f, 'err>) ->
  ('d -> Result<'f, 'err>)
map : ('x -> 'y) -> Result<'x, 'err> -> Result<'y, 'err>
```

When `(>=>) id` is type checked, `'d` must unify with `'a`, and `Result<'e, 'err>` must also unify with `'a`. Since `'a` and `'d` are currently unknown, this is fine; we simply define them both to be equal to `Result<'e, 'err>`, with the specialized type of `(>=>)` now
```
(>=>) : // (specialized)
  (Result<'e, 'err> -> Result<'e, 'err>) ->
  ('e -> Result<'f, 'err>) ->
  (Result<'e, 'err> -> Result<'f, 'err>)
```

For the second argument, we have `switch f`, which (inside the definition of `map`, where `f : 'x -> 'y`) has type `'x -> Result<'y, 'err>`. This is a much simpler match: define `'e` to be `'x` and `'f` to be `'y`.

So the final type of `id >=> switch f` is `Result<'x, 'err> -> Result<'y, 'err>`, which is exactly what the result of `map f` should be.

> This is how I would think evaluation goes, but apparently this is not it:
>
> ```
> id >=>> switch ((+) 2)
>           |
>           V
> (>=>>) id (switch ((+) 2))
>           |
>           V
>     match (id x) with
>     |    Ok o -> (switch ((+) 2)) o
>     | Error e -> Error e
> ```

No, that looks right! Keep going:
```
    match x with
    |    Ok o -> (switch ((+) 2)) o
    | Error e -> Error e
         |
         V
    match x with
    |    Ok o -> Ok (2 + o)
    | Error e -> Error e
```
which is exactly what `map ((+) 2)` should do.

Of course the reductions under the match clauses don't happen until that branch is reached, but that doesn't stop us from performing them ahead of time to show that they're equivalent to a different expression.