5.3. 애플리커티브 계약🔗

Functor, Monad, 그리고 BEq와 Hashable을 구현하는 타입과 마찬가지로, Applicative에도 모든 인스턴스가 지켜야 하는 일련의 규칙이 있습니다.

애플리커티브 펑터가 따라야 하는 규칙은 네 가지입니다.

항등성을 지켜야 하므로, pure id <*> v = v입니다.
함수 합성을 존중해야 하므로, pure (· ∘ ·) <*> u <*> v <*> w = u <*> (v <*> w)가 성립해야 합니다
순수 연산을 순서대로 실행하는 것은 아무 효과도 없어야 하므로 pure f <*> pure x=pure (f x)입니다.
순수 연산의 순서는 중요하지 않으므로 u <*> pure x = pure (fun f => f x) <*> u입니다

Applicative Option 인스턴스가 이 법칙들을 만족하는지 확인하려면, 먼저 pure를 some으로 전개하는 것으로 시작하십시오.

첫 번째 규칙은 some id <*> v = v입니다. Option에 대한 seq의 정의에 따르면 이는 id <$> v = v와 같으며, 이것은 이미 확인한 Functor 규칙 중 하나입니다.

두 번째 규칙은 some (· ∘ ·) <*> u <*> v <*> w = u <*> (v <*> w)라는 것입니다. u, v, w 중 어느 하나라도 none이면 양변이 모두 none이므로 이 성질이 성립합니다. u가 some f이고, v가 some g이며, w가 some x라고 가정하면, 이는 some (· ∘ ·) <*> some f <*> some g <*> some x = some f <*> (some g <*> some x)라고 말하는 것과 같습니다. 양변을 평가하면 같은 결과가 나옵니다:

              some (· ∘ ·) <*> some f <*> some g <*> some xsome (f ∘ ·) <*> some g <*> some xsome (f ∘ g) <*> some xsome ((f ∘ g) x)some (f (g x))

              some f <*> (some g <*> some x)some f <*> (some (g x))some (f (g x))

세 번째 규칙은 seq의 정의에서 바로 도출됩니다:

              some f <*> some xf <$> some xsome (f x)

네 번째 경우에서는 u가 some f라고 가정합니다. none이라면 등식의 양변이 모두 none이기 때문입니다. some f <*> some x는 곧바로 some (f x)로 평가되며, some (fun g => g x) <*> some f도 마찬가지입니다.

5.3.1. 모든 애플리커티브는 펑터입니다🔗

Applicative의 두 연산자만으로도 map을 정의할 수 있습니다:

def map [Applicative f] (g : α → β) (x : f α) : f β :=
  pure g <*> x

하지만 이것을 Functor 구현에 사용할 수 있는 것은 Applicative의 계약이 Functor의 계약을 보장하는 경우뿐입니다. Functor의 첫 번째 규칙은 id <$> x = x이며, 이는 Applicative의 첫 번째 규칙에서 바로 도출됩니다. Functor의 두 번째 규칙은 map (f ∘ g) x = map f (map g x)입니다. 여기서 map의 정의를 펼치면 pure (f ∘ g) <*> x = pure f <*> (pure g <*> x)가 됩니다. 순수 연산을 순차 실행해도 아무 효과가 없다는 규칙을 사용하면, 좌변을 pure (· ∘ ·) <*> pure f <*> pure g <*> x로 다시 쓸 수 있습니다. 이는 애플리커티브 펑터가 함수 합성을 보존한다는 규칙의 한 사례입니다.

이로써 Functor를 확장하는 Applicative 정의가 정당화되며, 이 정의에서 map의 기본 정의는 pure와 seq를 이용하여 주어집니다:

class Applicative (f : Type → Type) extends Functor f where
  pure : α → f α
  seq : f (α → β) → (Unit → f α) → f β
  map g x := seq (pure g) (fun () => x)

5.3.2. 모든 모나드는 애플리커티브 펑터입니다🔗

Monad 인스턴스는 이미 pure의 구현을 요구합니다. 여기에 bind를 더하면 seq를 정의하기에 충분합니다:

def seq [Monad m] (f : m (α → β)) (x : Unit → m α) : m β := do
  let g ← f
  let y ← x ()
  pure (g y)

다시 한번, Monad 계약이 Applicative 계약을 함의한다는 것을 확인하면, Monad가 Applicative를 확장하는 경우 이를 seq의 기본 정의로 사용할 수 있습니다.

이 절의 나머지 부분에서는 bind를 바탕으로 한 seq의 이 구현이 실제로 Applicative 계약을 만족한다는 논증을 인자 단위로 하나씩 따져 봅니다. 함수형 프로그래밍의 아름다운 점 중 하나는 이런 종류의 논증을 표현식 평가를 다룬 첫 절에 나온 평가 규칙들을 사용하여 종이와 연필만으로 풀어낼 수 있다는 것입니다. 이때 각 함수에 주어지는 인자가 어떻게 치환되는지를 차례로 따라가면 됩니다. 이러한 논증을 읽으면서 연산과 그 인자들의 의미를 생각해 보면 이해에 도움이 될 때가 있습니다.

