What is the rank of a polymorphic type?
Hello. Consider the type: (forall a . a) -> String. On one hand, it is rank-2 polymorphic, because it abstracts over a rank-1 polymorphic type. On the other hand, it is monomorphic because it isn't actually quantified itself: in my intuitive view, a parametrically polymorphic type has infinitely many instantiations (for example, Int -> Int is an instantiation of forall a . a -> a, and String -> String also is), and this type doesn't have any instantiations at all. Which is correct? Is there really a contradiction? What is the definition of rank of a polymorphic type? -- Eugene Kirpichov Web IR developer, market.yandex.ru
Eugene Kirpichov wrote:
Hello.
Consider the type: (forall a . a) -> String.
On one hand, it is rank-2 polymorphic, because it abstracts over a rank-1 polymorphic type. On the other hand, it is monomorphic because it isn't actually quantified itself: in my intuitive view, a parametrically polymorphic type has infinitely many instantiations (for example, Int -> Int is an instantiation of forall a . a -> a, and String -> String also is), and this type doesn't have any instantiations at all.
Which is correct? Is there really a contradiction? What is the definition of rank of a polymorphic type?
There's a nice paper about this: Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich and Mark Shields "Practical type inference for arbitrary-rank types" http://research.microsoft.com/en-us/um/people/simonpj/papers/higher-rank/put... Section 3.1 of that paper defines what rank types have: "The rank of a type describes the depth at which universal quantifiers appear contravariantly" Looking at the examples that are then given I'd say your example has rank 2 (but I'm no expert). It only mentions the depth of the forall, not whether it has any instantiations. HTH, Martijn.
Eugene,
Consider the type: (forall a . a) -> String.
It's of rank 2.
What is the definition of rank of a polymorphic type?
The minimal rank of a type is given by rank (forall a. t) = 1 `max` rank t rank (t -> u) = (if rank t == 0 then 0 else rank t + 1) `max` rank u rank _ = 0 HTH, Stefan
2009/12/5 Stefan Holdermans
Eugene,
Consider the type: (forall a . a) -> String.
It's of rank 2.
What is the definition of rank of a polymorphic type?
The minimal rank of a type is given by
rank (forall a. t) = 1 `max` rank t rank (t -> u) = (if rank t == 0 then 0 else rank t + 1) `max` rank u rank _ = 0
Thanks! 1) Does there exist an authoritative source saying the same? Not that I'm doubting, just supposing that the source would have other interesting information, too :) 2) Is it true that rank (forall a . a, forall a . a) == 0 ?
HTH,
Stefan
-- Eugene Kirpichov Web IR developer, market.yandex.ru
Eugene,
1) Does there exist an authoritative source saying the same? Not that I'm doubting, just supposing that the source would have other interesting information, too :)
You may want to have a look at the already mentioned JFP-article by Peyton Jones et al. and perhaps the work of Kfoury and Wells.
2) Is it true that rank (forall a . a, forall a . a) == 0 ?
No, for pairs one takes the maximum of the constituent types. So, here you'd get rank 1. Note that this is an impredicative type, which is yet another extension of the standard Hindley-Milner typing discipline. Cheers, Stefan
2009/12/6 Stefan Holdermans
Eugene,
1) Does there exist an authoritative source saying the same? Not that I'm doubting, just supposing that the source would have other interesting information, too :)
You may want to have a look at the already mentioned JFP-article by Peyton Jones et al. and perhaps the work of Kfoury and Wells.
2) Is it true that rank (forall a . a, forall a . a) == 0 ?
No, for pairs one takes the maximum of the constituent types. So, here you'd get rank 1.
Note that this is an impredicative type, which is yet another extension of the standard Hindley-Milner typing discipline.
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?
Cheers,
Stefan
-- Eugene Kirpichov Web IR developer, market.yandex.ru
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).
Apologies for the double-reply... Your mail prompted me to finally get around to adding a mono/polytype system to an interpreter I've been working on for pure type systems, to see what a GHC-alike type system would look like. Here's what I came up with. Constants are: *m, []m, *p and []p Axioms are: *m : []m, *p : []p Rules go as follows: (*m,*m,*m) This is obvious, because it allows normal functions. ([]m,[]m,[]m) This gives arbitrary order type constructors (that is, it expands the m-kinds to km ::= *m | km -> km) ([]m,*m,*p) ([]m,*p,*p) These allows quantification over types. Note that if you erase the mono/poly distinctions, you get the single rule ([],*,*), which is the impredicative rule for the lambda cube. However, this system tracks a distinction, so it remains predicative (universal quantifiers don't range over types that contain universal quantifiers). With just these rules, I think we accept just the types valid in ordinary Haskell. We have higher order types, but we can only have polytypes in prenex normal form, because quantification sticks a type into *p, and the only thing we can do with a *p is add more quantifiers (over []m) to the beginning.r To get rank-n types back, we need to be able to write functions that accept and return polytypes as arguments. This corresponds to the rules: (*m,*p,*p) (*p,*m,*p) (*p,*p,*p) Note that []p never appears in our rules; it exists only to give *p a type (which may not strictly be necessary, even, but it doesn't hurt). Data types would have kinds like: Maybe : *m -> *m and so types like Maybe (forall a. a -> a) would be invalid, because it's trying to use the type constructor with a *p. This type system is a bit stricter than the one GHC uses for rank-n types, as if you have: id : forall a : *m. a -> a You cannot instantiate a to forall a. a -> a, because it has kind *p. GHC allows that sort of impredicative instantiation with just rank-n types turned on. As alluded to earlier, one can recover an ordinary impredicative F_w by erasing the mono/poly distinctions. The rules collapse to: (*,*,*) ([],*,*) ([],[],[]) If anyone's interested in playing with the checker, it can be found at http://code.haskell.org/~dolio/ in the pts repository (I'll try to get a little documentation for the REPL uploaded). And let me know if you find something that types but shouldn't, or some such nonsense. Cheers, -- Dan
On Sun, Dec 6, 2009 at 8:39 AM, Dan Doel
Apologies for the double-reply...
Your mail prompted me to finally get around to adding a mono/polytype system to an interpreter I've been working on for pure type systems, to see what a GHC-alike type system would look like. Here's what I came up with.
Have you read "Henk: a typed intermediate language" by Simon Peyton
Jones and Erik Meijer? In section 4, they describe a PTS very similar
to yours.
http://research.microsoft.com/en-us/um/people/emeijer/Papers/Henk.pdf
--
Dave Menendez
participants (5)
-
Dan Doel -
David Menendez -
Eugene Kirpichov -
Martijn van Steenbergen -
Stefan Holdermans