((->)r)类型的适用法律 [英] Applicative Laws for the ((->) r) type
问题描述
我正在尝试检查适用法律是否适用于函数类型((->) r)
,这是我到目前为止所拥有的:
I'm trying to check that the Applicative laws hold for the function type ((->) r)
, and here's what I have so far:
-- Identiy
pure (id) <*> v = v
-- Starting with the LHS
pure (id) <*> v
const id <*> v
(\x -> const id x (g x))
(\x -> id (g x))
(\x -> g x)
g x
v
-- Homomorphism
pure f <*> pure x = pure (f x)
-- Starting with the LHS
pure f <*> pure x
const f <*> const x
(\y -> const f y (const x y))
(\y -> f (x))
(\_ -> f x)
pure (f x)
我是否正确执行了前两个定律的步骤?
Did I perform the steps for the first two laws correctly?
我正在努力与&组成法.对于交换,到目前为止,我有以下内容:
I'm struggling with the interchange & composition laws. For interchange, so far I have the following:
-- Interchange
u <*> pure y = pure ($y) <*> u
-- Starting with the LHS
u <*> pure y
u <*> const y
(\x -> g x (const y x))
(\x -> g x y)
-- I'm not sure how to proceed beyond this point.
我希望为验证Interchange& amp;的步骤提供任何帮助. ((->) r)
类型的成分适用法律.供参考,《组成法》的适用法律如下:
I would appreciate any help for the steps to verify the Interchange & Composition applicative laws for the ((->) r)
type. For reference, the Composition applicative law is as follows:
pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
推荐答案
我认为,在您的身份"证明中,您应该在任何地方都用v
替换g
(否则,g
以及它来自何处) ?).同样,到目前为止,在交换"证明中,一切看起来还不错,但是神奇出现的g
应该只是u
.要继续证明,您可以开始降低RHS并确认它还会产生\x -> u x y
.
I think in your "Identity" proof, you should replace g
with v
everywhere (otherwise what is g
and where did it come from?). Similarly, in your "Interchange" proof, things look okay so far, but the g
that magically appears should just be u
. To continue that proof, you could start reducing the RHS and verify that it also produces \x -> u x y
.
组成大致相同:在两侧插入pure
和(<*>)
的定义,然后在两侧开始计算.您很快就会来一些容易证明是等效的裸lambda.
Composition is more of the same: plug in the definitions of pure
and (<*>)
on both sides, then start calculating on both sides. You'll soon come to some bare lambdas that will be easy to prove equivalent.
这篇关于((->)r)类型的适用法律的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!