對應用型法律（（ - >）R）型

Question

我試圖檢查應用型法律保持功能型((->) r)，這裏是我到目前爲止有：

-- 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) 

我有沒有執行前兩個法律的步驟是否正確？

我正在努力與交換&組成法律。對於交流，到目前爲止，我有以下幾點：

-- 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. 

我希望得到任何幫助的步驟來驗證爲((->) r)式立交&組成應用性的法律。作爲參考，該組合物合用的法律如下：

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

Answer 1

我想在你的「身份證明」，就應該更換g與v無處不在（否則什麼是g和它是在哪裏來的呢？）。同樣，在你的「交匯」證明中，目前看起來還不錯，但神奇出現的g應該只是u。要繼續證明，您可以開始減少RHS並驗證它也生成\x -> u x y。

組成更多相同：在兩側插入pure和(<*>)的定義，然後開始在兩側進行計算。你很快會找到一些很容易證明是等價的光屁股。