5.6. 전체 정의
관련된 언어 기능을 모두 소개했으므로, 이 절에서는 Lean 표준 라이브러리에 정의된 그대로의 Functor, Applicative, Monad의 완전하고 정직한 정의를 설명합니다. 이해를 돕기 위해 세부 사항을 하나도 생략하지 않습니다.
5.6.1. 펑터
Functor 클래스의 완전한 정의에서는 유니버스 다형성과 기본 메서드 구현을 사용합니다:
class Functor (f : Type u → Type v) : Type (max (u+1) v) where
map : {α β : Type u} → (α → β) → f α → f β
mapConst : {α β : Type u} → α → f β → f α :=
Function.comp map (Function.const _)
이 정의에서 Function.comp는 함수 합성이며, 보통 ∘ 연산자로 표기합니다. Function.const는 상수 함수로, 두 번째 인자를 무시하는 두 인자 함수입니다. 이 함수를 인자 하나에만 적용하면 항상 같은 값을 반환하는 함수가 만들어집니다. 이는 API가 함수를 요구하지만 프로그램이 인자에 따라 다른 결과를 계산할 필요가 없을 때 유용합니다. Function.const의 간단한 버전은 다음과 같이 작성할 수 있습니다:
def simpleConst (x : α) (_ : β) : α := x
인자 하나만 넣은 이 함수를 List.map의 함수 인자로 사용해 보면 그 유용성이 드러납니다:
#eval [1, 2, 3].map (simpleConst "same")실제 함수의 시그니처는 다음과 같습니다:
여기서 타입 인자 β는 명시적 인자이므로, mapConst의 기본 정의는 _ 인자를 제공합니다. 이 인자는 프로그램이 타입 검사를 통과하도록 하는 유일한 타입을 찾아 Function.const에 전달하라고 Lean에 지시합니다. Function.comp map (Function.const _)는 fun (x : α) (y : f β) => map (fun _ => x) y와 동등합니다.
Functor 타입 클래스는 u+1과 v 중 더 큰 쪽의 유니버스에 속합니다. 여기서 u는 f가 인자로 받는 유니버스의 레벨이고, v는 f가 반환하는 유니버스입니다. Functor 타입 클래스를 구현하는 구조체가 왜 u보다 큰 유니버스에 있어야 하는지 알아보기 위해, 먼저 이 클래스를 단순화한 정의부터 살펴봅시다:
class Functor (f : Type u → Type v) : Type (max (u+1) v) where
map : {α β : Type u} → (α → β) → f α → f β이 타입 클래스의 구조체 타입은 다음 귀납적 타입과 동등합니다:
inductive Functor (f : Type u → Type v) : Type (max (u+1) v) where
| mk : ({α β : Type u} → (α → β) → f α → f β) → Functor f
mk에 인자로 전달되는 map 메서드의 구현에는 Type u에 속한 두 타입을 인자로 받는 함수가 포함되어 있습니다. 이는 함수 자체의 타입이 Type (u+1)에 속한다는 뜻이므로, Functor 역시 적어도 u+1 이상의 레벨에 있어야 합니다. 마찬가지로, 함수의 다른 인자들은 f를 적용하여 만든 타입을 가지므로, 이 역시 적어도 v 이상의 레벨을 가져야 합니다. 이 절의 모든 타입 클래스는 이 성질을 공유합니다.
5.6.2. 애플리커티브
Applicative 타입 클래스는 사실 관련 메서드를 일부씩 담고 있는 여러 개의 더 작은 클래스로 이루어져 있습니다. 첫 번째는 Pure와 Seq로, 각각 pure와 seq를 담고 있습니다:
class Pure (f : Type u → Type v) : Type (max (u+1) v) where
pure {α : Type u} : α → f αclass Seq (f : Type u → Type v) : Type (max (u+1) v) where
seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β
이 외에도 Applicative는 SeqRight 클래스와, 이와 비슷한 SeqLeft 클래스에도 의존합니다:
class SeqRight (f : Type u → Type v) : Type (max (u+1) v) where
seqRight : {α β : Type u} → f α → (Unit → f β) → f βclass SeqLeft (f : Type u → Type v) : Type (max (u+1) v) where
seqLeft : {α β : Type u} → f α → (Unit → f β) → f α
대안과 검증에 관한 절에서 소개한 seqRight 함수는 효과의 관점에서 보면 가장 쉽게 이해할 수 있습니다. E1 *> E2는 SeqRight.seqRight E1 (fun () => E2)로 풀어 쓰이며, 먼저 E1을 실행한 다음 E2를 실행하고 E2의 결과만을 내놓는 것으로 이해할 수 있습니다. E1의 효과로 인해 E2가 실행되지 않을 수도 있고, 여러 번 실행될 수도 있습니다. 실제로 f에 Monad 인스턴스가 있다면 E1 *> E2는 do let _ ← E1; E2와 동등하지만, seqRight는 Validate처럼 모나드가 아닌 타입에도 사용할 수 있습니다.
이와 사촌 격인 seqLeft도 매우 비슷하지만, 가장 왼쪽 표현식의 값을 반환한다는 점이 다릅니다. E1 <* E2는 SeqLeft.seqLeft E1 (fun () => E2)로 디슈가링됩니다. SeqLeft.seqLeft의 타입은 f α → (Unit → f β) → f α이며, 이는 f α를 반환한다는 점을 제외하면 seqRight의 타입과 동일합니다. E1 <* E2는 먼저 E1을 실행한 다음 E2를 실행하고, E1의 원래 결과를 반환하는 프로그램으로 이해할 수 있습니다. f에 Monad 인스턴스가 있다면, E1 <* E2는 do let x ← E1; _ ← E2; pure x와 동등합니다. 일반적으로 seqLeft는 검증이나 파서와 유사한 작업 흐름에서 값 자체를 바꾸지 않고 그 값에 추가 조건을 지정할 때 유용합니다.
Applicative의 정의는 Functor와 더불어 이 모든 클래스를 확장합니다:
class Applicative (f : Type u → Type v)
extends Functor f, Pure f, Seq f, SeqLeft f, SeqRight f where
map := fun x y => Seq.seq (pure x) fun _ => y
seqLeft := fun a b => Seq.seq (Functor.map (Function.const _) a) b
seqRight := fun a b => Seq.seq (Functor.map (Function.const _ id) a) b
Applicative를 완전히 정의하려면 pure와 seq의 정의만 있으면 됩니다. Functor, SeqLeft, SeqRight의 모든 메서드에 기본 정의가 있기 때문입니다. Functor의 mapConst 메서드에는 Functor.map을 사용하는 자체 기본 구현이 있습니다. 이러한 기본 구현은 동작이 동등하면서 더 효율적인 새 함수로만 재정의해야 합니다. 기본 구현은 자동으로 생성되는 코드일 뿐만 아니라 정확성에 대한 명세로도 보아야 합니다.
seqLeft의 기본 구현은 매우 간결합니다. 일부 이름을 해당 문법 설탕이나 정의로 바꾸면 이를 다른 관점에서 볼 수 있으므로 다음과 같이 바꿔 봅시다.
Seq.seq (Functor.map (Function.const _) a) b다음과 같이 됩니다.
fun a b => Seq.seq ((fun x _ => x) <$> a) b
(fun x _ => x) <$> a는 어떻게 이해해야 합니까? 여기서 a의 타입은 f α이고, f는 펑터입니다. f가 List이면 (fun x _ => x) <$> [1, 2, 3]은 [fun _ => 1, fun _ => 2, fun _ => 3으로 평가됩니다. f가 Option이면 (fun x _ => x) <$> some "hello"는 some (fun _ => "hello")로 평가됩니다. 각 경우에서 펑터 안의 값은 인자를 무시하고 원래 값을 반환하는 함수로 대체됩니다. 이 함수를 seq와 결합하면 seq의 두 번째 인자에서 나온 값은 버려집니다.
seqRight의 기본 구현도 이와 매우 비슷하지만, Function.const에 id라는 인자가 하나 더 있다는 점이 다릅니다. 이 정의도 비슷한 방식으로 이해할 수 있습니다. 먼저 몇 가지 표준적인 문법 설탕을 도입한 다음, 일부 이름을 그 정의로 바꾸면 됩니다:
fun a b => Seq.seq (Functor.map (Function.const _ id) a) bfun a b => Seq.seq ((fun _ => id) <$> a) bfun a b => Seq.seq ((fun _ => fun x => x) <$> a) bfun a b => Seq.seq ((fun _ x => x) <$> a) b
(fun _ x => x) <$> a는 어떻게 이해해야 합니까? 이번에도 예시를 보면 도움이 됩니다. fun _ x => x) <$> [1, 2, 3]은 [fun x => x, fun x => x, fun x => x]와 동등하고, (fun _ x => x) <$> some "hello"는 some (fun x => x)와 동등합니다. 다시 말해 (fun _ x => x) <$> a는 a의 전체적인 모양은 그대로 유지하지만, 각 값은 항등 함수로 대체됩니다. 효과의 관점에서 보면 a의 부수 효과는 일어나지만, seq와 함께 사용될 때 그 값들은 버려집니다.
5.6.3. 모나드
Applicative를 구성하는 연산들이 각자의 타입 클래스로 나뉘어 있는 것처럼, Bind에도 별도의 클래스가 있습니다:
class Bind (m : Type u → Type v) where
bind : {α β : Type u} → m α → (α → m β) → m β
Monad는 Bind를 더하여 Applicative를 확장합니다.
class Monad (m : Type u → Type v) : Type (max (u+1) v)
extends Applicative m, Bind m where
map f x := bind x (Function.comp pure f)
seq f x := bind f fun y => Functor.map y (x ())
seqLeft x y := bind x fun a => bind (y ()) (fun _ => pure a)
seqRight x y := bind x fun _ => y ()
전체 계층 구조에서 상속된 메서드와 기본 메서드를 모두 추적해 보면, Monad 인스턴스에는 bind와 pure의 구현만 있으면 된다는 것을 알 수 있습니다. 다시 말해, Monad 인스턴스가 있으면 seq, seqLeft, seqRight, map, mapConst의 구현이 자동으로 따라옵니다. API 경계의 관점에서 보면, Monad 인스턴스가 있는 타입은 모두 Bind, Pure, Seq, Functor, SeqLeft, SeqRight 인스턴스를 얻습니다.
5.6.4. 연습 문제
-
Option과Except같은 예제를 직접 풀어 보면서Monad에 있는map,seq,seqLeft,seqRight의 기본 구현을 이해하십시오. 다시 말해, 이 타입들의bind와pure정의를 기본 정의에 대입한 뒤 단순화하여, 손으로 직접 작성했을 법한map,seq,seqLeft,seqRight버전을 복원하십시오. -
종이나 텍스트 파일에
map과seq의 기본 구현이Functor와Applicative의 계약을 만족한다는 것을 스스로 증명해 보십시오. 이 논증에서는 인자를 대입하는 일반적인 표현식 평가뿐 아니라Monad계약의 규칙도 사용할 수 있습니다.