do-표기법을 >>=를 명시적으로 사용하는 형태로 바꾸면 Monad 규칙을 적용하기가 더 쉬워집니다:

def seq [Monad m] (f : m (α → β)) (x : Unit → m α) : m β :=
  f >>= fun g =>
  x () >>= fun y =>
  pure (g y)

이 정의가 항등성을 지키는지 확인하려면 seq (pure id) (fun () => v) = v인지 확인하십시오. 좌변은 pure id >>= fun g => (fun () => v) () >>= fun y => pure (g y)와 동등합니다. 가운데에 있는 unit 함수는 바로 제거할 수 있으며, 그 결과 pure id >>= fun g => v >>= fun y => pure (g y)를 얻습니다. pure가 >>=의 왼쪽 항등원이라는 사실을 이용하면, 이는 v >>= fun y => pure (id y)와 같고, 이는 곧 v >>= fun y => pure y입니다. fun x => f x는 f와 같으므로 이는 v >>= pure와 같으며, pure가 >>=의 오른쪽 항등원이라는 사실을 이용하면 v를 얻을 수 있습니다.

이런 비형식적 추론은 형식을 조금 바꾸면 더 읽기 쉽게 만들 수 있습니다. 다음 표에서 “EXPR1 ={ REASON }= EXPR2”는 “REASON이므로 EXPR1은 EXPR2와 같습니다”로 읽으십시오:

pure id >>= fun g => v >>= fun y => pure (g y)

pure는 >>=의 왼쪽 항등원입니다

v >>= fun y => pure (id y)

id 호출 축약

v >>= fun y => pure y

fun x => f x는 f와 같습니다

v >>= pure

pure는 >>=의 오른쪽 항등원입니다

v

함수 합성을 보존하는지 확인하려면 pure (· ∘ ·) <*> u <*> v <*> w = u <*> (v <*> w)인지 확인하십시오. 첫 번째 단계는 <*>를 seq의 이 정의로 바꾸는 것입니다. 그다음에는 Monad 계약의 항등 법칙과 결합 법칙을 사용하는 (다소 긴) 일련의 단계만 거치면 한쪽에서 다른 쪽으로 도달할 수 있습니다:

seq (seq (seq (pure (· ∘ ·)) (fun _ => u))
      (fun _ => v))
  (fun _ => w)

seq의 정의

((pure (· ∘ ·) >>= fun f =>
   u >>= fun x =>
   pure (f x)) >>= fun g =>
  v >>= fun y =>
  pure (g y)) >>= fun h =>
 w >>= fun z =>
 pure (h z)

pure는 >>=의 왼쪽 항등원입니다

((u >>= fun x =>
   pure (x ∘ ·)) >>= fun g =>
   v >>= fun y =>
  pure (g y)) >>= fun h =>
 w >>= fun z =>
 pure (h z)

명확성을 위한 괄호 삽입

((u >>= fun x =>
   pure (x ∘ ·)) >>= (fun g =>
   v >>= fun y =>
  pure (g y))) >>= fun h =>
 w >>= fun z =>
 pure (h z)

>>=의 결합 법칙

(u >>= fun x =>
  pure (x ∘ ·) >>= fun g =>
 v  >>= fun y => pure (g y)) >>= fun h =>
 w >>= fun z =>
 pure (h z)

pure는 >>=의 왼쪽 항등원입니다

(u >>= fun x =>
  v >>= fun y =>
  pure (x ∘ y)) >>= fun h =>
 w >>= fun z =>
 pure (h z)

>>=의 결합 법칙

u >>= fun x =>
v >>= fun y =>
pure (x ∘ y) >>= fun h =>
w >>= fun z =>
pure (h z)

pure는 >>=의 왼쪽 항등원입니다

u >>= fun x =>
v >>= fun y =>
w >>= fun z =>
pure ((x ∘ y) z)

함수 합성의 정의

u >>= fun x =>
v >>= fun y =>
w >>= fun z =>
pure (x (y z))

이제 거꾸로 되짚어 갈 차례입니다! pure는 >>=의 왼쪽 항등원입니다

u >>= fun x =>
v >>= fun y =>
w >>= fun z =>
pure (y z) >>= fun q =>
pure (x q)

>>=의 결합 법칙

u >>= fun x =>
v >>= fun y =>
 (w >>= fun p =>
  pure (y p)) >>= fun q =>
 pure (x q)

>>=의 결합 법칙

u >>= fun x =>
 (v >>= fun y =>
  w >>= fun q =>
  pure (y q)) >>= fun z =>
 pure (x z)

여기에는 seq의 정의가 포함됩니다

