edits

[lambda.git] / topics / week5_system_F.mdwn

diff --git a/topics/week5_system_F.mdwn b/topics/week5_system_F.mdwn
index c37f911..f89748b 100644 (file)
--- 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.  
 
 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>
 
     # 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
 -----------------------