与Haskell中的map函数等效的Lambda微积分是什么？

问题描述

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

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

解决方法

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

列表通常是可以被编码为解构匹配器：（这是 Scott编码，正如评论所告知的那样）

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结果仍然应该来自原始列表，因此我们需要在此时使用它-args仍然是TBD，但是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，其中包含两个TBD参数：

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作为参数，为此我们有一个正好是{{1} }：

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 ‘\ 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。在标准的lambda演算中，您实际上不能递归地调用定义（您需要使用Fixpoint组合器来模拟它），但是在这里我将忽略它。这是有效的Haskell解决方案：

fmap f

或以lambda样式编写（删除instance Functor (List r) where fmap f (List l) = List $ \nilCs consCs -> l nilCs $ \lHead lTail -> consCs (f lHead) (fmap f lTail) newtype构造函数）

map = \f l ν ζ ⟼ l ν (\h t ⟼ ζ (f h) (map f t))