u >>= fun x =>
seq v (fun () => w) >>= fun q =>
pure (x q)

여기에는 seq의 정의도 포함됩니다

seq u (fun () => seq v (fun () => w))

순수 연산을 차례로 실행해도 아무 효과가 없음을 확인하려면 다음과 같이 합니다:

seq (pure f) (fun () => pure x)

seq를 그 정의로 바꾸기

pure f >>= fun g =>
pure x >>= fun y =>
pure (g y)

pure는 >>=의 왼쪽 항등원입니다

pure f >>= fun g =>
pure (g x)

pure는 >>=의 왼쪽 항등원입니다

pure (f x)

마지막으로, 순수 연산의 순서가 중요하지 않음을 확인하려면 다음과 같이 합니다.

seq u (fun () => pure x)

seq의 정의

u >>= fun f =>
pure x >>= fun y =>
pure (f y)

pure는 >>=의 왼쪽 항등원입니다

u >>= fun f =>
pure (f x)

규칙이 들어맞도록 한 표현식을 그와 동등한 다른 표현식으로 영리하게 바꿔 쓰기

u >>= fun f =>
pure ((fun g => g x) f)

pure는 >>=의 왼쪽 항등원입니다

pure (fun g => g x) >>= fun h =>
u >>= fun f =>
pure (h f)

seq의 정의

seq (pure (fun f => f x)) (fun () => u)

이는 Applicative를 확장하고 seq의 기본 정의를 갖춘 Monad 정의가 타당함을 보여 줍니다:

class Monad (m : Type → Type) extends Applicative m where
  bind : m α → (α → m β) → m β
  seq f x :=
    bind f fun g =>
    bind (x ()) fun y =>
    pure (g y)

Applicative 자체에 있는 map의 기본 정의 덕분에, 모든 Monad 인스턴스는 Applicative 인스턴스와 Functor 인스턴스도 자동으로 생성합니다.

5.3.3. 추가 규정🔗

각 타입 클래스에 연관된 개별 계약을 준수하는 것에 더해, Functor, Applicative, Monad를 함께 구현할 때는 이러한 기본 구현과 동등하게 동작해야 합니다. 다시 말해, Applicative 인스턴스와 Monad 인스턴스를 모두 제공하는 타입은 Monad 인스턴스가 기본 구현으로 생성하는 버전과 다르게 동작하는 seq 구현을 가져서는 안 됩니다. 이것이 중요한 이유는 다형 함수를 리팩터링하면서 >>=를 사용하는 부분을 동등한 <*> 사용으로 바꾸거나, <*>를 사용하는 부분을 동등한 >>= 사용으로 바꿀 수 있기 때문입니다. 이러한 리팩터링이 이 코드를 사용하는 프로그램의 의미를 바꾸어서는 안 됩니다.

이 규칙은 Monad 인스턴스에서 bind를 구현하는 데 Validate.andThen을 사용해서는 안 되는 이유를 설명합니다. 그 자체로는 모나드 계약을 따릅니다. 그러나 이 함수로 seq를 구현하면, 그 동작은 seq 자체와 동등하지 않습니다. 어디서 차이가 나는지 알아보기 위해, 둘 다 오류를 반환하는 두 계산을 예로 들어 봅시다. 두 개의 오류가 반환되어야 하는 경우의 예부터 시작합시다. 하나는 함수를 검증할 때 발생한 오류(이 오류는 그 함수에 앞서 전달된 인자에서 발생했을 수도 있습니다)이고, 다른 하나는 인자를 검증할 때 발생한 오류입니다:

def notFun : Validate String (Nat → String) :=
  .errors { head := "First error", tail := [] }

def notArg : Validate String Nat :=
  .errors { head := "Second error", tail := [] }

이들을 Validate의 Applicative 인스턴스에 정의된 <*>로 결합하면 두 오류가 모두 사용자에게 보고됩니다:

                notFun <*> notArgmatch notFun with
| .ok g => g <$> notArg
| .errors errs =>
  match notArg with
  | .ok _ => .errors errs
  | .errors errs' => .errors (errs ++ errs')match notArg with
| .ok _ =>
  .errors { head := "First error", tail := [] }
| .errors errs' =>
  .errors ({ head := "First error", tail := [] } ++ errs').errors
  ({ head := "First error", tail := [] } ++
   { head := "Second error", tail := []}).errors {
  head := "First error",
  tail := ["Second error"]
}

>>=로 구현한 seq 버전(여기서는 andThen으로 다시 작성했습니다)을 사용하면 첫 번째 오류만 얻을 수 있습니다:

                seq notFun (fun () => notArg)notFun.andThen fun g =>
notArg.andThen fun y =>
pure (g y)match notFun with
| .errors errs => .errors errs
| .ok val =>
  (fun g =>
    notArg.andThen fun y =>
    pure (g y)) val.errors { head := "First error", tail := [] }