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))
세 번째 규칙은 seq의 정의로부터 직접 따라옵니다:
네 번째 경우에는 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
하지만 이는 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로 다시 쓸 수 있습니다. 이는 애플리커티브 펑터가 함수 합성을 보존한다는 규칙의 한 사례입니다.
이는 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)와 동치입니다. 중간에 있는 단위 함수는 즉시 제거할 수 있으며, 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 is a left identity of >>=
v >>= fun y => pure (id y)
Reduce the call to id
v >>= fun y => pure y
fun x => f x is the same as f
v >>= pure
pure is a right identity of >>=
v
함수 합성을 보존하는지 확인하려면 pure (· ∘ ·) <*> u <*> v <*> w = u <*> (v <*> w)인지 확인하십시오. 첫 번째 단계는 <*>를 seq의 이 정의로 대체하는 것입니다. 그 다음, Monad 계약의 항등 법칙과 결합 법칙을 사용하는 (다소 긴) 일련의 단계를 거치면 한쪽에서 다른 쪽으로 도달하기에 충분합니다:
seq (seq (seq (pure (· ∘ ·)) (fun _ => u))
(fun _ => v))
(fun _ => w)
Definition of 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 is a left identity of >>=
((u >>= fun x =>
pure (x ∘ ·)) >>= fun g =>
v >>= fun y =>
pure (g y)) >>= fun h =>
w >>= fun z =>
pure (h z)Insertion of parentheses for clarity
((u >>= fun x =>
pure (x ∘ ·)) >>= (fun g =>
v >>= fun y =>
pure (g y))) >>= fun h =>
w >>= fun z =>
pure (h z)
Associativity of >>=
(u >>= fun x =>
pure (x ∘ ·) >>= fun g =>
v >>= fun y => pure (g y)) >>= fun h =>
w >>= fun z =>
pure (h z)
pure is a left identity of >>=
(u >>= fun x =>
v >>= fun y =>
pure (x ∘ y)) >>= fun h =>
w >>= fun z =>
pure (h z)
Associativity of >>=
u >>= fun x =>
v >>= fun y =>
pure (x ∘ y) >>= fun h =>
w >>= fun z =>
pure (h z)
pure is a left identity of >>=
u >>= fun x =>
v >>= fun y =>
w >>= fun z =>
pure ((x ∘ y) z)Definition of function composition
u >>= fun x =>
v >>= fun y =>
w >>= fun z =>
pure (x (y z))
Time to start moving backwards!
pure is a left identity of >>=
u >>= fun x =>
v >>= fun y =>
w >>= fun z =>
pure (y z) >>= fun q =>
pure (x q)
Associativity of >>=
u >>= fun x =>
v >>= fun y =>
(w >>= fun p =>
pure (y p)) >>= fun q =>
pure (x q)
Associativity of >>=
u >>= fun x =>
(v >>= fun y =>
w >>= fun q =>
pure (y q)) >>= fun z =>
pure (x z)
This includes the definition of seq
u >>= fun x =>
seq v (fun () => w) >>= fun q =>
pure (x q)
This also includes the definition of seq
seq u (fun () => seq v (fun () => w))순수 연산의 시퀀싱이 아무 동작도 하지 않음을 확인하려면 다음과 같이 합니다:
seq (pure f) (fun () => pure x)
Replacing seq with its definition
pure f >>= fun g =>
pure x >>= fun y =>
pure (g y)
pure is a left identity of >>=
pure f >>= fun g =>
pure (g x)
pure is a left identity of >>=
pure (f x)마지막으로, 순수 연산의 순서가 중요하지 않은지 확인하려면 다음과 같습니다:
seq u (fun () => pure x)
Definition of seq
u >>= fun f =>
pure x >>= fun y =>
pure (f y)
pure is a left identity of >>=
u >>= fun f =>
pure (f x)Clever replacement of one expression by an equivalent one that makes the rule match
u >>= fun f =>
pure ((fun g => g x) f)
pure is a left identity of >>=
pure (fun g => g x) >>= fun h =>
u >>= fun f =>
pure (h f)
Definition of 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으로 다시 작성됨)을 사용하면 첫 번째 오류만 확인할 수 있습니다: