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가 있다는 점이 다릅니다. 이 정의도 몇 가지 표준적인 문법적 설탕(syntactic sugar)을 먼저 도입한 다음 일부 이름을 그 정의로 치환하면 비슷하게 이해할 수 있습니다:
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는 Applicative를 Bind로 확장한 모나드입니다:
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(모나드) 계약의 규칙도 사용할 수 있습니다.