Lambda微积分等效于Haskell中的map函数吗? [英] What is a Lambda Calculus equivalent of the map function in Haskell?

问题描述

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

The map function returns a list constructed by applying a function (the first argument) to all items in a list passed as the second argument.

我试图弄清楚如果以Lambda Calculus表示法显示的话会是什么样子.有人可以举个例子吗?

I'm trying to figure out what this would look like if displayed in Lambda Calculus notation. Can anyone give an example?

推荐答案

由于已将其标记为 haskell ，因此我将在Haskell中编写答案，但是像在lambda演算中那样构建所有功能.通常，这会为延续传递样式带来一个额外的类型参数 r .

Since this is tagged haskell I'll write the answer in Haskell, but building everything on functions like you would in lambda calculus. This generally incurs carrying around an extra type parameter r for the continuation-passing style.

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

Lists are usually can be encoded as deconstruction-matchers: (this is Scott encoding, as the comments inform me)

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

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

Now we want to give this a Functor instance. As with other problems, you can let the compiler guide you:

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绑定一些参数开始可能是一个好主意:

So we're supposed to define a function; well then it's probably a good idea to start with lambda-binding some arguments:

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的情况不会改变，因此我们也可以立即通过:

The CPS-result should still come from the original list, so we need to use that at this point – with args still TBD, but the nil case won't change so we can right away pass that too:

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)

这又是函数时间，即绑定一些参数:

So it's again function-time, i.e. bind some arguments:

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参数:

At this point we have a lot in scope that could conceivably be used, but a good rule of thumb is that we should probably use all of them at least once, so let's bring in consCs, with two TBD arguments:

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 :

Ok, there's only one way to obtain a b value: using f, which needs an a as its argument, for which we have exactly one, namely 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演算中，您实际上不能递归地调用定义(您需要使用一个Fixpoint组合器来模拟它)，但是在这里我将忽略它.这是有效的Haskell解决方案:

Here we have a bit of a problem: no List r b is in scope or in the result of any of the bindings. However, what does yield a List r b is the function we're just defining here: fmap f. In standard lambda calculus you can't actually recursively call a definition (you need to use a fixpoint combinator to emulate it), but I'll ignore this here. This is a valid Haskell solution:

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构造函数)

Or written in lambda style (erasing the List newtype constructor),

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

这篇关于Lambda微积分等效于Haskell中的map函数吗?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！