From 70caa161130de826fdaebf237ab76fc1ff7c821c Mon Sep 17 00:00:00 2001 From: Chris Date: Mon, 9 Mar 2015 16:10:06 -0400 Subject: [PATCH 1/1] 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