5.3. The Applicative Contract🔗

Functor, Monad, 그리고 BEq와 Hashable을 구현하는 타입과 마찬가지로 Applicative에도 모든 인스턴스가 따라야 할 규칙 집합이 있다.

Applicative functor가 따라야 할 규칙은 네 가지다.

항등성을 존중해야 하므로 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. All Applicatives are Functors🔗

Applicative의 두 연산자만으로 map을 정의할 수 있다.

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

하지만 이는 Applicative 계약이 Functor 계약을 보장할 때에만 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로 다시 쓸 수 있다. 이는 애플리커티브 펑터가 함수 합성을 존중한다는 규칙의 한 사례다.

따라서 Applicative가 Functor를 확장하도록 정의할 수 있으며, 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. All Monads are Applicative Functors🔗

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)와 같다. 가운데의 단위 함수는 즉시 제거할 수 있으므로 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)

따라서 Monad가 Applicative를 확장하도록 정의할 수 있으며, seq의 기본 정의는 다음과 같다.

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. Additional Stipulations🔗

각 타입 클래스에 대응하는 개별 계약을 따르는 것에 더해, Functor, Applicative, Monad의 결합된 구현은 이 기본 구현과 동등하게 작동해야 한다. 다시 말해 Applicative와 Monad 인스턴스를 모두 제공하는 타입은 Monad 인스턴스가 기본 구현으로 생성하는 버전과 다르게 작동하는 seq 구현을 가져서는 안 된다. 이는 다형 함수에서 >>= 사용을 동등한 <*> 사용으로, 또는 <*> 사용을 동등한 >>= 사용으로 리팩터링할 수 있기 때문에 중요하다. 이 리팩터링은 이 코드를 사용하는 프로그램의 의미를 바꾸지 않아야 한다.

이 규칙 때문에 Validate.andThen을 Monad 인스턴스의 bind 구현에 사용해서는 안 된다. 그 자체로는 Monad 계약을 따른다. 하지만 이를 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 := [] }