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 simply-typed 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 pair-manipulation 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