[Haskell-cafe] sample terms and interpreting program output from Tc Monad

[Andres Löh]

[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