-expect any function that is ready to handle arguments of the same
-types the pair was built from, and there is no restriction on the type
-(ρ) of the result returned from the pair-manipulation function.
-
-The type we gave the `pair` function above is a specific instance of
-the more general type, with `α`, `β`, and `ρ` all set to `N`.
-Many practical type systems guarantee that under reasonably general
-conditions, there will be a ***principle type***: a type such that
-every other possible type for that expression is a more specific
-version of the principle type.
-
-As we have seen, it is often possible to infer constraints on the type
-of an expression based on its internal structure, as well as by the
-way in which it is used. When programming interpreters and compilers
-infer types, they often (but not always) aim for the principle type
-(if one is guaranteed to exist).
+expect a handler function (`z`) that is ready to handle arguments of
+the same types the pair was built from, but there is no restriction on
+the type (ρ) of the result returned by the handler function.
+
+The number specific type we gave the `pair` function above (i.e.,
+`N->N->(N->N->N)->N`) is a specific instance of the more general type,
+with `α`, `β`, and `ρ` all set to `N`. Many practical type systems
+guarantee that under reasonably general conditions, there will be a
+***principal type***: a type such that every other possible type for
+that expression is a more specific version of the principal type.
+
+As we have seen, it is often possible to infer a type for an
+expression based on its internal structure, as well as by the way in
+which it is used. In the simply-typed lambda calculus, types for a
+well-typed expression can always be inferred; this is what enables
+programs to be written "Curry-style", i.e., without explicit types.
+
+Unfortunately, reliably inferring types is not always possible. For
+unrestricted System F, type inference is undecidable, so a certain
+amount of explicit type specification is required. OCaml places
+restrictions on its type system that makes type inference feasible.
+
+When programming language interpreters and compilers infer types, they
+often (but not always) aim for the principal type (if one is
+guaranteed to exist).