4.5. IO 모나드🔗

모나드로서의 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 내부에서만 사용되므로 표현이 전혀 필요 없는 자명한 원시 타입입니다.