On Sunday 06 December 2009 1:42:34 am Eugene Kirpichov wrote:
OK, thanks. However, isn't the type (forall a . a) -> String impredicative because it instantiates a type variable of the type constructor (->) p q with p = forall a . a?
There's probably no clear cut answer to this independent of how you think of (->). For instance, if we explain the Haskell type system by way of a pure type system, (->) is a special case of a pi type, which looks like: pi x : k. t where any xs in t are bound by the pi. We then have: p -> q = pi _ : p. q forall a : k. b = pi a : k. b pi types are given types by sets of rules, which look like triples. If (s,t,u) is a rule, then: G |- k : s G, a : k |- b : t ------------------------------- G |- (pi a : k. b) : u is the corresponding typing rule. Type systems like Haskell's are commonly thought of in terms of the lambda cube, which has constant sorts * and [], with * : []. The rule (*,*,*) gives you ordinary functions. (*,[],[]) gives you dependent types, so that's out. ([],*,*) is an impredicative rule for polymorphism. This says that, for instance: forall a. a -> a = (pi a : *. pi _ : a. a) : * because (pi _ : a. a) : * if a : *, by the (*,*,*) rule, and then we apply the impredicative rule for the universal quantification. One could also use the predicative rule ([],*,[]), which would result in forall a. a -> a having type []. However, Haskell also has arbitrarily higher-order types. This is given by the rule ([],[],[]), which allows expressions like: (* -> *) -> * = pi _ : (pi _ : *. *). * This type system is called F_omega, while just the ([],*,?) rule is known as F_2. However, the F_omega rule also allows for arbitrary rank polymorphism even with the predicative universal quantifier rule above (predicative F_2 allows a little, but it's very limited*). For instance, the higher rank type: forall a. (forall b. b) -> a checks thusly: (forall b. b) : [] via ([],*,[]) ((forall b. b) -> a) : [] via ([],*,[]) (forall a. (forall b. b) -> a) : [] via ([],[],[]) Data types, by contrast, have kinds like * -> *, so using say, Maybe (forall a. a -> a) genuinely relies on the impredicative rule. GHC's type system isn't exactly set up in this way, but (->) is similarly special in that it somehow isn't quite just another type constructor with kind * -> * -> * (or even whatever special kinds GHC uses to support unboxed values and such). Hope that wasn't too confusing. :) -- Dan * Predicative F_2 will essentially allow one universal quantifier somewhere in the type. This can be: forall a. a -> a or it can be: (((forall a. a) -> T) -> U) -> V for T, U and V of kind * (the only kind in F_2), which is a rank-4 type. It doesn't allow: forall a b. a -> b even, because the inner (forall b. a -> b) : [], so adding the forall a requires the F_omega rule. Predicative F_2 and F_w also blow up with quantification on the right of an arrow, because it looks like the rule for dependent types: T -> (forall a. a) T : *, (forall a. a) : [] so the rule (*,[],[]) would be invoked. GHC doesn't have this sort of hierarchy, and so doesn't have these sorts of weird cases, despite being predicative of a sort. Instead it distinguishes somehow between monotypes ([Float], String -> Int, a -> b) and polytypes (forall a. a, ...), although it doesn't really display the difference. Quantifiers are only supposed to range over kinds that classify monotypes (or monotype constructors), which keeps the predicativity (although, even this gets fudged some: If I have forall a. a -> a, I can instantiate a to the polytype forall a. a -> a with rank-n polymorphism, because it only seems to worry about the validity of the resulting type, and (->) is special; by contrast, the same cannot be said for forall a. Maybe a, because Maybe genuinely only accepts monotypes without -XImpredicativeTypes).