From a1c83924c7d5794bacb0b517f7ad8fae7fb8a5cc Mon Sep 17 00:00:00 2001
From: Chris
Date: Mon, 9 Mar 2015 15:59:53 0400
Subject: [PATCH] added a bit about principle types

topics/week5_system_F.mdwn  56 +++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 55 insertions(+), 1 deletion()
diff git a/topics/week5_system_F.mdwn b/topics/week5_system_F.mdwn
index c20b61c5..c37f9116 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,6 +123,11 @@ 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 principle 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 ≡ âÎ±.(Î±>Î±)>Î±>Î±
.
@@ 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 ω

@@ 182,7 +191,6 @@ type for ω, there is no general type for Ω ≡ ω
strongly normalizing, from which it follows that System F is not
Turing complete.

## Polymorphism in natural language
Is the simplytyped lambda calclus enough for analyzing natural
@@ 495,6 +503,52 @@ Question: why do thunks work? We know that `blackhole ()` doesn't terminate, so
terminate?
+
+Type inference and principle 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`, 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 any function that is ready to handle arguments of the same
+types the pair was built from, and there is no restriction on the type
+(Ï) of the result returned from the pairmanipulation function.
+
+The type we gave the `pair` function above 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 ***principle type***: a type such that
+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).
+
+ # let pair a b z = z a b;;
+ val pair : 'a > 'b > ('a > 'b > 'c) > 'c =
+
+For instance, when we define the same `pair` function given above in
+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).
+
+
Bottom type, divergence


2.11.0