From: Chris Date: Mon, 9 Mar 2015 20:10:06 +0000 (-0400) Subject: edits X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=70caa161130de826fdaebf237ab76fc1ff7c821c;hp=fec31e5e99518d29570360ef74ff870284fc0114 edits --- 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 -----------------------