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. Identity 모나드
모나드는 실패, 예외, 로깅과 같은 효과를 지닌 프로그램을 데이터와 함수로 이루어진 명시적 표현으로 인코딩합니다. 하지만 때로는 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과 동등해집니다. 하지만 이런 방식으로 호출하려면, Lean에게 의도한 모나드가 Id라는 힌트를 제공해야 합니다:
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의 결합 법칙은 기본적으로, 일어나는 일들의 순서만 유지된다면 순차 처리를 위한 부기(bookkeeping) 자체는 중요하지 않다는 것을 말해줍니다.