5.6. The Complete Definitions
관련된 언어 기능을 모두 소개했으므로, 이 절에서는 Lean 표준 라이브러리에 있는 Functor, Applicative, Monad의 완전하고 정직한 정의를 설명한다.
이해를 위해 어떤 세부 사항도 생략하지 않는다.
5.6.1. Functor
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
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 α이며, seqRight와 반환 타입이 f α라는 점만 다르다.
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. Monad
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 인스턴스를 얻는다.