[Haskell-cafe] sample terms and interpreting program output from Tc Monad
Andres Löh
andres at well-typed.com
Mon Jul 9 13:04:40 CEST 2012
[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
More information about the Haskell-Cafe
mailing list