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