모나드는 함수형 언어에서 비내장 효과를 표현하고, 효과의 전파와 순서를 통일적으로 서술하는 강력한 의미론적 도구다. 이 장은 계산적 람다 계산을 기반으로 모나드와 클라이슬리 삼중항, 다양한 효과 모나드의 예, 모나드 변환과 그 의미 보존, 그리고 모나드를 활용한 프로그래밍 기법을 소개한다.
URL: https://xavierleroy.org/control-structures/book/main013.html
Title: Chapter 11 Monads
모나드는 함수형 언어에서 인기 있는 프로그래밍 패턴이다. 하스켈에서의 가변 상태, OCaml에서의 비제한(undelimited) 컨티뉴에이션처럼 언어가 본래 지원하지 않는 효과를 표현할 수 있게 해준다. 모나드는 또한 강력한 의미론적 장치이기도 하다. 프로그래밍 언어에서 효과의 전파와 순서를 일반적으로 다룰 수 있게 한다. 이 장의 모나드 소개는 의미론적 측면을 특히 강조하는데, 이는 12장(알제브라적 효과)의 이론을 전개하기 위한 출발점이 되기 때문이다(장12).
Denotational semantics은 명령형 언어의 문장 s 같은 구문적 객체에 수학적 객체 ⟦ s ⟧를 대응시키는 방식으로 진행된다. 6.2절과6.3절에서 보았듯이, 표상하려는 프로그래밍 언어의 기능에 따라 기호 의미(denotation)의 도메인이 달라진다. 예를 들어, 단순 명령형 언어 IMP의 경우 다음 네 가지 서로 다른 도메인을 고려했다:
⟦ s ⟧: Store → Store(1) ⟦ s ⟧: Store → Store + {⊥}(2) ⟦ s ⟧: Store → (Store → Store + {⊥}) → Store + {⊥}(3) ⟦ s ⟧: Env → Store → (Store → Store + {⊥}) → Store + {⊥}(4)
(1)에서는 문장 s가 변수에서 값으로의 사상을 보관하는 저장소(store)를 변환하는 저장소 변환기(store transformer) 라는 단순한 생각에서 출발한다. (2)에서는 반복문이 종료하지 않는 경우를 다루기 위해 “바닥”(⊥) 결과를 추가한다. (3)에서는 문장 s의 컨티뉴에이션을 명시적으로 만드는 CPS(continuation-passing style)로 전환한다. 마지막으로, (4)에서는 환경(environment) 을 매개변수로 추가하여 예를 들어 코드 라벨에 컨티뉴에이션을 연결할 수 있게 한다.
의미 도메인이 바뀜에 따라 기본 문장의 기호 의미도 바뀌지만, 그 직관적 의미는 동일하게 유지된다. 예를 들어, 아래는 위 네 도메인에서의 skip(“아무 것도 하지 않음”)과 x := e(대입)의 기호 의미다:
⟦ skip ⟧σ= σ⟦ x := e ⟧σ= σ x := ⟦ e ⟧σ, (2) ⟦ skip ⟧σ k= k σ⟦ x := e ⟧σ k= k σ x := ⟦ e ⟧σ ⟦ skip ⟧ρ σ k= k σ⟦ x := e ⟧ρ σ k= k σ x := ⟦ e ⟧σ
모든 경우에 ⟦ skip ⟧은 초기 저장소 σ를 그대로 돌려주고, ⟦ x := e ⟧은 x의 값을 갱신한 후의 σ를 돌려준다. 다만 그 저장소를 “돌려주는” 방식이 서로 다를 뿐이다.
이 현상은 s 1; s 2 같은 제어 구조(순차 실행)에서는 더욱 두드러진다.
⟦ s 1;s 2 ⟧σ= ⟦ s 2 ⟧(⟦ s 1 ⟧σ)(1) ⟦ s 1; s 2 ⟧σ=⎧ ⎨ ⎩⊥if ⟦ s 1 ⟧σ = ⊥ ⟦ s 2 ⟧(⟦ s 1 ⟧σ)otherwise(2) ⟦ s 1; s 2 ⟧σ k= ⟦ s 1 ⟧(λ σ′.⟦ s 2 ⟧σ′k)(3) ⟦ s 1; s 2 ⟧ρ σ k= ⟦ s 1 ⟧(λ σ′.⟦ s 2 ⟧ρ σ′k)(4)
모든 경우에 s 1의 실행이 종료한다면 그 끝의 저장소가 s 2 실행의 초기 저장소가 된다. 그러나 이 직관을 수학적으로 표현하는 방식은 네 가지가 된다.
이 지점에서의 질문은 다음과 같다: 대입과 순차 실행 같은 기본 구성의 기호 의미를, 의미 도메인이 바뀌더라도 동일한 의미 방정식으로 남도록 줄 수 있는가?
프로그램 변환은 또 다른 의미 부여 방식이다. 복잡한 언어를 더 단순하고 잘 이해된 언어로 번역한다. 예를 들어, 6.5절의 CPS 변환은 함수형 언어에서 이름에 의한 호출과 값에 의한 호출의 차이를 분명히 해준다.
표준 의미론의 경우와 마찬가지로, FUN 같은 함수형 언어에 대한 프로그램 변환들 사이에도 공통점이 있다. 6.5절의 값-호출 CPS 변환 𝒞, 8.4절의 이중 배럴 CPS 변환 𝒞 2, 그리고 같은 8.4절의 ERS(exception-returning style) 변환 ℰ를 보자. 상수, 변수, 함수 추상에 대한 번역은 다음과 같다:
𝒞(c)= λ k . k c 𝒞(x)= λ k . k x 𝒞(λ x . e)= λ k . k(λ x . 𝒞(e)) 𝒞 2(c)= λ k . λ k′ . k c 𝒞 2(x)= λ k . λ k′ . k x 𝒞 2(λ x . e)= λ k . λ k′ . k(λ x . 𝒞 2(e)) ℰ(c)= V c ℰ(x)= V x ℰ(λ x . e)= V(λ x . ℰ(e))
세 경우 모두에서, 표현식의 값은 즉시 결과로 “반환”되지만, 그 반환 방식은 서로 다르다. 𝒞에서는 이어지는 컨티뉴에이션에 값을 전달하고, 𝒞 2에서는 첫 번째 컨티뉴에이션에 전달하며, ℰ에서는 V 생성자로 값을 감싼다.
함수 적용에 대한 번역도 보자:
𝒞(e 1 e 2)= λ k . 𝒞(e 1)(λ f . 𝒞(e 2)(λ v . f v k)) 𝒞 2(e 1 e 2)= λ k . λ k′ . 𝒞 2(e 1)(λ f . 𝒞 2(e 2)(λ v . f v k)k′)k′ ℰ(e 1 e 2)= match ℰ(e 1)with E x → E x ∣ V f → match ℰ(e 2)with E x → E x ∣ V v → f v
세 변환 모두 먼저 함수 e 1을 평가하여 그 값을 f에 바인딩하고, 다음에 인자 e 2를 평가하여 그 값을 v에 바인딩한 뒤, 마지막에 f를 v에 적용한다. 서로 다른 점은 평가가 낸 값을 어떻게 바인딩하고, 예외를 내는 평가를 어떻게 다루느냐이다.
이 지점에서의 질문은 다음과 같다: 서로 다른 계산 표상과 상이한 언어 확장을 다루더라도, 함수 추상과 함수 적용 같은 기본 구성에 대한 변환 정의를 여러 프로그램 변환 간에 공유할 수 있는가?
Eugenio Moggi는 계산적 람다 계산(computational lambda-calculus) 과 그에 대한 범주론적 의미론인 모나드 를 도입하여 위 두 질문에 모두 긍정적으로 답했다(Moggi, 1989, Moggi, 1991). 계산적 람다 계산은 표기 의미론과 프로그램 변환의 “메타-언어”로 쓰인다. 즉, 기호 의미 방정식 ⟦ s ⟧ = …과 변환 방정식 𝒞(e) = …의 우변을 적는 언어다.
구문. 계산적 람다 계산의 구문은 다음과 같다:
Values: v::=c 상수 ∣x 변수 ∣λ x . M 함수 추상 Computations: M, N::=v 1 v 2 함수 적용 ∣if v then M else N 조건식 ∣val v 사소한 계산 ∣do x ⇐ M in N 계산의 순차 실행 ∣…모나드 고유 연산들
이 구문은 값 과 계산 을 엄격히 구분한다. 값은 계산이 내는 최종 결과이고, 계산은 궁극적으로 값을 내되 그 과정에서 발산(비종료), 입출력, 예외, 백트래킹(비결정성) 등의 다양한 효과 를 수행할 수 있는 과정이다. Paul Blain Levy의 기억에 남는 표현대로, “값은 존재하고; 계산은 한다(values are; computations do).”
값에는 상수(불리언, 정수 등), 변수, 함수 추상이 포함된다. 계산에는 함수 적용과 if-then-else 조건이 포함된다. 적용의 함수부와 인자부가 모두 값이어야 하므로, 적용은 값-호출을 사용하고 평가 순서에 무감각하다. val v는 값을 즉시 산출하는 사소한 계산이다. do x ⇐ M in N은 계산 M과 N을 순서대로 실행하고, M이 낸 값을 N의 실행 동안 x에 바인딩한다. 이는 효과의 전파를 처리한다. 다양한 종류의 효과는 11.3절에서 보듯이 계산을 위한 더 많은 생성자를 추가하여 만들 수 있다(절11.3).
타입.값과 계산의 구분은 타입 시스템에도 드러난다. 타입 T A는 A 타입의 값을 산출하는 계산을 뜻한다.
Value types: A::=ι 기저 타입(bool, int, …) ∣A → B 함수 타입 Computation types: B::=T A A 값을 산출하는 계산
그림11.1은 타이핑 규칙을 요약한다.
Γ ⊢ x : Γ(x)
Γ ⊢ true : bool
Γ ⊢ false : bool
Γ, x : A ⊢ M : B
Γ ⊢ λ x . M : A → B
Γ ⊢ v 1 : A → B Γ⊢ v 2 : A
Γ ⊢ v 1 v 2 : B
Γ ⊢ v : bool Γ⊢ M : B Γ⊢ N : B
Γ ⊢ if v then M else N : B
Γ ⊢ v : A Γ ⊢ val v : T A
Γ ⊢ M : T A Γ, x : A ⊢ N : B
Γ ⊢ do x ⇐ M in N : B
그림 11.1: 계산적 람다 계산의 타이핑 규칙.
클라이슬리 삼중항.다양한 효과는 타입 생성자 T의 서로 다른 해석을 통해 계산적 람다 계산에서 모델링할 수 있다. 예를 들어, T X = X는 계산이 곧 값인, 효과가 없는 순수 언어를 준다. 반면 T X = 𝒫(X) (X의 집합)는 비결정성을 모델링하며, 계산이 가능한 값들의 집합을 산출한다.
어떤 T의 해석이든 적절한 ret와 bind 연산을 동반해야 한다. 모든 타입 X, Y에 대해
ret: X → T X bind: T X → (X → T Y) → T Y
ret v는 Moggi (1991)에서는 η(v)로도 쓰며, 값을 계산의 세계로 주입한다. 이는 계산적 람다 계산의 val v 생성자의 의미를 이룬다.
bind M F는 Moggi (1991)에서는 F*(M)으로도 쓰며, 값에서 계산으로 가는 함수 F: X → T Y를 계산에서 계산으로 가는 함수 F*: T X → T Y로 변환하고, 이를 계산 M에 적용한다. do x ⇐ M in N의 의미는 bind M(λ x . N)으로 주어진다.
(T, ret, bind)를 묶어 클라이슬리 삼중항(Kleisli triple) 이라 한다. 특히, ret와 bind는 다음 세 가지 법칙을 만족해야 한다:
bind(ret v)F= F v(M1) bind M(λ x . ret x)= M(M2) bind(bind M F)G= bind M(λ x . bind(F x)G)(M3)
대략적으로 (M1)과 (M2)는 ret가 bind의 항등원임을, (M3)는 bind가 결합법칙을 만족함을 말한다.
이 세 클라이슬리 법칙은 프로그래밍 언어 세계에서는 “모나드의 세 법칙”으로 알려져 있는데, 아래 이유 때문이다.
모나드와의 연결.범주론에서 모나드 는 (T, η, µ) 삼중으로, T는 함자이고
T(f): T X → T Y if f: X → Y η: X → T X µ: T(T X) → T X η; µ= id = T(η); µ T(µ); µ= µ; µ
직관을 위해, T를 T X = 𝒫(X)(X의 부분집합들) 같은 컨테이너 타입으로 생각하자. 그러면 η는 원소 x를 단원소 컨테이너 {x}로 주입하는 것이고, µ는 컨테이너들의 컨테이너를 평탄화(flatten)하여 하나의 컨테이너로 만드는 것이다:
µ(M) =∪ x ∈ M x
모나드 (T, η, µ)가 주어지면, 다음과 같이 T 위의 클라이슬리 삼중항을 정의할 수 있다.
ret v= η(v) bind a f= µ(T(f)a)
반대로, 클라이슬리 삼중항 (T, ret, bind)가 주어지면, 다음과 같이 T 위의 모나드를 정의할 수 있다.
T(f)= λ M . bind M(λ x . ret(f x)) η(v)= ret v µ(M)= bind M(λ x . x)
모나드와 클라이슬리 삼중항의 연결은 매우 밀접하여, 프로그래밍 언어 연구자들은 클라이슬리 삼중항을 일컬어 “모나드”라고 부른다. 즉, 프로그래밍 언어의 모나드는 위의 세 법칙(M1), (M2), (M3)을 만족하는 ret와 bind 연산이 딸린 타입 생성자 T를 말한다.
등식 이론.계산적 람다 계산에 축약 의미론을 주는 것은 크게 유익하지 않다. 그런 의미론은 val과 do를 해석하는 데 사용하는 특정 모나드에 크게 의존하기 때문이다. 대신 Moggi (1991)는 두 항이 계산적으로 동치임을 증명할 수 있는 등식 이론 을 전개한다. 항들의 동치(≡로 표기)는 다음 규칙들을 포함하는 합동(congruence) 관계다:
(λ x . M)v≡ M x := v if true then M else N≡ M if false then M else N≡ N do x ⇐ val v in M≡ M x := v do x ⇐ M in val x≡ M(M2) do x ⇐ (do y ⇐ M in N) in P≡ do y ⇐ M in(do x ⇐ N in P)(M3)
첫 세 등식은 함수 적용과 조건식에 대한 익숙한 축약 규칙의 “대칭화된” 버전이다. 마지막 세 등식은 모나드의 세 법칙이다.
이제 다양한 효과를 구현하는 몇 가지 모나드를 설명한다. 각 모나드는 그 클라이슬리 삼중항 (T, ret, bind)과, 예외 모나드의 예외 발생·처리처럼 계산적 람다 계산에 더해지는 고유 연산으로 서술한다.
T X=X + {⊥} ret v=v bind M F=⎧ ⎨ ⎩⊥if M = ⊥ F M otherwise
부분성 모나드는 종료하지 않는 계산을 특별한 “바닥” 결과 ⊥로 표현하여 지원한다. 이 모나드의 전형적 연산은 고정점 조합자다.
fix:⎛
⎝(A → T B) → (A → T B)⎞
⎠→ (A → T B)
이 모나드는 또한 치명적 오류를 표현하는 데도 사용할 수 있는데, ⊥가 잡을 수 없는 예외를 나타낸다.
T X=𝒫(X) (X의 부분집합들) ret v={v} bind M F=∪ v ∈ M F v
비결정성 모나드는 난수 추출처럼 여러 서로 다른 결과를 낼 수 있는 계산, 그리고 실패하여 아무 결과도 내지 않는 계산을 지원한다. 계산은 값들의 집합으로 표현된다. 이 모나드의 연산에는 choose(비결정적 선택)와 fail(실패)이 포함된다.
choose:T A → T A → T A fail:T A choose M N=M ⋃ N fail=∅
T X=X + Exn ret v=inj 1(v) bind(inj 1(v))F=F v bind(inj 2(e))F=inj 2(e)
예외 모나드는 값을 내거나 예외를 던지는 계산을 지원한다. bind M F는 M이 던진 예외를 전파하며, F의 평가를 건너뛴다. 주요 연산은 예외를 던지는 raise와, 계산에서 발생하는 예외를 잡아 처리하는 handle이다:
raise:Exn → T A handle:T A → (Exn → T A) → T A raise e=inj 2(e)handle M F=⎧ ⎨ ⎩inj 1(v)if M = inj 1(v) F v if M = inj 2(v)
T X=(X → Res) → Res ret v=λ k . k v bind M F=λ k . M(λ x . F x k)
컨티뉴에이션 모나드는 타입 T A의 계산의 컨티뉴에이션을 A → Res 함수로 명시화한다. 여기서 Res는 전체 프로그램 결과의 타입이다. 이 모나드는 callcc 같은 제어 연산자를 지원한다:
callcc:(Cont A → T A) → T A throw:Cont A → A → T B callcc F=λ k . F k k throw k v=λ k′ . k v
여기서 Cont A는 A → Res, 즉 A 값을 기대하는 컨티뉴에이션의 타입을 뜻한다.
T X=Store → X × Store ret v=λ σ . (v,σ) bind M F=λ σ . let(x,σ′) = M σ in F x σ′
상태 모나드는 명령형 변수와 가변 데이터 구조를 지원한다. 메모리 상태는 현재 값을 메모리 위치에 대응시키는 저장소로 표현한다. 계산은 초기 저장소를 추가 인자로 받아 최종 저장소를 추가 결과로 돌려준다. bind M F는 저장소를 평가 과정에 꿰어 준다. 즉 M의 최종 저장소를 F의 초기 저장소로 넘긴다.
이 모나드의 전형적 연산은 참조(메모리 위치)의 현재 값을 읽는 get과, 그 값을 갱신하는 set이다.
get:Ref A → T A set:Ref A → A → T A get ℓ=λ σ . (σ(ℓ), σ)set ℓ v=λ σ . ((), σ [ℓ ↦ v])
T X=Env → X ret v=λ ρ . v bind M F=λ ρ . F(M ρ)ρ
환경 모나드(리더 모나드)는 상태 모나드의 단순화 버전으로, 계산이 인자로 환경 ρ(참조에서 값으로의 사상)를 받지만 수정된 환경을 반환하지 않는다. 따라서 bind M F는 동일한 환경 ρ를 M과 F에 모두 전달한다.
전형적 연산은 환경에서 ℓ에 대응된 값을 얻는 lookup ℓ과, M을 평가하는 동안만 환경에서 ℓ을 v로 임시 설정하는 assign ℓ v M이다.
lookup:Ref A → T A assign:Ref A → A → T B → T B lookup ℓ=λ ρ . ρ(ℓ)assign ℓ v M=λ ρ . M ρ [ℓ ↦ v]
T X=X × String ret v=(v, ε) bind M F=let(x, w 1) = M in let(y, w 2) = F x in(y, w 1 . w 2)
출력 모나드(라이터/로깅 모나드)는 계산 중에 출력된 문자열을 수집한다. ret는 빈 출력 ε를 만들고, bind M F는 M과 F가 생성한 출력을 연결한다. 이 모나드의 전형적 연산은 주어진 문자열을 출력하는 print다:
print:String → T Unit print s=((), s)
라이터 모나드는 문자열 대신 임의의 모노이드(연결 연산과 항등원을 갖춘 타입)를 사용할 수 있다.
확률.비결정적 계산에 대해 가능한 결과들에 확률을 부여할 수도 있다. 예를 들어, 편향된 동전 던지기 flip p를 제공하여 true가 나올 확률이 p, false가 나올 확률이 1−p가 되도록 할 수 있다.
분포 모나드는 각 가능한 결과 값에 확률을 부여함으로써 비결정성 모나드를 확장한다. 즉, 가능한 결과들의 집합 𝒫(X)은 각 x: X에 대해 x가 결과로 나올 확률을 주는 함수 X → [0,1]로 바뀐다. 이 확률들의 합은 1이어야 한다.
T X=X → [0,1] ret v=λ x . if x=v then 1 else 0 bind M F=λ x .∑ v M v · F v x flip p=λ x . if x then p else 1−p
특히 bind M F가 값 x를 돌려줄 확률은, 중간 값 v에 대해 M이 v를 돌려줄 확률과 F v가 x를 돌려줄 확률의 결합 확률을 모두 합한 것이다.
기대값 모나드는 컨티뉴에이션 모나드를 확장하여, 컨티뉴에이션을 가능한 결과들의 집합 𝒫(X)에 대한 측도 µ: X → [0,1]로 다룬다(이 접근의 예시는 7.6절을 보라7.6).
T X=(X → [0,1]) → [0,1] ret v=λ µ . µ v bind M F=λ µ . M(λ x . F x µ) flip p=λ µ . p · µ true + (1−p) · µ false
복합 효과를 위한 모나드.두 모나드를 일반적으로 합성하는 구성은 없다. 그러나 동시에 지원하려는 두 가지 이상의 효과가 주어지면, 그에 맞는 모나드를 고안하는 것은 보통 어렵지 않다. 다음은 복합 효과를 위한 모나드 예시들이다( ret와 bind의 정의는 독자에게 연습문제로 남긴다).
상태와 예외: T X = State → (X + Exn) × State
상태와 컨티뉴에이션: T X = State → (X → State → Res) → Res
예외와 컨티뉴에이션(8.4절의 이중 배럴 CPS 접근 사용): T X = (X → Res) → (Exn → Res) → Res
비결정성과 컨티뉴에이션(7.5절의 “성공/실패 컨티뉴에이션” 접근 사용): T X = (X → (Unit → Res) → Res) → (Unit → Res) → Res
여기서 Unit → Res는 실패 컨티뉴에이션이고, X → (Unit → Res) → Res는 성공 컨티뉴에이션이다.
대신 모나드 변환기(monad transformer) 를 사용해, 어떤 모나드를 인자로 받아 그 기능을 다른 모나드에 더할 수 있다. 예시는 Newbern et al. (2025)을 보라.
모나드 변환은 함수형 언어를 계산적 람다 계산으로 번역한다. 다음은 핵심 FUN 언어의 표현식 e를 변환한 ℳ(e)이다:
ℳ(c)= val c ℳ(x)= val x ℳ(λ x . e)= val(λ x . ℳ(e)) ℳ(e 1 e 2)= do f ⇐ ℳ(e 1) in do v ⇐ ℳ(e 2) in f v ℳ(if e 1 then e 2 else e 3)= do b ⇐ ℳ(e 1) in if b then ℳ(e 2)else ℳ(e 3)
이 번역은 계산적 람다 계산의 val과 do 구성에 의미를 부여하는 데 어떤 모나드를 쓰는지에 독립적이다. 그러나 컨티뉴에이션 모나드를 쓰면 val v는 λ k . k v가 되고 do x ⇐ M in N은 λ k . M(λ x . N k)가 되어, 값-호출 CPS 변환 𝒞를 회수하게 된다. 마찬가지로 예외 모나드를 쓰면 ERS 변환 ℰ를 회수한다.
값-호출 대 이름-호출.목표 모나드에 독립적이더라도, 모나드 변환은 특정 평가 전략을 포착한다. 위의 ℳ 변환은 값-호출을 구현한다. 함수 적용 e 1 e 2의 인자 e 2를 함수 e 1에 넘기기 전에( do 바인딩으로) 값으로 축약하며, 그 결과 변수 x는 값에 바인딩된다. 반대로, 다음은 이름-호출을 구현하는 모나드 번역 𝒩(e)이다:
𝒩(c)= val c 𝒩(x)= x() 𝒩(λ x . e)= val(λ x . 𝒩(e)) 𝒩(e 1 e 2)= do f ⇐ 𝒩(e 1) in f(λ () . 𝒩(e 2)) 𝒩(if e 1 then e 2 else e 3)= do b ⇐ 𝒩(e 1) in if b then 𝒩(e 2)else 𝒩(e 3)
이름-호출의 요점은 변수가 값이 아니라 계산에 바인딩된다는 것이다. 함수 적용 e 1 e 2의 인자 e 2는 𝒩(e 2)로 평가되지 않은 채 전달된다. 우리의 계산적 람다 계산의 구문 제약을 수용하려면, 𝒩(e 2) 같은 계산을 그대로 전달하는 대신 썽크 λ () . 𝒩(e 2)를 전달하고, 이를 ()에 적용해 계산을 복구해야 한다. 이는 5.4절에서 이름-호출을 값-호출 언어에 부호화할 때 사용했던 것과 같은 트릭이다(절5.4).
FUN에 효과 추가. 핵심 FUN 언어의 번역을 그대로 두면서, 새 구성으로 확장된 FUN을 다루기 위해 번역 규칙을 더할 수 있다. 예를 들어, 발산할 수 있는 재귀적 함수 정의로 FUN을 확장하려면 다음 경우를 추가한다:
ℳ(let rec f x = e 1 in e 2) = do f ⇐ fix(λ f . λ x . ℳ(e 1)) in ℳ(e 2)
그리고 변환된 항은 부분성 모나드에서 해석한다. 마찬가지로 예외 처리를 FUN에 추가하려면 번역 규칙 두 개를 더한다:
ℳ(raise e)= do v ⇐ ℳ(e) in raise v ℳ(try e 1 with x → e 2)= handle ℳ(e 1)(λ x . ℳ(e 2))
그리고 변환된 항은 예외 모나드에서 해석한다.
타이핑. 모나드 변환 ℳ은 원 소스 FUN 항에 부여할 수 있는 단순 타입을 다음 의미에서 보존한다:
if Γ ⊢ e : τ, then ↑Γ ⊢ ℳ(e) : T↑τ
여기서 ↑τ는 함수 결과 타입 앞에 T를 붙인 간단한 변환이다:
↑ι = ι ↑(σ → τ) = ↑σ → T↑τ
특히 e가 예컨대 bool 타입의 닫힌 프로그램이면, 그 모나드 번역 ℳ(e)는 T bool 타입의 닫힌 프로그램이다.
이름-호출 변환 𝒩도 단순 타입을 보존한다. 값-호출과의 유일한 차이는 자유 변수와 함수 인자가 이제 중단된 계산이므로 그 타입 앞에 unit → T를 붙여야 한다는 점이다. 보다 정확히는:
if Γ ⊢ e : τ, then ⇑Γ ⊢ ℳ(e) : T↑τ
where
↑ι = ι ↑(σ → τ) = ⇑σ → T↑τ ⇑τ = unit → T↑τ
의미 보존.모나드 변환 ℳ은 FUN의 값-호출 의미를 보존하고, 𝒩 변환은 이름-호출 의미를 보존한다.
정리 1 모든 항 e와 상수 c에 대해,
값-호출의 경우에 대한 증명 개요를 제시한다. 먼저, FUN 값 v의 번역 v를 다음과 같이 정의한다.
c= c λ x . e= λ x . ℳ(e)
이 정의를 통해 주장을 강화할 수 있다. e →v*v이고 v가 값이면, ℳ(e) ≡ val v이다.
둘째, ℳ의 유용한 두 가지 구문적 성질을 증명한다. v가 값일 때,
ℳ(v)= val v(A) ℳ(e [x := v])= ℳ(e) x :=v
마지막으로, e →v e′이면 ℳ(e) ≡ ℳ(e′)임을 증명한다. 결과는 ≡의 추이성과 성질 (A), (B)에서 따른다. β-축약의 경우를 보이자.
ℳ((λ x . e)v)= do f ⇐ ℳ(λ x . e) in do y ⇐ ℳ(v) in f y = do f ⇐ val(λ x . ℳ(e)) in do y ⇐ val v in f y(by A) ≡ do y ⇐ val v in(λ x . ℳ(e))y(by M1) ≡ (λ x . ℳ(e))v(by M1) ≡ ℳ(e) [x :=v](by β) = ℳ(e [x := v])(by B)
컨티뉴에이션은 먼저 의미론적 도구로(장6) 도입되었으나, 곧 함수형 언어에서 CPS로 프로그래밍하는 데 널리 쓰이게 되었다(장7). 비슷하게, 모나드는 Moggi (1989)가 의미론적 도구로 도입했지만, 곧 Wadler (1992)와 하스켈 커뮤니티의 작업을 거쳐 중요한 함수형 프로그래밍 기법이 되었다. 이런 모나딕 스타일에서는, 프로그램을 특정 모나드의 ret, bind 및 고유 연산을 참조하는 순수 함수형 스타일로 작성한 뒤, 표준 라이브러리가 제공하는 적절한 모나드 구현과 연결(link)한다.
언어 비내장 효과 사용.함수형 프로그래밍에서 모나드를 사용하는 첫 번째 이유는 사용 중인 함수형 언어가 본래 지원하지 않는 효과를 제공하기 위해서다. 예를 들어 하스켈은 순수 함수형 언어이므로 부분성(일반 재귀 함수)을 본래 지원하지만, 그 외의 효과는 없다. 입출력, 가변 상태, 오류/예외, 제어 연산자는 표준 라이브러리에 정의된 모나드로 제공된다(Newbern et al., 2025). 이들 중 일부는 순수 하스켈로 구현되고, IO 모나드처럼 일부는 컴파일러와 런타임 시스템의 특별 지원을 받는 명령형 구현을 사용하지만, 모나드 인터페이스가 그들이 순수 함수형 구현처럼 행동하도록 보장한다.
또 다른 예로, OCaml은 입출력, 가변 상태, 예외를 본래 지원하지만 OCaml 5의 이펙트 핸들러 도입 전에는 제어 연산자를 제공하지 않았다. 이전에는 경량 스레드와 비동기 입출력을 위한 Lwt와 Async 라이브러리가 컨티뉴에이션 모나드를 사용하는 모나딕 프로그래밍 스타일에 의존했다(Vouillon, 2008).
마지막으로, 증명 지향 함수형 언어 F*는 본래 순수하고 종료하는 프로그램만을 지원한다. 부분성(일반 재귀)을 포함한 모든 효과는 모나드 계층을 통해 제공되며, 이는 함수 명세와 검증의 구조화에도 쓰인다(Swamy et al., 2016).
모나드로 프로그램 구조화. 모나드는 모나드가 저수준 세부사항을 일부 숨기고 고수준 구조를 강조하는 프로그래밍 스타일을 장려한다.
예를 들어, 많은 열거 문제는 리스트 모나드에서의 비결정적 계산으로 표현하면 가장 잘 드러난다. 주어진 리스트의 모든 순열을 구성하는 문제를 생각해 보자. 다음은 하스켈로 쓴 직접적(비모나딕) 해법이다:
permut :: [a] -> [[a]] permut [] = [[]] permut (x:xs) = concat (map (insert x) (permut xs))
insert :: a -> [a] -> [[a]] insert x [] = [[x]] insert x (y:ys) = (x:y:ys) : map (y:) (insert x ys)
리스트의 리스트를 다루는 연산이 많아, 이 코드가 무엇을 하는지 즉시 분명하지 않다. 다음은 같은 알고리즘을 리스트 모나드에서 수행할 “주어진 리스트의 임의의 순열을 찾는” 비결정적 계산으로 다시 표현한 것이다:
permut :: [a] -> [[a]] permut [] = [[]] permut (x:xs) = do ys <- permut xs; insert x ys
위 코드는 더 읽기 쉽다. x:xs의 순열을 구하려면, xs의 순열 ys를 하나 구한 뒤 x를 ys 안의 임의 위치에 삽입하라. insert도 더 명확히 만들 수 있다:
insert :: a -> [a] -> [[a]] insert x ys = return (x:ys) ++ case ys of [] -> [] y:ys ->do zs <- insert x ys; return (y:zs)
이 코드는 다음처럼 읽힌다. x를 ys의 임의 위치에 삽입하려면, 머리에 삽입(x:ys)하거나, ys가 비어 있지 않다면 꼬리 ys의 임의 위치에 x를 삽입하라.
또 다른 예로, OCaml 프로그램에서 참조와 배열 대입 같은 명령형 동작을 백트래킹하는 문제를 생각해 보자. (Paul-Elliot Anglès d’Auriac 제공) 한 해법은 계산의 값과 그 계산이 수행한 명령형 동작을 되돌리는 “undo” 함수를 쌍으로 본 “되돌릴 수 있는(undoable)” 계산의 모나드를 정의하는 것이다:
type 'a undo = 'a * (unit -> unit) let ret (x: 'a) : 'a undo = (x, (fun () -> ())) let bind (m: 'a undo) (f: 'a -> 'b undo) : 'b undo = let (x, undo1) = m in let (y, undo2) = f x in (y, (fun () -> undo2(); undo1()))
let array_set (arr: 'a array) (idx: int) (new_v: 'a) : unit undo = let old_v = arr.(idx) in arr.(idx) <- new_v; ((), (fun () -> arr.(idx) <- old_v))
undo 모나드는 라이터 모나드의 변형으로, 문자열 대신 unit -> unit 타입의 undo 함수를 출력으로 사용한다. ret 연산은 항등 undo 함수 fun () -> ()를 낸다. array_set 같은 명령형 연산은 배열의 이전 상태를 복원하는 함수를 낸다. bind 연산은 순차적으로 실행되는 두 계산의 undo 함수를 (올바른 순서로) 합성한다.
모나드 다형성.많은 모나딕 함수는 어떤 모나드와도, 또는 특정 효과를 지원하는 모나드와도 함께 사용할 수 있다. 이런 모나드-다형 함수는 하스켈의 타입 클래스 메커니즘 덕분에 정의와 재사용이 쉽다. 예를 들어, 다음은 리스트에 대한 일반 모나딕 map 함수다:
mmap :: Monad m => (t -> m a) -> [t] -> m [a] mmap f [] = return [] mmap f (x:xs) = do y <- f x; ys <- mmap f xs; return (y:ys)
mmap의 타입에 주목하라. Monad 타입 클래스의 임의의 인스턴스 m에 적용된다. 예외 모나드와 함께 쓰면 매핑된 함수가 던진 예외를 전파한다. I/O 모나드와 함께 쓰면 그 함수가 수행한 I/O를 순차화한다. 항등 모나드와 함께 쓰면 리스트에 대한 표준(비모나딕) map과 동일하다.
또 다른 예로, 두 인자의 순수 함수를 모나딕 함수로 들어올리는 liftM2를 보자:
liftM2 :: Monad m => (t1 -> t2 -> b) -> m t1 -> m t2 -> m b liftM2 f xx yy = do x <- xx; y <- yy; return (f x y)
Maybe 모나드와 함께 쓰면, liftM2 f는 인자들이 Just x와 Just y일 때 Just (f x y)를, 어느 한쪽이 Nothing이면 Nothing을 돌려준다. 하지만 리스트 모나드와 함께 쓰면, liftM2 f l1 l2는 l1의 원소 하나와 l2의 원소 하나에 f를 적용한 모든 결과의 리스트를 돌려준다. 예를 들어 liftM2 (+) [1,2,3] [4,5,6,7]은 [5,6,7,8,6,7,8,9,7,8,9,10]이다.
모나드로 프로그래밍하는 튜토리얼은 매우 많다. Wadler (1995)는 초기 작업 중 하나이지만 여전히 좋은 입문서다. Newbern et al. (2025)은 하스켈에서의 모나딕 프로그래밍을 심도 있게 다루며, 여러 효과를 지원하는 모나드를 구성하기 위한 모나드 변환기의 사용도 포함한다. Clarkson et al. (2025, section 8.8)은 OCaml에서의 모나딕 프로그래밍을 설명한다.
모나드 외에도, 범주론에서 영감을 받은 함수형 프로그래밍의 다른 “디자인 패턴”이 있다: 코모나드(Uustalu and Vene, 2008), 어플리케이티브 구조(McBride and Paterson, 2008), 그리고 애로우(Hughes, 2000). 어플리케이티브와 애로우는 모나드의 bind 연산에 내재된 엄격한 순차 실행보다 더 유연한 방식으로 효과적 계산을 합성하는 수단을 제공한다. 코모나드는 “공효과(coeffects)”, 즉 계산이 환경에 의존하는 방식을 기술한다.
알제브라적 효과 이론(장12)은 모나드 이론 다음 단계로 볼 수 있다. 모나드는 효과의 전파와 순차 실행만을 설명하지만, 알제브라적 효과는 효과의 생성과 처리까지도 설명한다.
