如何解决与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))
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。