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?

Related: [What is predicativity?](https://stackoverflow.com/a/33093888/791604) To type your term properly, you would need to instantiate one of the type variables of `(.)` with a polymorphic type. — Daniel Wagner, May 24 '20 at 01:49
If you start getting annoyed that you can't predict what can and can't be inferred, a good solution is to make `List` a `newtype List a = List { unList :: forall b. (a -> b -> b) -> b -> b }`. You have to be explicit about wrapping and unwrapping, but things and up being simpler and more predictable as a result. — luqui, May 24 '20 at 08:19

Joseph Sible-Reinstate Monica · Answer 1 · 2020-05-24T01:06:27.960

3

Haskell's type system isn't powerful enough to write map the way you did. Write it like this instead:

map f xs c n = xs (c . f) n

edited May 24 '20 at 01:06

answered May 24 '20 at 00:52

Joseph Sible-Reinstate Monica

45,431
5
48
98

score 2 · Accepted Answer · answered May 24 '20 at 08:17

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.

Your first definition of `map` actually does work if you turn on the `ImpredicativeTypes` extension. — Joseph Sible-Reinstate Monica, May 24 '20 at 16:43
@JosephSible-ReinstateMonica Interesting. Still, that extension is in a bad state right now. Typically GHC error messages suggest to turn the extension on when you are trying to use it, but in this case the error pretends that the extension does not exist. — chi, May 24 '20 at 17:58
The fact that Haskell doesn't really support impredicativity answers my question. I know how `newtype` is used in practice and wanted to see how far `type` can be pushed with `RankNTypes` because it gives rise to interesting generalizations, like `return id` for `[]`, `Nothing` and `0` in Curch encoding. — Marvin, May 25 '20 at 15:58

Functoriality of List in Pure Haskell Lambda Calculus

2 Answers2