edits

diff --git a/topics/week5_system_F.mdwn b/topics/week5_system_F.mdwn
index 97b17f8..f89748b 100644 (file)
--- a/topics/week5_system_F.mdwn
+++ b/topics/week5_system_F.mdwn
@@ -536,9 +536,17 @@ version of the principle 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
 
 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.  When programming interpreters and compilers infer
-types, they often (but not always) aim for the principle type (if one
-is guaranteed to exist).
+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, 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 interpreters and compilers infer types,
+they often (but not always) aim for the principle type (if one is
+guaranteed to exist).

 
     # let pair a b z = z a b;;
     val pair : 'a -> 'b -> ('a -> 'b -> 'c) -> 'c = <fun>
 
     # let pair a b z = z a b;;
     val pair : 'a -> 'b -> ('a -> 'b -> 'c) -> 'c = <fun>


@@ -548,6 +556,11 @@ the OCaml interpreter, it correctly infers the principle type we gave
 above (remember that OCaml doesn't bother giving the explicit
 universal type quantifiers required by System F).
 
 above (remember that OCaml doesn't bother giving the explicit
 universal type quantifiers required by System F).
 

+Computing principle types involves unification algorithms.  Inferring
+types is a subtle and complicated business, and all sorts of
+extensions to a programming language can interfere with it.
+
+

 
 Bottom type, divergence
 -----------------------
 
 Bottom type, divergence
 -----------------------