however, we won't have an `'a`; we'll have a pair whose first element
is an `'a`. So we have to unpack the pair:
- ... let (a, s') = u s in ... (f a) ...
+ ... let (a, s') = u s in ... f a ...
Abstracting over the `s` and adjusting the types gives the result:
... u (fun (a : 'a) (b : 'b) -> ... f a ... ) ...
-In order for `u` to have the kind of argument it needs, the `fun a b -> ... f a ...` has to have type `'a -> 'b -> 'b`; so the `... f a ...` has to evaluate to a result of type `'b`. The easiest way to do this is to collapse (or "unify") the types `'b` and `'d`, with the result that `f a` will have type `('c -> 'b -> 'b) -> 'b -> 'b`. Let's postulate an argument `k` of type `('c -> 'b -> 'b)` and supply it to `(f a)`:
+In order for `u` to have the kind of argument it needs, the `fun a b -> ... f a ...` has to have type `'a -> 'b -> 'b`; so the `... f a ...` has to evaluate to a result of type `'b`. The easiest way to do this is to collapse (or "unify") the types `'b` and `'d`, with the result that `f a` will have type `('c -> 'b -> 'b) -> 'b -> 'b`. Let's postulate an argument `k` of type `('c -> 'b -> 'b)` and supply it to `f a`:
... u (fun (a : 'a) (b : 'b) -> ... f a k ... ) ...