+Question: why do thunks work? We know that `blackhole ()` doesn't terminate, so why do expressions like:
+
+ let f = fun () -> blackhole ()
+ in true
+
+terminate?
+
+Bottom type, divergence
+-----------------------
+
+Expressions that don't terminate all belong to the **bottom type**. This is a subtype of every other type. That is, anything of bottom type belongs to every other type as well. More advanced type systems have more examples of subtyping: for example, they might make `int` a subtype of `real`. But the core type system of OCaml doesn't have any general subtyping relations. (Neither does System F.) Just this one: that expressions of the bottom type also belong to every other type. It's as if every type definition in OCaml, even the built in ones, had an implicit extra clause:
+
+ type 'a option = None | Some of 'a;;
+ type 'a option = None | Some of 'a | bottom;;
+
+Here are some exercises that may help better understand this. Figure out what is the type of each of the following:
+
+ fun x y -> y;;
+
+ fun x (y:int) -> y;;
+
+ fun x y : int -> y;;
+
+ let rec blackhole x = blackhole x in blackhole;;
+
+ let rec blackhole x = blackhole x in blackhole 1;;
+
+ let rec blackhole x = blackhole x in fun (y:int) -> blackhole y y y;;
+
+ let rec blackhole x = blackhole x in (blackhole 1) + 2;;
+
+ let rec blackhole x = blackhole x in (blackhole 1) || false;;
+
+ let rec blackhole x = blackhole x in 2 :: (blackhole 1);;
+
+By the way, what's the type of this:
+
+ let rec blackhole (x:'a) : 'a = blackhole x in blackhole
+
+
+Back to thunks: the reason you'd want to control evaluation with thunks is to
+manipulate when "effects" happen. In a strongly normalizing system, like the
+simply-typed lambda calculus or System F, there are no "effects." In Scheme and
+OCaml, on the other hand, we can write programs that have effects. One sort of
+effect is printing (think of the [[damn]] example at the start of term).
+Another sort of effect is mutation, which we'll be looking at soon.
+Continuations are yet another sort of effect. None of these are yet on the
+table though. The only sort of effect we've got so far is *divergence* or
+non-termination. So the only thing thunks are useful for yet is controlling
+whether an expression that would diverge if we tried to fully evaluate it does
+diverge. As we consider richer languages, thunks will become more useful.
+
+
+Towards Monads
+--------------
+
+This has now been moved to the start of [[week7]].
+