X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2Fweek5_system_F.mdwn;h=fabb868b4831c0ff44a1209185d43240aba4bd87;hp=36c071cd9e305f2f9ac1e0edc2e2a7daf8c2e1d1;hb=a0eb18e702862266fdc8a7d935d6cc33821fdf4a;hpb=6a0ec687459f0862571cccde6bb2529ca06dd568

diff --git a/topics/week5_system_F.mdwn b/topics/week5_system_F.mdwn
index 36c071cd..fabb868b 100644
--- a/topics/week5_system_F.mdwn
+++ b/topics/week5_system_F.mdwn
@@ -1,3 +1,6 @@
+<!-- λ Λ ∀ ≡ α β ρ ω Ω -->
+
+
 [[!toc levels=2]]
 
 # System F: the polymorphic lambda calculus
@@ -120,9 +123,14 @@ reserved words in Pierce's system.]
 
 Exercise: convince yourself that `zero` has type `N`.
 
+[By the way, in order to keep things as simple as possible here, the
+types used in this definition of the ancillary functions given here
+are not as general as they could be; see the discussion below of type
+inference and principal types in the OCaml type system.]
+
 The key to the extra expressive power provided by System F is evident
 in the typing imposed by the definition of `pred`.  The variable `n`
-is typed as a Church number, i.e., as `N &equiv; ∀α.(α->α)->α->α`.
+is typed as a Church number, i.e., as <code>N &equiv; ∀α.(α->α)->α->α</code>.
 The type application `n [Pair]` instantiates `n` in a way that allows
 it to manipulate ordered pairs: `n [Pair]: (Pair->Pair)->Pair->Pair`.
 In other words, the instantiation turns a Church number into a certain
@@ -144,6 +152,7 @@ entirely from explicit base types, we'd be unable to proceed.
 [See Benjamin C. Pierce. 2002. *Types and Programming Languages*, MIT
 Press, chapter 23.]
 
+
 Typing &omega;
 --------------
 
@@ -182,7 +191,6 @@ type for &omega;, there is no general type for &Omega; &equiv; &omega;
 strongly normalizing, from which it follows that System F is not
 Turing complete.
 
-
 ## Polymorphism in natural language
 
 Is the simply-typed lambda calclus enough for analyzing natural
@@ -495,6 +503,66 @@ Question: why do thunks work? We know that `blackhole ()` doesn't terminate, so
 
 terminate?
 
+
+Type inference and principal types
+----------------------------------
+
+As we mentioned, the types given to some of the functions defined
+above in the System F definition of `pred` are not as general as they
+might be.  
+
+    let pair = λx:N. λy:N. λz:N->N->N. z x y in
+    ...
+
+For instance, in the definition of `pair`, repeated here, we assumed
+that the function `z` would return something of type `N`, i.e., a
+Church number.  But we can give a more general treatment.
+
+    let general_pair = Λα. Λβ. λx:α. λy:β. Λρ. λz:α->β->ρ. z x y in
+    ...
+
+In this more general version, the pair function accepts any kind of
+objects as its first and second element.  The resulting pair will
+expect a handler function (`z`) that is ready to handle arguments of
+the same types the pair was built from, but there is no restriction on
+the type (ρ) of the result returned by the handler function.
+
+The number specific type we gave the `pair` function above (i.e.,
+`N->N->(N->N->N)->N`) is a specific instance of the more general type,
+with `α`, `β`, and `ρ` all set to `N`.  Many practical type systems
+guarantee that under reasonably general conditions, there will be a
+***principal type***: a type such that every other possible type for
+that expression is a more specific version of the principal 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.  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, reliably inferring types is not always possible.  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 language interpreters and compilers infer types, they
+often (but not always) aim for the principal type (if one is
+guaranteed to exist).
+
+    # let pair a b z = z a b;;
+    val pair : 'a -> 'b -> ('a -> 'b -> 'c) -> 'c = <fun>
+
+For instance, when we define the same `pair` function given above in
+the OCaml interpreter, it correctly infers the principal type we gave
+above (remember that OCaml doesn't bother giving the explicit
+universal type quantifiers required by System F).
+
+Computing principal 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
 -----------------------