Haskell 中映射函数的 Lambda 演算等效项是什么？

Question

map 函数返回一个通过将函数（第一个参数）应用于作为第二个参数传递的列表中的所有项目而构造的列表。

我试图弄清楚如果以 Lambda 微积分表示法显示会是什么样子。谁能举个例子？

Answer 1

由于这被标记为haskell，我将在 Haskell 中写下答案，但在函数上构建所有内容，就像在 lambda 演算中一样。这通常会导致为延续传递样式携带一个额外的类型参数r。

列表通常可以编码为解构匹配器：（这是 Scott 编码，正如 cmets 告诉我的那样）

newtype List r a = List { deconstructList
             :: r                    -- ^ `Nil` case
             -> (a -> List r a -> r) -- ^ `Cons` case
             -> r                    -- ^ result
           }

现在我们要给它一个Functor 实例。与其他问题一样，您可以让编译器指导您：

instance Functor (List r) where
  fmap f (List l) = List _

这会提示

LambdaList.hs:8:26: error:
    • Found hole: _ :: r -> (b -> List r b -> r) -> r
      Where: ‘b’ is a rigid type variable bound by
               the type signature for:
                 fmap :: forall a b. (a -> b) -> List r a -> List r b
               at LambdaList.hs:8:3-6
             ‘r’ is a rigid type variable bound by
               the instance declaration
               at LambdaList.hs:7:10-25
    • In the first argument of ‘List’, namely ‘_’
      In the expression: List _
      In an equation for ‘fmap’: fmap f (List l) = List _
    • Relevant bindings include
        l :: r -> (a -> List r a -> r) -> r (bound at LambdaList.hs:8:16)
        f :: a -> b (bound at LambdaList.hs:8:8)
        fmap :: (a -> b) -> List r a -> List r b
          (bound at LambdaList.hs:8:3)
      Valid hole fits include
        const :: forall a b. a -> b -> a
          with const @r @(b -> List r b -> r)
          (imported from ‘Prelude’ at LambdaList.hs:1:1
           (and originally defined in ‘GHC.Base’))
        return :: forall (m :: * -> *) a. Monad m => a -> m a
          with return @((->) (b -> List r b -> r)) @r
          (imported from ‘Prelude’ at LambdaList.hs:1:1
           (and originally defined in ‘GHC.Base’))
        pure :: forall (f :: * -> *) a. Applicative f => a -> f a
          with pure @((->) (b -> List r b -> r)) @r
          (imported from ‘Prelude’ at LambdaList.hs:1:1
           (and originally defined in ‘GHC.Base’))
  |
8 |   fmap f (List l) = List _
  |                          ^

所以我们应该定义一个函数；那么从 lambda 绑定一些参数开始可能是个好主意：

instance Functor (List r) where
  fmap f (List l) = List $ \nilCs consCs -> _

LambdaList.hs:8:45: error:
    • Found hole: _ :: r
      Where: ‘r’ is a rigid type variable bound by
               the instance declaration
               at LambdaList.hs:7:10-25
    • In the expression: _
      In the second argument of ‘($)’, namely ‘\ nilCs consCs -> _’
      In the expression: List $ \ nilCs consCs -> _
    • Relevant bindings include
        consCs :: b -> List r b -> r (bound at LambdaList.hs:8:35)
        nilCs :: r (bound at LambdaList.hs:8:29)
        l :: r -> (a -> List r a -> r) -> r (bound at LambdaList.hs:8:16)
        f :: a -> b (bound at LambdaList.hs:8:8)
        fmap :: (a -> b) -> List r a -> List r b
          (bound at LambdaList.hs:8:3)
      Valid hole fits include nilCs :: r (bound at LambdaList.hs:8:29)

CPS-result 应该仍然来自原始列表，所以我们需要在这一点上使用它 - args 仍然待定，但 nil 大小写不会改变，所以我们也可以立即传递它：

instance Functor (List r) where
  fmap f (List l) = List $ \nilCs consCs -> l nilCs _

LambdaList.hs:8:53: error:
    • Found hole: _ :: a -> List r a -> r
      Where: ‘a’ is a rigid type variable bound by
               the type signature for:
                 fmap :: forall a b. (a -> b) -> List r a -> List r b
               at LambdaList.hs:8:3-6
             ‘r’ is a rigid type variable bound by
               the instance declaration
               at LambdaList.hs:7:10-25
    • In the second argument of ‘l’, namely ‘_’
      In the expression: l nilCs _
      In the second argument of ‘($)’, namely
        ‘\ nilCs consCs -> l nilCs _’
    • Relevant bindings include
        consCs :: b -> List r b -> r (bound at LambdaList.hs:8:35)
        nilCs :: r (bound at LambdaList.hs:8:29)
        l :: r -> (a -> List r a -> r) -> r (bound at LambdaList.hs:8:16)
        f :: a -> b (bound at LambdaList.hs:8:8)
        fmap :: (a -> b) -> List r a -> List r b
          (bound at LambdaList.hs:8:3)

