证明构成适用于（（ - >）r）类型的法则 [英] Proving Composition Applicative law for ((->) r) type

问题描述

构成适用法律如下：

 纯（。）* u * v * w = u * （v * w）
  

下面是我试图证明（（ - >）r）类型：

RHS：

  u <*> （v * w）
 u * （\\ yy  - > v y（w y））
 \ x  - > u（（\ y  - > v y（w y））x）
 \ x  - > ux（vx（wx）） - （A）
  

LHS：

 纯（。）* * u * v * w 
 const（。）* * u * v * （ff（uf））* f（ff） v * （·）（u f））* *（b） v * （·）（u f））g（v g））* w 
 \x  - > （\ g  - >（\ f  - >（。）（uf））g（vg））x（wx）
  - 通过应用x 
 \ x扩展labmda  - > （（））（）（）（）（）（）（） （（（。）（u x））（v x））（w x）
 
 \ x  - > （（ux）。（vx））（wx） - （B）
  

认为（A）& （B）是相同的，那么我在哪里犯了一个错误？我将不胜感激任何帮助或建议。

解决方案

你快到了。您只需要使用（。）的定义，即 $ b

 （f。g）x = f（gx）
  

在最后一行你的LHS计算，你应该有两个明显相等的lambda表达式。

The Composition Applicative Law is as follows:

pure (.) <*> u <*> v <*> w = u <*> (v <*> w)

Here's my attempt at proving the Composition law for the ((->) r) type:

RHS:

u <*> (v <*> w)
u <*> ( \y -> v y (w y) )
\x -> u x ( (\y -> v y (w y)) x )
\x -> u x ( v x (w x)) -- (A)

LHS:

pure (.) <*> u <*> v <*> w
const (.) <*> u <*> v <*> w
(\f -> const (.) f (u f)) <*> v <*> w
(\f -> (.) (u f)) <*> v <*> w
(\g -> (\f -> (.) (u f)) g (v g)) <*> w
\x -> (\g -> (\f -> (.) (u f)) g (v g)) x (w x)
-- Expanding labmda by applying to x
\x -> ((\f -> (.) (u f)) x (v x)) (w x)
\x -> (( (.) (u x)) (v x)) (w x)

\x -> ((u x) . (v x)) (w x) -- (B)

I don't think (A) & (B) are equivalent, so where did I make a mistake? I would appreciate any help or suggestions.

解决方案

You're almost there. You just need to use the definition of (.), which is

(f . g) x = f (g x)

After substituting that definition in the last line of your LHS calculation, you should have two obviously equal lambdas.

这篇关于证明构成适用于（（ - >）r）类型的法则的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！