haskellfunctional-programmingalgebraic-data-typeshigher-rank-typesscott-encoding

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


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


Solution

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