所以又是函数时间，即绑定一些参数：

instance Functor (List r) where
  fmap f (List l) = List
     $ \nilCs consCs -> l nilCs $ \lHead lTail -> _

LambdaList.hs:9:51: error:
    • Found hole: _ :: r
      Where: ‘r’ is a rigid type variable bound by
               the instance declaration
               at LambdaList.hs:7:10-25
    • In the expression: _
      In the second argument of ‘($)’, namely ‘\ lHead lTail -> _’
      In the expression: l nilCs $ \ lHead lTail -> _
    • Relevant bindings include
        lTail :: List r a (bound at LambdaList.hs:9:42)
        lHead :: a (bound at LambdaList.hs:9:36)
        consCs :: b -> List r b -> r (bound at LambdaList.hs:9:15)
        nilCs :: r (bound at LambdaList.hs:9:9)
        l :: r -> (a -> List r a -> r) -> r (bound at LambdaList.hs:8:16)
        f :: a -> b (bound at LambdaList.hs:8:8)
        (Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)
      Valid hole fits include nilCs :: r (bound at LambdaList.hs:9:9)

在这一点上，我们有很多可以使用的范围，但一个好的经验法则是我们应该至少使用一次，所以让我们引入consCs，带有两个待定参数：

instance Functor (List r) where
  fmap f (List l) = List
     $ \nilCs consCs -> l nilCs $ \lHead lTail -> consCs _ _

LambdaList.hs:9:58: error:
    • Found hole: _ :: b
      Where: ‘b’ is a rigid type variable bound by
               the type signature for:
                 fmap :: forall a b. (a -> b) -> List r a -> List r b
               at LambdaList.hs:8:3-6
    • In the first argument of ‘consCs’, namely ‘_’
      In the expression: consCs _ _
      In the second argument of ‘($)’, namely
        ‘\ lHead lTail -> consCs _ _’
    • Relevant bindings include
        lTail :: List r a (bound at LambdaList.hs:9:42)
        lHead :: a (bound at LambdaList.hs:9:36)
        consCs :: b -> List r b -> r (bound at LambdaList.hs:9:15)
        nilCs :: r (bound at LambdaList.hs:9:9)
        l :: r -> (a -> List r a -> r) -> r (bound at LambdaList.hs:8:16)
        f :: a -> b (bound at LambdaList.hs:8:8)
        (Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)

好的，获得b 值的方法只有一种：使用f，它需要a 作为参数，而我们正好有一个，即lHead：

instance Functor (List r) where
  fmap f (List l) = List
     $ \nilCs consCs -> l nilCs
      $ \lHead lTail -> consCs (f lHead) _

LambdaList.hs:9:60: error:
    • Found hole: _ :: List r b
      Where: ‘b’ is a rigid type variable bound by
               the type signature for:
                 fmap :: forall a b. (a -> b) -> List r a -> List r b
               at LambdaList.hs:8:3-6
             ‘r’ is a rigid type variable bound by
               the instance declaration
               at LambdaList.hs:7:10-25
    • In the second argument of ‘consCs’, namely ‘_’
      In the expression: consCs _ _
      In the second argument of ‘($)’, namely
        ‘\ lHead lTail -> consCs _ _’
    • Relevant bindings include
        lTail :: List r a (bound at LambdaList.hs:9:42)
        lHead :: a (bound at LambdaList.hs:9:36)
        consCs :: b -> List r b -> r (bound at LambdaList.hs:9:15)
        nilCs :: r (bound at LambdaList.hs:9:9)
        l :: r -> (a -> List r a -> r) -> r (bound at LambdaList.hs:8:16)
        f :: a -> b (bound at LambdaList.hs:8:8)
        (Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)

这里我们有一点问题：没有List r b 在范围内或在任何绑定的结果中。然而，产生List r b 的是我们刚刚在这里定义的函数：fmap f。在标准 lambda 演算中，您实际上不能递归调用定义（您需要使用定点组合器来模拟它），但我将在这里忽略这一点。这是一个有效的 Haskell 解决方案：

instance Functor (List r) where
  fmap f (List l) = List
     $ \nilCs consCs -> l nilCs
      $ \lHead lTail -> consCs (f lHead) (fmap f lTail)

或者用 lambda 风格编写（删除 List newtype 构造函数），

map = \fl ν ζ ⟼ l ν (\ht ⟼ ζ (fh ) (地图 ft))