[Sorry, I forgot to reply to the list.] Hi.
> I understand these to be Rank 0 terms: > > (\(x::Int) . x) (0 :: Int) :: (forall. Int) -- value > > (\(x::Int). x) :: (forall. Int -> Int) Yes. > (\(x::a). x) :: (forall. a -> a) > > Although the program prints forall, the absence of a type variable > indicates Rank 0, correct? It's a bit unclear what you mean, and the prototype implementation you seem to be using deviates from Haskell conventions here. The prototype checker sees "a" as a type constant here, so it plays the same role as "Int" before. In particular, "a" isn't a type variable, and there's no quantification. > I understand these to be Rank 1 terms: > > (\x. x) :: (forall a. a -> a) -- This is not the same as the third > example above, right? This one identifies the type variable a, the one > above does not. Also, there's no explicit annotation, it's inferred. The implementation indeed considers them to be different. Before "a" was a concrete type, and the function was the monomorphic identity function on that type. Now, "a" is a type variable, and the function is the polymorphic identity function. [...] > I understand these to be Rank 2 terms: > > (\(x::(forall a. a)). 0) :: (forall. (forall a. a) -> Int) > > The explicit forall annotation on the bound and binding variable x > causes the program to infer a Rank 2 polytype as indicated by the "-> > Int" following the (forall a. a), while noting the absence of a type > variable following the left-most forall printed by the program, correct? Your description here is a bit strange. It's a rank-2 type because there's a rank-1 type occurring to the left of the function arrow. > > (\(x::(forall a. a -> a)). x) :: (forall b. (forall a. a -> a) -> b -> > b) > > Also Rank 2, only one arrow to the right of (forall a. a -> a) counts. It's rank 2, yes. I'm not sure what you mean here by saying that only one arrow counts. > The universal quantifier on type variable b ranges over the type > variable a, correct? No. The universal quantifier ranges over all (mono)types. > I understand this to be a Rank 3 term: > > (\(f::(forall a. a -> a)). \(x::(forall b. b)). f (f x)) :: (forall c. > (forall a. a -> a) -> (forall b. b) -> c) No, this is still rank 2. It uses two rank 1 types as function arguments. For it to be rank 3, it'd have to use a rank 2 type in the argument position of a function type. Note that the function arrow associates to the right: forall c. (forall a. a -> a) -> ((forall b. b) -> c) -- rank 2 (forall c. ((forall a. a -> a) -> (forall b. b)) -> c) -- rank 3 > The arrows to the right of the universally quantified a and b > expressions qualify this as Rank 3. No, you seem to be applying a wrong definition of rank. The correct definition is given in Section 3.1 of the paper. Here's how you can derive the type above as a sigma_2: sigma_2 ~> forall c. sigma_2 ~> forall c. sigma_1 -> sigma_2 ~> forall c. sigma_1 -> sigma_1 -> sigma_2 ~> forall c. sigma_1 -> sigma_1 -> sigma_1 ~> forall c. sigma_1 -> sigma_1 -> sigma_0 ~> forall c. sigma_1 -> sigma_1 -> c ~> forall c. (forall a. sigma_1) -> sigma_1 -> c ~> forall c. (forall a. sigma_0) -> sigma_1 -> c ~> forall c. (forall a. tau -> tau) -> sigma_1 -> c ~> forall c. (forall a. a -> a) -> sigma_1 -> c ~> forall c. (forall a. a -> a) -> (forall b. sigma_1) -> c ~> forall c. (forall a. a -> a) -> (forall b. sigma_0) -> c ~> forall c. (forall a. a -> a) -> (forall b. b) -> c > Type variable c ranges over type > variables a and b, correct? No. Each of the type variables ranges over all (mono)types. (Or do you mean what the scope of "c" is? If so, then the scope of c is the complete type signature.) Cheers, Andres -- Andres Löh, Haskell Consultant Well-Typed LLP, http://www.well-typed.com _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
