纯哈斯克尔Lambda微积分中列表的向量性

Question

我正在尝试用Haskell实现纯lambda微积分中的各种事情，一切都很好。

{-# 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)

直到 map 对于 List 来了。

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

导致了这个错误信息。

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

为什么 cons 工作和 map 不是吗？是不是每一个实例都应该是 List 屡试不爽 b 因为它受 forall?

Answer 1

问题是，为了让你的映射工作，你需要选择量化的类型变量。b 在 List a 类型 List b (这是 "另一个") b 的类型变量）。) 赋予一个 forall 类型到一个类型变量需要不可知性，而GHC不支持。

在这里，我试图强制实例化那个 b 所谓 xs 作为 xs @(List b) .... 使用explcit类型的应用程序。

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

一个可能的解决方案是将 List a 在...中 newtype，并手动执行wrappingunwrapping。

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)

代码中会有大量的 Ls和 unL的，但这是同样的代码。

上面Joseph Sible提出了一个更简单的解决方案，它不需要把多态类型的值传来传去。

Answer 2

Haskell的类型系统不够强大，无法写出 map 你的方式。改成这样写。

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