適用：純粋なf <*> x =純粋な（フリップ（$））<*> x <*>純粋なf

Question

Typoclassopedia私の研究中に私はこの証拠に遭遇しましたが、私の証拠が正しいかどうかわかりません。問題は次のとおりです。

有効な引数に純粋な関数を適用するための何かを述べている交換法則の変種を想像するかもしれません。上記の法律を使用して、そのことを証明：

pure f <*> x = pure (flip ($)) <*> x <*> pure f

どこに "上記の法律" のポイントをに、簡単に次のように

pure id <*> v = v -- identity law 
pure f <*> pure x = pure (f x) -- homomorphism 
u <*> pure y = pure ($ y) <*> u -- interchange 
u <*> (v <*> w) = pure (.) <*> u <*> v <*> w -- composition 

私の証明は次のとおりです。

pure f <*> x = pure (($) f) <*> x -- identical 
pure f <*> x = pure ($) <*> pure f <*> x -- homomorphism 
pure f <*> x = pure (flip ($)) <*> x <*> pure f -- flip arguments 

Answer 1

私は後方にそれを証明することになった：最後の変換の

pure (flip ($)) <*> x <*> pure f 
    = (pure (flip ($)) <*> x) <*> pure f -- <*> is left-associative 
    = pure ($ f) <*> (pure (flip ($)) <*> x) -- interchange 
    = pure (.) <*> pure ($ f) <*> pure (flip ($)) <*> x -- composition 
    = pure (($ f) . (flip ($))) <*> x -- homomorphism 
    = pure (flip ($) f . flip ($)) <*> x -- identical 
    = pure f <*> x 

は説明：

flip ($)はタイプa -> (a -> c) -> cであり、直感的には、タイプaの引数をとり、その引数を受け取り、最後に最初の引数を持つ関数を呼び出します。したがって、flip ($) 5は引数として5で呼び出される関数を引数としてとります。 (+ 2)をflip ($) 5に渡すと、(+2) $ 5と等価で、7と評価されるflip ($) 5 (+2)が得られます。

flip ($) fは、\x -> x $ fに相当します。つまり、入力として関数を呼び出し、関数fを引数として呼び出します。

これらの関数の合成このように動作します：まずflip ($)が、それは最初の引数だとしてxを取り、機能flip ($) xを返し、それはそれは引数だとしてxと呼ばれる最後の引数、だとして、この関数は、関数を待っています。今度はこの関数flip ($) xがflip ($) fに渡されるか、それと等価である(\x -> x $ f) (flip ($) x)と書くと、(flip ($) x) fという表現になります。これはf $ xに相当します。

あなたはflip ($) f . flip ($)の種類を確認することができますが（あなたの関数fに応じて）このようなものです：

λ: let f = sqrt 
λ: :t (flip ($) f) . (flip ($)) 
(flip ($) f) . (flip ($)) :: Floating c => c -> c 

Answer 2

あなたの証明の最初の2つのステップは上手く見えますが、最後のステップはありません。 flipの定義はあなたのような法律を使用することができますが：

f a b = flip f b a 

意味するものではありません。

pure f <*> a <*> b = pure (flip f) <*> b <*> a 

実際には、これは一般的に偽です。この2行の出力を比較します。あなたがヒントをしたい場合

pure (+) <*> [1,2,3] <*> [4,5] 
pure (flip (+)) <*> [4,5] <*> [1,2,3] 

、あなたはこのバリアントを証明するためにいくつかの点で、元の交換法則を使用する必要があるとしています。

実際には、これを証明するために準同型、交換、および合成の法則を使用しなければならないことがわかりました。証明の一部は、特に($ f)など(($) f)とは違って、 GHCiを開いて、私の証明タイプの各ステップをチェックし、正しい結果を出したことを再確認することが役に立ちました。 （細かい型チェック上のあなたの証明、それは最後のステップは正当ではなかったということだけだ。）

> let f = sqrt 
> let x = [1,4,9] 
> pure f <*> x 
[1.0,2.0,3.0] 
> pure (flip ($)) <*> x <*> pure f 
[1.0,2.0,3.0] 
> 

Answer 3

で書かれたとき、私は、このような定理は、原則として、はるかに少ない関与していることを注意したいですその後、法律がある

class Functor f => Monoidal f where 
    pure :: a -> f a 
    (⑂) :: f a -> f b -> f (a,b) 

同等クラスでmonoidalファンクタではなく、応用的バージョン、すなわちの数学的なスタイル

id <$> v = v 
f <$> (g <$> v) = f . g <$> v 
f <$> pure x = pure (f x) 
x ⑂ pure y = fmap (,y) x 
a⑂(b⑂c) = assoc <$> (a⑂b)⑂c 

assoc ((x,y),z) = (x,(y,z))。

が

定理は、その後

pure u ⑂ x = swap <$> x ⑂ pure u 

証明読み：

swap <$> x ⑂ pure u 
    = swap <$> fmap (,u) x 
    = swap . (,u) <$> x 
    = (u,) <$> x 
    = pure u ⑂ x 

□