4.5. The IO Monad🔗

모나드로서의 IO는 프로그램 실행 절에서 설명한 두 관점으로 이해할 수 있다. 두 관점 모두 IO에서 pure와 bind가 의미하는 바를 이해하는 데 도움이 된다.

첫 번째 관점에서 IO 동작은 Lean의 런타임 시스템에 보내는 명령이다. 예를 들어 “이 파일 디스크립터에서 문자열을 읽은 다음, 그 문자열과 함께 순수 Lean 코드를 다시 호출하라”는 명령일 수 있다. 이 관점은 운영 체제의 입장에서 프로그램을 바라보는 외부 관점이다. 이 경우 pure는 RTS에 어떤 효과도 요청하지 않는 IO 동작이고, bind는 RTS에 효과를 일으킬 수 있는 연산 하나를 먼저 수행한 다음 그 결과값과 함께 프로그램의 나머지를 호출하도록 지시한다.

두 번째 관점에서 IO 동작은 세계 전체를 변환한다. IO 동작은 고유한 세계를 인수로 받아 변경된 세계를 반환하므로 실제로는 순수하다. 이 관점은 Lean 내부에서 IO가 표현되는 방식에 대응하는 내부 관점이다. Lean에서는 세계를 토큰으로 표현하며, IO 모나드는 각 토큰이 정확히 한 번만 사용되도록 구성되어 있다.

이것이 어떻게 작동하는지 보려면 정의를 한 번에 하나씩 벗겨 보는 것이 도움이 된다. #print 명령은 Lean 데이터 타입과 정의의 내부를 보여 준다. 예를 들어 다음과 같다.

실행 결과는 다음과 같다.

inductive Nat : Type
number of parameters: 0
constructors:
Nat.zero : Nat
Nat.succ : Nat → Nat

그리고

실행 결과는 다음과 같다.

def String.toLower : String → String :=
fun s => String.map Char.toLower s

때로는 #print의 출력에 이 책에서 아직 소개하지 않은 Lean 기능이 포함된다. 예를 들어 다음과 같다.

다음 결과를 만든다.

def List.head?.{u} : {α : Type u} → List α → Option α :=
fun {α} x =>
  match x with
  | [] => none
  | a :: tail => some a

정의 이름 뒤에 .{u}가 포함되고 타입에 단순히 Type이 아니라 Type u라는 주석이 붙는다. 지금은 이를 안전하게 무시해도 된다.

IO의 정의를 출력하면 더 단순한 구조를 이용해 정의되었음을 알 수 있다.

@[reducible] def IO : Type → Type :=
EIO IO.Error

IO.Error는 IO 동작이 던질 수 있는 모든 오류를 나타낸다.

inductive IO.Error : Type
number of parameters: 0
constructors:
IO.Error.alreadyExists : Option String → UInt32 → String → IO.Error
IO.Error.otherError : UInt32 → String → IO.Error
IO.Error.resourceBusy : UInt32 → String → IO.Error
IO.Error.resourceVanished : UInt32 → String → IO.Error
IO.Error.unsupportedOperation : UInt32 → String → IO.Error
IO.Error.hardwareFault : UInt32 → String → IO.Error
IO.Error.unsatisfiedConstraints : UInt32 → String → IO.Error
IO.Error.illegalOperation : UInt32 → String → IO.Error
IO.Error.protocolError : UInt32 → String → IO.Error
IO.Error.timeExpired : UInt32 → String → IO.Error
IO.Error.interrupted : String → UInt32 → String → IO.Error
IO.Error.noFileOrDirectory : String → UInt32 → String → IO.Error
IO.Error.invalidArgument : Option String → UInt32 → String → IO.Error
IO.Error.permissionDenied : Option String → UInt32 → String → IO.Error
IO.Error.resourceExhausted : Option String → UInt32 → String → IO.Error
IO.Error.inappropriateType : Option String → UInt32 → String → IO.Error
IO.Error.noSuchThing : Option String → UInt32 → String → IO.Error
IO.Error.unexpectedEof : IO.Error
IO.Error.userError : String → IO.Error

