CODEWITHSUNDEEP
haskell
Sal
Sal

Reputation: 4326

Deducing rank from forall quantification

Given the code below (from Yoneda Lemma explanation):

{-# LANGUAGE RankNTypes #-}

check1 :: a -> (forall b . (a -> b) -> b)
check1 a f = f a

uncheck1 :: (forall b . (a -> b) -> b) -> a
uncheck1 t = t id

forall quantification for check1 seems to be rank-1 as confirmed in ghci:

$ :t check1
check1 :: a -> (a -> b) -> b
$ :t uncheck1
uncheck1 :: (forall b. (a -> b) -> b) -> a

I can't figure out why check1 has rank-1 type signature, while uncheck1 still maintains rank-2 type signature. I read the type signature for check1 as "For all types b, accept a function of type a to b where a is fixed, and return a value of type b". That led me to believe that the user is not allowed to select type b in advance (unlike type a), and hence, the type should be rank-2. There seem to be some nuances here that I am definitely missing when trying to learn whether an explicit forall signature should be read as rank-1 or higher rank.

Update: Though I have accepted the answer below, this email explanation from Lennart Augustsson in terms of capital lambda is very clear and intuitive in my opinion - it cuts through the caller-callee confusion, and clearly shows how to do type-level lambda to interpret forall.

Upvotes: 4

Views: 133

Answers (1)

daniel gratzer
daniel gratzer

Reputation: 53891

As it happens we can float at the forall in check1 since it's on the right of that arrow.

 check1 :: a -> (forall b. (a -> b) -> b)
 check1 :: forall b. a -> (a -> b) -> b

An intuition for this, in uncheck1, who get's to choose what b is? Certain not the caller, since that function has to work for all b's.

In check1 the caller does get to choose b, since we have to return a function that works for all b. We're returning the function to them, so they can specialize it to whatever they choose. Since the caller gets to choose anyways, this is exactly equivalent to

check1 :: a -> (a -> b) -> b

The HaskellWiki page discusses this.

Upvotes: 5

Related Questions