How to infer the type of the Scott encoded List constructor?

Question

Scott encoded lists can be defined as followed:

newtype List a =
    List {
      uncons :: forall r. r -> (a -> List a -> r) -> r
    }

As opposed to the ADT version List is both type and data constructor. Scott encoding determines ADTs through pattern matching, which essentially means removing one layer of constructors. Here is the full uncons operation without implicit arguments:

uncons :: r -> (a -> List a -> r) -> List a -> r
--    Nil ^    ^^^^^^^^^^^^^^^^^^ Cons
uncons nil cons (List f) = f nil cons

This makes perfect sense. uncons takes a constant, a continuation and a List and produces whatever value.

The type of the data constructor, however, doesn't make much sense to me:

List :: (forall r. r -> (a -> List a -> r) -> r) -> List a

I see that r has its own scope but this isn't very helpful. Why are r and List a flipped compared to uncons? And why are there additional parentheses on the LHS?

I'm probably muddling up type and term level here..

Answer 1

What is a List? As you say, it's a thing that, when provided with a constant (what to do if the list is empty) and a continuation (what to do if the list is non-empty), does one of those things. In types, it takes an r and a a -> List a -> r and produces an r.

So, how do we make a list? Well, we need the function that underlies this behavior. That is, we need a function that itself takes the r and the a -> List a -> r and does something with them (presumably, either returning the r directly or calling the function on some a and List a). The type of that would look something like:

List :: (r -> (a -> List a -> r) -> r) -> List a
--         ^ the function that _takes_ the nil and continuation and does stuff with them

But, this isn't quite right, which becomes clear if we use explicit forall:

List :: forall a r. (r -> (a -> List a -> r) -> r) -> List a

Remember, List should be able to work for any r, but with this function, the r is actually provided ahead of time. Indeed, there's nothing wrong with someone specializing this type to, say, Int, resulting in:

List :: forall a. (Int -> (a -> List a -> Int) -> Int) -> List a

But this is no good! This List would only ever be able to produce Ints! Instead, we put the forall inside the first set of parentheses, indicating that the creator of a List must provide a function that can work on any r rather than a particular one. This yields the type:

List :: (forall r. r -> (a -> List a -> r) -> r) -> List a

Answer 2

^{(Moved my comment to this answer as requested.)}

Given

newtype List a =
    List {
      uncons :: forall r. r -> (a -> List a -> r) -> r
    }

let us write down some lists. Note that lists are essentially functions of two parameters (\nil cons -> ...).

-- []
empty = List (\nil _ -> nil)

-- [True]
-- True : []
-- (:)  True []
-- cons True nil
list1 = List (\_ cons -> cons True (List (\nil _ -> nil)))

-- [True, False]
-- True : False : []
-- (:)  True ((:)  False [])
-- cons True (cons False nil)
list2 = List (\_ cons -> 
           cons True (List (\_ cons' -> 
               cons' False (List (\nil _ -> nil)))))