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

6
votes

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..

2
haskellfunctional-programmingalgebraic-data-typeshigher-rank-typesscott-encoding
That's not the type of uncons. If you look at its actual type, you see List and uncons are just inverses (List :: something -> something else; uncons :: something else -> something). – HTNW
"Here is the full uncons operation without implicit arguments" - where did you get that from? The "implicit argument" List a comes first, and produces the type of the "field". – Bergi
I should have called the standalone version uncons'. It is not meant to be the written out version of the newtype declaration. I put the List argument at the end for convenience. List's type still doesn't make sense to me. It is a type level lambda which takes another type level lambda as an argument and produces a list. I cannot make the connection to the term level. – Iven Marquardt
@scriptum In cons True nil the second parameter needs to be a list (but nil is not a list!). Lists are functions of two parameters \nil _ -> nil would be a list. Putting it together results in: List (\_ cons -> cons True (List (\nil _ -> nil))) – Micha Wiedenmann
related search. related Q (and the comments under the answer). – Will Ness

2 Answers

5
votes

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
2
votes

(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)))))