실용적 : <a href="https://wiki.haskell.org/Typeclassopedia" rel="nofollow noreferrer">Typoclassopedia</a> 내 연구 기간 동안 <*> X = 순수 (플립 ($)) <*> X <*> 순수 f`

Question

F '순수 증명 나는이 증거를 발견,하지만 난 내 증거가 맞는지 확실하지 않다. 문제는 다음과 같습니다.

유효한 인수에 순수한 함수를 적용하는 것에 관한 상호 법칙의 변형을 상상할 수 있습니다. 위의 법을 사용하여, 그 증명 :

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

경우 "위 법률"포인트를 Applicative Laws에, 간단히 다음과 같이

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에 전달하면 flip ($) 5 (+2)이되며 이는 (+2) $ 5이라는 표현과 같으며 7으로 평가됩니다.

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과 같습니다.

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

Answer 2

증명의 처음 두 단계는 괜찮아 보이지만 마지막 단계는 그렇지 않습니다. flip의 정의는이 같은 법을 사용할 수 있지만 :

f a b = flip f b a 

의미하지 않는다 :

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

사실, 이것은 일반적으로 false입니다.

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

내가 작성 때와 같은 정리가 훨씬 덜 관여 원칙적으로,있는 발언 것 :

당신은 flip ($) f . flip ($)의 유형이 같은 것입니다 확인하실 수 있습니다

(함수 f에 따라 다름) 그런 법이 있습니다

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 

□