4.2. The Monad Type Class
모나드인 각 타입마다 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. General Monad Operations
서로 다른 많은 타입이 모나드이므로 어떤 모나드에 대해서도 다형적인 함수는 매우 강력하다.
예를 들어 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. The Identity Monad
모나드는 실패, 예외, 로깅 같은 효과가 있는 프로그램을 데이터와 함수로 이루어진 명시적 표현으로 인코딩한다. 하지만 유연성을 위해 모나드를 사용하는 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 β여야 한다.
이는 α → (α → β) → β로 줄어들므로 두 번째 인수를 첫 번째 인수에 적용해 결과를 얻을 수 있다.
4.2.3. The Monad Contract
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의 결합성은 일이 일어나는 순서가 보존되는 한 순서 연결을 기록하는 방식 자체는 중요하지 않다는 뜻이다.