true ≡ Λα. λy:α. λn:α. y
false ≡ Λα. λy:α. λn:α. n
not ≡ λp:Bool. p [Bool] false true
- and ≡ λp:Bool. λq:Bool. p [Bool] (q [Bool]) false
- or ≡ λp:Bool. λq:Bool. p [Bool] true (q [Bool])
+ and ≡ λp:Bool. λq:Bool. p [Bool] q false
+ or ≡ λp:Bool. λq:Bool. p [Bool] true q
+
+ When I first wrote up these answers, I had put `(q [Bool])` where I now have just `q` in the body of `and` and `or`. On reflection,
+ this isn't necessary, because `q` is already a `Bool`. But as I learned by checking these answers with Pierce's evaluator, it's
+ also a mistake. What we want is a result whose type _is_ `Bool`, that is, `∀α. α -> α -> α`. `(q [Bool])` doesn't have that type, but
+ rather the type `Bool -> Bool -> Bool`. The first, desired, type has an outermost `∀`. The second, wrong type doesn't; it only has `∀`s
+ inside the antecedents and consequents of the various arrows. The last one of those could be promoted to be an outermost `∀`, since
+ `P -> ∀α. Q ≡ ∀α. P -> Q` when `α` is not free in `P`. But that couldn't be done with the others.
The type `Nat` (for "natural number") may be encoded as follows:
-- Or this:
let sysf_true = (\y n -> y) :: Sysf_bool a
- :set -XExplicitForAll
+ Note that in both OCaml and Haskell code, the generalization `∀α` on the free type variable `α` is implicit. If you really want to, you can supply it explicitly in Haskell by saying:
+
+ :set -XExplicitForAll
let { sysf_true :: forall a. Sysf_bool a; ... }
-- or
let { sysf_true :: forall a. a -> a -> a; ... }
type 'a notok = 'a -> 'a notok
- (In the technical jargon, OCaml has isorecursive not equirecursive types.) In any case, the reason that OCaml rejects b, e, and g is not the mere fact that they involve self-application, but the fact that typing them would require constructing one of the kinds of infinite chains of unbroken arrows that OCaml forbids. In case c, we can already see that the type of `f` is acceptable (it was ok in case a), and the self-application doesn't impose any new typing constraints because it never returns, so it can have any result type at all.
+ (In the technical jargon, OCaml has isorecursive not equirecursive types.) In any case, the reason that OCaml rejects b is not the mere fact that it involves self-application, but the fact that typing it would require constructing one of the kinds of infinite chains of unbroken arrows that OCaml forbids. In case c, we can already see that the type of `f` is acceptable (it was ok in case a), and the self-application doesn't impose any new typing constraints because it never returns, so it can have any result type at all.
- In case g, the typing fails not specifically because of a self-application, but because OCaml has already determined that `f` has to take a `()` argument, and even before settling on `f`'s final type, one thing it knows about `f` is that it isn't `()`. So `let rec f () = f () in f f` fails for the same reason that `let rec f () = f () in f id` would.
+ In cases e and g, the typing fails not specifically because of a self-application, but because OCaml has already determined that `f` has to take a `()` argument, and even before settling on `f`'s final type, one thing it knows about `f` is that it isn't `()`. So `let rec f () = f () in f f` fails for the same reason that `let rec f () = f () in f id` would.
24. Throughout this problem, assume that we have:
m. let _ = blackhole in 2
n. let _ = blackhole () in 2
- ANSWERS: These terminate: a,c,e,f,g,j,m; these don't: b,d,h,i,k,l,n. Generalization: blackhole is a suspended infinite loop, that is forced by feeding it an argument. The expressions that feed blackhole an argument (in a context that is not itself an unforced suspension) won't terminate.
+ ANSWERS: These terminate: a,c,e,f,g,j,m; these don't: b,d,h,i,k,l,n. Generalization: blackhole is a suspended infinite loop, that is forced by feeding it an argument. The expressions that feed blackhole an argument (in a context that is not itself an unforced suspension) won't terminate. Also, unselected clauses of `if`-terms aren't ever evaluated.
25. This problem aims to get you thinking about how to control order of evaluation.
Here is an attempt to make explicit the behavior of `if ... then ... else ...` explored in the previous question.
match b with true -> y () | false -> n ()
that would arguably still be relying on the special evaluation order properties of OCaml's native `match`. You'd be assuming that `n ()` wouldn't be evaluated in the computation that ends up selecting the other branch. Your assumption would be correct, but to avoid making that assumption, you should instead first select the `y` or `n` result, _and then afterwards_ force the result. That's what we do in the above answer.
+
+ Question: don't the rhs of all the match clauses in `match b with true -> y | false -> n` have to have the same type? How can they, when one of them is `blackhole` and the other is `blackhole ()`? The answer has two parts. First is that an expression is allowed to have different types when it occurs several times on the same line: consider `let id x = x in (id 5, id true)`, which evaluates just fine. The second is that `blackhole` will get the type `'a -> 'b`, that is, it can have any functional type at all. So the principle types of `y` and `n` end up being `y : unit -> 'a -> 'b` and `n : unit -> 'c`. (The consequent of `n` isn't constrained to use the same type variable as the consequent of `y`.) OCaml can legitimately infer these to be the same type by unifying the types `'c` and `'a -> 'b`; that is, it instantiates `'c` to the functional type had by `y ()`.