EIO ε α는 ε 타입의 오류로 종료되거나 α 타입의 값으로 성공하는 IO 동작을 나타낸다. 따라서 Except ε 모나드처럼 IO 모나드에도 오류 처리와 예외를 정의하는 기능이 포함된다.

한 층을 더 벗겨 보면 EIO 자체도 더 단순한 구조를 사용해 정의되어 있다.

def EIO : Type → Type → Type :=
fun ε α => EST ε IO.RealWorld α

EST 모나드는 오류와 상태를 모두 포함하며, Except와 State를 결합한 것과 비슷하다. 이는 또 다른 타입인 EST.Out을 사용해 정의된다.

def EST : Type → Type → Type → Type :=
fun ε σ α => Void σ → EST.Out ε σ α

즉 EST ε σ α 타입의 프로그램은 σ 타입의 초기 상태를 받아 EST.Out ε σ α를 반환하는 함수다. 상태는 Void 타입으로 감싸는데, 이는 컴파일된 코드에서 값이 지워지게 하는 내부 기본 타입이다. Void σ는 Unit과 같은 표현을 가진다.

EST.Out은 Except의 정의와 매우 비슷하다. 성공적인 종료를 나타내는 생성자 하나와 오류를 나타내는 생성자 하나가 있다.

inductive EST.Out : Type → Type → Type → Type
number of parameters: 3
constructors:
EST.Out.ok : {ε σ α : Type} → α → Void σ → EST.Out ε σ α
EST.Out.error : {ε σ α : Type} → ε → Void σ → EST.Out ε σ α

Except ε α와 마찬가지로 ok 생성자는 α 타입의 결과를 포함하고, error 생성자는 ε 타입의 예외를 포함한다. Except와 달리 두 생성자 모두 계산의 최종 상태를 담는 추가 상태 필드를 가진다.

EST ε σ에 대한 Monad 인스턴스는 pure와 bind를 요구한다. State와 마찬가지로 EST의 pure 구현은 초기 상태를 받아 변경하지 않고 반환한다. 또한 Except와 마찬가지로 인수를 ok 생성자 안에 넣어 반환한다.

protected def EST.pure : {α ε σ : Type} → α → EST ε σ α :=
fun {α ε σ} a s => EST.Out.ok a s

protected는 EST 네임스페이스를 열었더라도 전체 이름인 EST.pure가 필요하다는 뜻이다.

마찬가지로 EST의 bind는 초기 상태를 인수로 받는다. 이 초기 상태를 첫 동작에 전달한다. 그런 다음 Except의 bind와 마찬가지로 결과가 오류인지 검사한다. 오류라면 오류를 변경하지 않고 반환하며 bind의 두 번째 인수는 사용하지 않는다. 결과가 성공이면 두 번째 인수를 반환된 값과 결과 상태 모두에 적용한다.

protected def EST.bind : {ε σ α β : Type} → EST ε σ α → (α → EST ε σ β) → EST ε σ β :=
fun {ε σ α β} x f s =>
  match x s with
  | EST.Out.ok a s => f a s
  | EST.Out.error e s => EST.Out.error e s

이 모든 것을 종합하면 IO는 상태와 오류를 동시에 추적하는 모나드다. 가능한 오류의 집합은 IO.Error 데이터 타입으로 주어지며, 이 타입의 생성자들은 프로그램에서 발생할 수 있는 여러 문제를 설명한다. 상태는 현실 세계를 나타내는 타입인 IO.RealWorld다. 각 기본 IO 동작은 이 현실 세계를 받아 오류 또는 결과와 짝지은 다른 현실 세계를 반환한다. IO에서 pure는 세계를 변경하지 않고 반환하며, bind는 변경된 세계를 한 동작에서 다음 동작으로 전달한다.

우주 전체를 컴퓨터 메모리에 담을 수 없으므로 전달되는 세계는 단지 표현일 뿐이다. 세계 토큰을 재사용하지 않는 한 이 표현은 안전하다. IO.RealWorld 타입은 Void 내부에서만 사용되므로 어떤 표현도 필요 없는 단순한 기본 타입이다.