4.2. 모나드 타입 클래스
모나드인 타입마다 ok나 andThen 같은 연산자를 일일이 임포트할 필요 없이, Lean 표준 라이브러리에는 이러한 연산자를 오버로드할 수 있게 해 주는 타입 클래스가 있어 어떤 모나드에든 같은 연산자를 사용할 수 있습니다. 모나드에는 ok 및 andThen에 해당하는 두 가지 연산이 있습니다:
class Monad (m : Type → Type) where
pure : α → m α
bind : m α → (α → m β) → m β이 정의는 약간 단순화한 것입니다. Lean 라이브러리의 실제 정의는 이보다 다소 복잡하며, 나중에 소개하겠습니다.
Option과 Except ε의 Monad 인스턴스는 각 타입의 andThen 연산 정의를 조금 고쳐서 만들 수 있습니다:
instance : Monad Option where
pure x := some x
bind opt next :=
match opt with
| none => none
| some x => next x
instance : Monad (Except ε) where
pure x := Except.ok x
bind attempt next :=
match attempt with
| Except.error e => Except.error e
| Except.ok x => next x
예를 들어, firstThirdFifthSeventh는 Option α 반환 타입과 Except String α 반환 타입에 대해 각각 따로 정의되었습니다. 이제는 이 함수를 어떤 모나드에 대해서든 다형적으로 정의할 수 있습니다. 다만 모나드마다 결과를 찾지 못하는 방식이 다를 수 있으므로, 조회 함수를 인자로 받아야 합니다. bind의 중위 연산자 버전은 >>=이며, 앞의 예제에서 ~~>가 하던 것과 같은 역할을 합니다.
def firstThirdFifthSeventh [Monad m] (lookup : List α → Nat → m α)
(xs : List α) : m (α × α × α × α) :=
lookup xs 0 >>= fun first =>
lookup xs 2 >>= fun third =>
lookup xs 4 >>= fun fifth =>
lookup xs 6 >>= fun seventh =>
pure (first, third, fifth, seventh)
느린 포유류와 빠른 새의 예시 목록이 주어지면, firstThirdFifthSeventh의 이 구현을 Option과 함께 사용할 수 있습니다:
def slowMammals : List String :=
["Three-toed sloth", "Slow loris"]
def fastBirds : List String := [
"Peregrine falcon",
"Saker falcon",
"Golden eagle",
"Gray-headed albatross",
"Spur-winged goose",
"Swift",
"Anna's hummingbird"
]#eval firstThirdFifthSeventh (fun xs i => xs[i]?) slowMammals#eval firstThirdFifthSeventh (fun xs i => xs[i]?) fastBirds
Except의 조회 함수 get의 이름을 더 구체적인 이름으로 바꾸고 나면, firstThirdFifthSeventh의 구현을 그대로 Except에도 사용할 수 있습니다:
def getOrExcept (xs : List α) (i : Nat) : Except String α :=
match xs[i]? with
| none =>
Except.error s!"Index {i} not found (maximum is {xs.length - 1})"
| some x =>
Except.ok x#eval firstThirdFifthSeventh getOrExcept slowMammals#eval firstThirdFifthSeventh getOrExcept fastBirds4.2.1. 일반적인 모나드 연산
수많은 타입이 모나드이기 때문에, 어떤 모나드에 대해서든 다형적인 함수는 매우 강력합니다. 예를 들어, mapM 함수는 Monad를 사용하여 함수를 적용한 결과들을 순서대로 실행하고 결합하는 map의 한 버전입니다:
def mapM [Monad m] (f : α → m β) : List α → m (List β)
| [] => pure []
| x :: xs =>
f x >>= fun hd =>
mapM f xs >>= fun tl =>
pure (hd :: tl)
함수 인자 f의 반환 타입에 따라 어떤 Monad 인스턴스가 사용될지 결정됩니다. 다시 말해, mapM은 로그를 생성하는 함수, 실패할 수 있는 함수, 가변 상태를 사용하는 함수에 모두 사용할 수 있습니다. f의 타입이 사용 가능한 효과를 결정하므로, API 설계자는 이러한 효과를 엄격하게 제어할 수 있습니다.
이 장의 도입부에서 설명했듯이, State σ α는 σ 타입의 가변 변수를 사용하고 α 타입의 값을 반환하는 프로그램을 나타냅니다. 이러한 프로그램은 실제로는 시작 상태를 받아 값과 최종 상태의 쌍을 돌려주는 함수입니다. Monad 클래스는 그 매개변수가 하나의 타입 인자를 받을 것을 요구합니다. 즉, 매개변수는 Type → Type이어야 합니다. 따라서 State에 대한 인스턴스는 상태 타입 σ를 명시해야 하며, 이 타입은 인스턴스의 매개변수가 됩니다:
instance : Monad (State σ) where
pure x := fun s => (s, x)
bind first next :=
fun s =>
let (s', x) := first s
next x s'
이는 bind로 순서가 정해진 get 호출과 set 호출 사이에서 상태의 타입이 바뀔 수 없다는 뜻이며, 이는 상태를 다루는 계산에 합리적인 규칙입니다. increment 연산자는 저장된 상태를 주어진 양만큼 증가시키고, 이전 값을 반환합니다:
def increment (howMuch : Int) : State Int Int :=
get >>= fun i =>
set (i + howMuch) >>= fun () =>
pure i
mapM을 increment와 함께 사용하면 리스트 항목의 합을 계산하는 프로그램이 됩니다. 더 구체적으로 말하면, 가변 변수에는 지금까지의 합이 담기고 결과 리스트에는 누적 합이 담깁니다. 다시 말해, mapM increment의 타입은 List Int → State Int (List Int)이며, State의 정의를 펼치면 List Int → Int → (Int × List Int)가 됩니다. 이 함수는 초기 합을 인자로 받으며, 그 값은 0이어야 합니다:
#eval mapM increment [1, 2, 3, 4, 5] 0
로깅 효과는 WithLog를 사용하여 표현할 수 있습니다. State와 마찬가지로, 그 Monad 인스턴스는 기록되는 데이터의 타입에 대해 다형적입니다:
instance : Monad (WithLog logged) where
pure x := {log := [], val := x}
bind result next :=
let {log := thisOut, val := thisRes} := result
let {log := nextOut, val := nextRes} := next thisRes
{log := thisOut ++ nextOut, val := nextRes}4.2.2. 항등 모나드
모나드는 실패, 예외, 로깅과 같은 효과를 지닌 프로그램을 데이터와 함수로 이루어진 명시적인 표현으로 인코딩합니다. 그러나 때로는 유연성을 위해 모나드를 사용하도록 API를 작성했는데도 정작 그 API의 클라이언트에게는 인코딩된 효과가 전혀 필요하지 않을 수 있습니다. 항등 모나드는 아무런 효과가 없는 모나드입니다. 항등 모나드를 사용하면 순수한 코드를 모나드 API와 함께 사용할 수 있습니다:
def Id (t : Type) : Type := t
instance : Monad Id where
pure x := x
bind x f := f x
pure의 타입은 α → Id α여야 하지만, Id α는 그저 α로 환원됩니다. 마찬가지로 bind의 타입은 α → (α → Id β) → Id β여야 합니다. 이 타입은 α → (α → β) → β로 환원되므로, 두 번째 인자를 첫 번째 인자에 적용하여 결과를 구할 수 있습니다.
항등 모나드를 사용하면 mapM은 map과 동등해집니다. 하지만 이런 방식으로 호출하려면 의도한 모나드가 Id라는 힌트를 Lean에 제공해야 합니다:
def numbers := mapM (m := Id) (do return · + 1) [1, 2, 3, 4, 5]
어떤 모나드를 사용해야 하는지에 대한 구체적인 단서를 타입이 전혀 제공하지 않는 문맥에서 mapM을 사용하면 “instance problem is stuck” 메시지가 나타납니다:
def numbers := mapM (do return · + 1) [1, 2, 3, 4, 5]4.2.3. 모나드 계약
BEq와 Hashable의 인스턴스 쌍이 모두 같은 두 값은 같은 해시를 갖도록 보장해야 하듯이, Monad의 각 인스턴스에도 지켜야 하는 규약이 있습니다. 첫째, pure는 bind의 왼쪽 항등원이어야 합니다. 즉, bind (pure v) f는 f v와 같아야 합니다. 둘째, pure는 bind의 오른쪽 항등원이어야 하므로, bind v pure는 v와 같습니다. 마지막으로, bind는 결합 법칙을 만족해야 하므로, bind (bind v f) g는 bind v (fun x => bind (f x) g)와 같습니다.
이 계약은 효과가 있는 프로그램에 기대되는 속성을 더 일반적인 형태로 규정합니다. pure에는 효과가 없으므로, bind로 그 효과를 순서대로 연결해도 결과가 달라지지 않아야 합니다. bind의 결합 법칙은 요컨대 일이 일어나는 순서만 유지된다면 순서를 연결하는 데 필요한 관리 작업 자체는 중요하지 않다는 뜻입니다.