纯Haskell Lambda微积分中的列表的功能

我正在尝试使用Haskell在纯lambda演算中实现各种功能。 一切正常

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

导致此错误消息:

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

评论
  • Avery
    Avery 回复

    You need to enable the RankNTypes extension, or your type synonym won't mean what you want it to mean. (IMO, it's a wart in Haskell that without that extension, it accepts your synonym with the wrong meaning instead of rejecting it.)

    You may also want to consider using a newtype wrapper instead of type, like this:

    {-# LANGUAGE RankNTypes #-}
    
    newtype List a = List (forall b. (a -> b -> b) -> b -> b)
    
    empty :: List a
    empty = List $ const id
    
    cons :: a -> List a -> List a
    cons x (List xs) = List $ \f y -> f x (xs f y)
    

    以免您在将来尝试对列表进行更多处理时遇到对可干扰性的缺乏支持。