How to infer the type of the Scott encoded List constructor?
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 Int
s! 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