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 내부에서만 사용되기 때문입니다.