X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;ds=sidebyside;f=topics%2Fweek5_system_F.mdwn;h=f89748b74e2f1f62dd20f1097ceb86b4222adf70;hb=70caa161130de826fdaebf237ab76fc1ff7c821c;hp=c37f9116e0ec081ddccefce935fc6614c2abf43d;hpb=a1c83924c7d5794bacb0b517f7ad8fae7fb8a5cc;p=lambda.git

diff --git a/topics/week5_system_F.mdwn b/topics/week5_system_F.mdwn
index c37f9116..f89748b7 100644
--- a/topics/week5_system_F.mdwn
+++ b/topics/week5_system_F.mdwn
@@ -534,11 +534,19 @@ 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).
+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, 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>
@@ -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).
 
+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
 -----------------------