Functoriality of List in Pure Haskell Lambda Calculus

Question

I'm trying to implement various things in pure lambda calculus with Haskell. Everything works fine

{-# LANGUAGE RankNTypes #-}

type List a = forall b. (a -> b -> b) -> b -> b

empty :: List a
empty = const id

cons :: a -> List a -> List a
cons x xs f y = f x (xs f y)

until map for List comes along.

map :: (a -> b) -> List a -> List b
map f xs = xs (cons . f) empty

Leads to this error message:

• Couldn't match type ‘List b’ with ‘(b -> b1 -> b1) -> b1 -> b1’
  Expected type: b
                 -> ((b -> b1 -> b1) -> b1 -> b1) -> (b -> b1 -> b1) -> b1 -> b1
    Actual type: b -> List b -> List b
• In the first argument of ‘(.)’, namely ‘cons’
  In the first argument of ‘xs’, namely ‘(cons . f)’
  In the expression: xs (cons . f) empty
• Relevant bindings include
    f :: a -> b (bound at Basic.hs:12:5)
    map :: (a -> b) -> List a -> List b (bound at Basic.hs:12:1)

Why does cons work and map not? Shouldn't every instance of List work for every value of b since it's bound by forall?

Answer 1

The issue is that, for your map to work, you need to choose the quantified type variable b in the List a type to be List b (this is the "other" b you used, which is not the same type variable). Assigning a forall type to a type variable requires impredicativity, which GHC does not support.

Here I try to force the instantiation of that b as we need by calling xs as xs @(List b) .... using an explcit type application.

map :: forall a b. (a->b) -> List a -> List b
map f xs = xs @(List b) (cons . f) empty

error:
    * Illegal polymorphic type: List b
      GHC doesn't yet support impredicative polymorphism
    * In the expression: xs @(List b) (cons . f) empty
      In an equation for `map': map f xs = xs @(List b) (cons . f) empty

A possible solution is to wrap List a in a newtype, and perform the wrapping/unwrapping manually.

newtype L a = L { unL :: List a }

map :: forall a b. (a->b) -> List a -> List b
map f xs =  unL $ xs @(L b) (\y ys -> L (cons (f y) (unL ys))) (L empty)

The code gets littered with Ls and unLs, but it's the same code.

Joseph Sible above suggested a simpler solution, which does not require to pass polymorphically typed values around.