From 70caa161130de826fdaebf237ab76fc1ff7c821c Mon Sep 17 00:00:00 2001
From: Chris
Date: Mon, 9 Mar 2015 16:10:06 -0400
Subject: [PATCH] edits
---
topics/week5_system_F.mdwn | 19 ++++++++++++++++---
1 file changed, 16 insertions(+), 3 deletions(-)
diff --git a/topics/week5_system_F.mdwn b/topics/week5_system_F.mdwn
index 97b17f83..f89748b7 100644
--- 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
-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 =
@@ -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
-----------------------
--
2.11.0