6.1. IO와 Reader 결합하기🔗

리더 모나드가 유용하게 쓰이는 한 가지 경우는 애플리케이션의 "현재 구성"이라는 개념이 있어 이것이 많은 재귀 호출을 거쳐 전달되는 경우입니다. 이러한 프로그램의 한 예로 tree가 있는데, 이는 현재 디렉터리와 그 하위 디렉터리에 있는 파일을 재귀적으로 출력하며 문자를 사용해 트리 구조를 나타냅니다. 이 장에서 다루는 tree의 버전은 북미 서해안을 장식하는 웅장한 더글러스 전나무(Douglas Fir)를 기려 doug라 불리며, 디렉터리 구조를 표시할 때 유니코드 박스 그리기 문자나 이에 대응하는 ASCII 문자를 선택할 수 있는 옵션을 제공합니다.

예를 들어, 다음 명령은 doug-demo라는 디렉터리에 디렉터리 구조와 몇 개의 빈 파일을 생성합니다:

cd doug-demomkdir -p a/b/cmkdir -p a/dmkdir -p a/e/ftouch a/b/hellotouch a/d/another-filetouch a/e/still-another-file-again

doug를 실행하면 다음과 같은 결과가 나타납니다.

doug

├── doug-demo/
│   ├── a/
│   │   ├── b/
│   │   │   ├── c/
│   │   │   ├── hello
│   │   ├── d/
│   │   │   ├── another-file
│   │   ├── e/
│   │   │   ├── f/
│   │   │   ├── still-another-file-again

6.1.1. 구현🔗

내부적으로 doug는 디렉터리 구조를 재귀적으로 순회하면서 설정 값을 아래로 전달합니다. 이 설정에는 두 개의 필드가 있습니다: useASCII는 구조를 나타내기 위해 유니코드 상자 그리기 문자를 사용할지 ASCII 수직선과 대시 문자를 사용할지를 결정하며, currentPrefix는 출력의 각 줄 앞에 붙일 문자열을 담고 있습니다. 현재 디렉터리가 깊어질수록, 접두사 문자열에는 디렉터리 안에 있음을 나타내는 표시가 누적됩니다. 설정은 구조체입니다:

structure Config where
  useASCII : Bool := false
  currentPrefix : String := ""

이 구조체에는 두 필드 모두에 대한 기본 정의가 있습니다. 기본 Config는 접두사 없이 유니코드 표시를 사용합니다.

doug를 호출하는 사용자는 명령줄 인자를 제공할 수 있어야 합니다. 사용법 정보는 다음과 같습니다:

def usage : String :=
  "Usage: doug [--ascii]
Options:
\t--ascii\tUse ASCII characters to display the directory structure"

따라서 명령줄 인수 목록을 검사하여 설정을 구성할 수 있습니다:

def configFromArgs : List String → Option Config
  | [] => some {} -- both fields default
  | ["--ascii"] => some {useASCII := true}
  | _ => none

main 함수는 설정을 사용하여 디렉터리의 내용을 보여 주는 dirTree라는 내부 워커를 감싸는 래퍼입니다. dirTree를 호출하기 전, main은 명령줄 인자를 처리할 책임이 있습니다. 또한 운영 체제에 적절한 종료 코드를 반환해야 합니다:

def main (args : List String) : IO UInt32 := do
  match configFromArgs args with
  | some config =>
    dirTree config (← IO.currentDir)
    pure 0
  | none =>
    IO.eprintln s!"Didn't understand argument(s) {" ".separate args}\n"
    IO.eprintln usage
    pure 1

IO.eprintln은 표준 오류로 출력하는 IO.println의 버전입니다.

모든 경로가 디렉터리 트리에 표시되어야 하는 것은 아닙니다. 특히, . 또는 ..라는 이름의 파일은 건너뛰어야 합니다. 이들은 사실상 파일 자체라기보다는 탐색에 사용되는 기능이기 때문입니다. 표시되어야 하는 파일 중에는 일반 파일과 디렉터리라는 두 종류가 있습니다:

inductive Entry where
  | file : String → Entry
  | dir : String → Entry

파일을 표시해야 하는지 여부와 어떤 종류의 항목인지를 결정하기 위해, doug는 toEntry를 사용합니다:

def toEntry (path : System.FilePath) : IO (Option Entry) := do
  match path.components.getLast? with
  | none => pure (some (.dir ""))
  | some "." | some ".." => pure none
  | some name =>
    pure (some (if (← path.isDir) then .dir name else .file name))

System.FilePath.components는 경로를 경로 구성 요소들의 목록으로 변환하며, 디렉터리 구분자를 기준으로 이름을 분할합니다. 마지막 구성 요소가 없으면 해당 경로는 루트 디렉터리입니다. 마지막 구성 요소가 특수 탐색 파일(. 또는 ..)인 경우, 해당 파일은 제외해야 합니다. 그렇지 않으면 디렉터리와 파일은 해당 생성자로 감싸집니다.

Lean의 논리에는 디렉터리 트리가 유한하다는 것을 알 수 있는 방법이 없습니다. 실제로 일부 시스템에서는 순환 디렉터리 구조의 생성을 허용합니다. 따라서 dirTree는 partial로 선언됩니다:

partial def dirTree (cfg : Config) (path : System.FilePath) : IO Unit := do
  match ← toEntry path with
  | none => pure ()
  | some (.file name) => showFileName cfg name
  | some (.dir name) =>
    showDirName cfg name
    let contents ← path.readDir
    let newConfig := cfg.inDirectory
    doList (contents.qsort dirLT).toList fun d =>
      dirTree newConfig d.path

toEntry 호출은 중첩 액션으로, match처럼 화살표가 다른 의미를 가질 수 없는 위치에서는 괄호가 선택적입니다. 파일 이름이 트리 항목에 대응하지 않는 경우(예를 들어 ..이기 때문인 경우), dirTree는 아무 일도 하지 않습니다. 파일 이름이 일반 파일을 가리키는 경우, dirTree는 현재 설정으로 이를 보여 주기 위해 도우미를 호출합니다. 파일 이름이 디렉터리를 가리키는 경우, 이는 헬퍼와 함께 표시되며, 이후 새로운 디렉터리 안에 있음을 고려하여 접두사가 확장된 새로운 설정에서 그 내용이 재귀적으로 표시됩니다. 디렉터리의 내용은 출력을 결정적으로 만들기 위해 정렬되며, dirLT에 따라 비교됩니다.

def dirLT (e1 : IO.FS.DirEntry) (e2 : IO.FS.DirEntry) : Bool :=
  e1.fileName < e2.fileName

파일과 디렉터리의 이름을 보여주는 것은 showFileName과 showDirName으로 이루어집니다:

def showFileName (cfg : Config) (file : String) : IO Unit := do
  IO.println (cfg.fileName file)

def showDirName (cfg : Config) (dir : String) : IO Unit := do
  IO.println (cfg.dirName dir)

이 두 헬퍼는 모두 ASCII 대 유니코드 설정을 고려하는 Config의 함수들에 위임합니다:

def Config.preFile (cfg : Config) :=
  if cfg.useASCII then "|--" else "├──"

def Config.preDir (cfg : Config) :=
  if cfg.useASCII then "|  " else "│  "

def Config.fileName (cfg : Config) (file : String) : String :=
  s!"{cfg.currentPrefix}{cfg.preFile} {file}"

def Config.dirName (cfg : Config) (dir : String) : String :=
  s!"{cfg.currentPrefix}{cfg.preFile} {dir}/"

마찬가지로, Config.inDirectory는 디렉터리 마커로 접두사를 확장합니다:

def Config.inDirectory (cfg : Config) : Config :=
  {cfg with currentPrefix := cfg.preDir ++ " " ++ cfg.currentPrefix}

디렉터리 내용 목록에 대해 IO 액션을 반복 실행하는 것은 doList를 사용하여 구현합니다. doList는 리스트에 있는 모든 동작을 실행할 뿐 그 동작들이 반환하는 값을 바탕으로 제어 흐름을 결정하지 않기 때문에, Monad가 지닌 완전한 힘까지는 필요하지 않으며, 어떤 Applicative에 대해서도 동작합니다:

def doList [Applicative f] : List α → (α → f Unit) → f Unit
  | [], _ => pure ()
  | x :: xs, action =>
    action x *>
    doList xs action

6.1.2. 사용자 정의 모나드 사용하기🔗

doug의 이 구현은 작동하지만, 설정을 수동으로 전달하는 것은 장황하고 오류가 발생하기 쉽습니다. 예를 들어, 잘못된 설정이 아래로 전달되더라도 타입 시스템은 이를 잡아내지 못합니다. 리더 이펙트는 수동으로 재정의하지 않는 한 모든 재귀 호출에 동일한 설정이 전달되도록 보장하며, 코드를 더 간결하게 만드는 데 도움을 줍니다.

Config의 리더이기도 한 IO의 버전을 만들려면, 평가기 예제의 레시피를 따라 먼저 해당 타입과 그 Monad 인스턴스를 정의합니다:

def ConfigIO (α : Type) : Type :=
  Config → IO α

instance : Monad ConfigIO where
  pure x := fun _ => pure x
  bind result next := fun cfg => do
    let v ← result cfg
    next v cfg

이 Monad 인스턴스와 Reader의 인스턴스 사이의 차이점은, 이 인스턴스가 result에서 반환된 값에 next를 직접 적용하는 대신 bind가 반환하는 함수의 본문에서 IO 모나드의 do-표기법을 사용한다는 것입니다. result가 수행하는 모든 IO 효과는 next가 호출되기 전에 일어나야 하며, 이는 IO 모나드의 bind 연산자에 의해 보장됩니다. 기저 IO 타입 역시 유니버스 다형성을 갖지 않기 때문에, ConfigIO도 유니버스 다형성을 갖지 않습니다.

ConfigIO 액션을 실행하는 것은 구성을 제공하여 이를 IO 액션으로 변환하는 과정을 포함합니다:

def ConfigIO.run (action : ConfigIO α) (cfg : Config) : IO α :=
  action cfg

이 함수는 호출자가 설정을 직접 제공하면 되므로 실제로는 필요하지 않습니다. 그러나 연산에 이름을 붙이면 코드의 어느 부분이 어느 모나드에서 실행되도록 의도되었는지 파악하기가 더 쉬워질 수 있습니다.

다음 단계는 ConfigIO의 일부로서 현재 설정에 접근하는 수단을 정의하는 것입니다:

def currentConfig : ConfigIO Config :=
  fun cfg => pure cfg

이는 평가기 예제에 나오는 read와 마찬가지이지만, 값을 직접 반환하는 대신 IO의 pure를 사용해 반환한다는 점만 다릅니다. 디렉터리에 진입하면 재귀 호출의 범위 동안 현재 구성이 변경되므로, 구성을 재정의할 방법이 필요합니다:

def locally (change : Config → Config) (action : ConfigIO α) : ConfigIO α :=
  fun cfg => action (change cfg)

doug에서 사용되는 코드 대부분은 설정이 필요하지 않으며, doug는 표준 라이브러리에 있는, Config가 전혀 필요하지 않은 평범한 Lean IO 액션들을 호출합니다. 일반적인 IO 액션은 설정 인자를 무시하는 runIO를 사용하여 실행할 수 있습니다:

def runIO (action : IO α) : ConfigIO α :=
  fun _ => action

이러한 구성 요소들을 사용하면, showFileName과 showDirName이 ConfigIO 모나드를 통해 암묵적으로 설정 인자를 받도록 갱신할 수 있습니다. 이 함수들은 설정을 가져오기 위해 중첩된 액션을 사용하고, IO.println 호출을 실제로 실행하기 위해 runIO를 사용합니다:

def showFileName (file : String) : ConfigIO Unit := do
  runIO (IO.println ((← currentConfig).fileName file))

def showDirName (dir : String) : ConfigIO Unit := do
  runIO (IO.println ((← currentConfig).dirName dir))

새로운 버전의 dirTree에서는 toEntry와 readDir 호출이 runIO로 감싸져 있습니다. 또한, 새로운 설정을 만든 다음 재귀 호출에 어떤 것을 전달할지 프로그래머가 계속 추적하도록 요구하는 대신, locally를 사용하여 수정된 설정을 프로그램의 작은 영역으로만 자연스럽게 한정합니다. 이 영역에서는 수정된 설정이 유일한 유효 설정입니다:

partial def dirTree (path : System.FilePath) : ConfigIO Unit := do
  match ← runIO (toEntry path) with
    | none => pure ()
    | some (.file name) => showFileName name
    | some (.dir name) =>
      showDirName name
      let contents ← runIO path.readDir
      locally (·.inDirectory)
        (doList (contents.qsort dirLT).toList fun d =>
          dirTree d.path)

새 버전의 main은 ConfigIO.run을 사용하여 초기 설정으로 dirTree를 호출합니다:

def main (args : List String) : IO UInt32 := do
    match configFromArgs args with
    | some config =>
      (dirTree (← IO.currentDir)).run config
      pure 0
    | none =>
      IO.eprintln s!"Didn't understand argument(s) {" ".separate args}\n"
      IO.eprintln usage
      pure 1

이 커스텀 모나드는 설정을 수동으로 전달하는 것에 비해 여러 가지 장점이 있습니다:

변경이 필요한 경우를 제외하고는 설정이 변경되지 않은 채로 전달되도록 보장하는 것이 더 쉽습니다.
설정을 전달하는 관심사는 디렉터리 내용을 출력하는 관심사와 더 명확하게 분리됩니다
프로그램이 커질수록 설정을 전달하는 것 외에는 아무 작업도 하지 않는 중간 계층이 점점 더 많아지는데, 이러한 계층은 설정 로직이 바뀌더라도 다시 작성할 필요가 없습니다.

하지만 몇 가지 명백한 단점도 있습니다:

프로그램이 발전하고 모나드에 더 많은 기능이 필요해짐에 따라, locally와 currentConfig와 같은 각각의 기본 연산자를 업데이트해야 합니다
일반적인 IO 액션을 runIO로 감싸는 것은 번잡하며 프로그램의 흐름을 방해합니다
모나드 인스턴스를 손으로 작성하는 것은 반복적인 작업이며, 다른 모나드에 리더 효과를 추가하는 기법은 문서화와 의사소통 오버헤드를 필요로 하는 디자인 패턴입니다.

모나드 트랜스포머라는 기법을 사용하면, 이러한 단점을 모두 해결할 수 있습니다. 모나드 트랜스포머는 모나드를 인자로 받아 새로운 모나드를 반환합니다. 모나드 트랜스포머는 다음으로 구성됩니다:

변환기 자체의 정의로, 일반적으로 타입에서 타입으로의 함수입니다
내부 타입이 이미 모나드라고 가정하는 Monad 인스턴스
runIO와 유사하게, 내부 모나드의 액션을 변환된 모나드로 “끌어올리는(lift)” 연산자

6.1.3. 모든 모나드에 Reader 추가하기🔗

IO에 리더 효과를 추가하는 작업은 IO α를 함수 타입으로 감싸는 방식으로 ConfigIO에서 수행되었습니다. Lean 표준 라이브러리에는 이러한 작업을 어떤 다형 타입에도 수행할 수 있는 함수가 있으며, ReaderT라고 불립니다:

def ReaderT (ρ : Type u) (m : Type u → Type v) (α : Type u) :
    Type (max u v) :=
  ρ → m α

그 인자는 다음과 같습니다:

ρ는 리더가 접근할 수 있는 환경입니다
m은 변환되고 있는 모나드로, 예를 들어 IO와 같습니다
α는 모나드 계산에 의해 반환되는 값의 타입입니다. α와 ρ는 모두 같은 유니버스에 속하는데, 이는 모나드에서 환경을 가져오는 연산자가 m ρ 타입을 가지기 때문입니다.

ReaderT를 사용하면, ConfigIO는 다음과 같아집니다:

abbrev ConfigIO (α : Type) : Type := ReaderT Config IO α

이것이 abbrev인 이유는 ReaderT가 표준 라이브러리에 정의된 유용한 기능을 많이 가지고 있는데, 축약 불가능한(non-reducible) 정의는 이를 가려버리기 때문입니다. 이들이 ConfigIO에 대해 직접 작동하도록 만드는 책임을 지기보다는, ConfigIO가 ReaderT Config IO와 동일하게 동작하도록 하는 편이 더 쉽습니다.

수동으로 작성된 currentConfig는 리더에서 환경을 가져왔습니다. 이 효과는 read라는 이름 아래, ReaderT의 모든 사용에 대해 일반적인 형태로 정의할 수 있습니다:

def read [Monad m] : ReaderT ρ m ρ :=
   fun env => pure env

하지만 리더 효과를 제공하는 모든 모나드가 ReaderT로 만들어지는 것은 아닙니다. 타입 클래스 MonadReader는 모든 모나드가 read 연산자를 제공할 수 있도록 합니다:

class MonadReader (ρ : outParam (Type u)) (m : Type u → Type v) :
    Type (max (u + 1) v) where
  read : m ρ

instance [Monad m] : MonadReader ρ (ReaderT ρ m) where
  read := fun env => pure env

export MonadReader (read)

타입 ρ는 출력 매개변수인데, 이는 주어진 모나드가 일반적으로 리더를 통해 단 하나의 환경 타입만을 제공하기 때문이며, 따라서 모나드가 알려졌을 때 이를 자동으로 선택하도록 하면 프로그램을 작성하기가 더 편리해집니다.

ReaderT에 대한 Monad 인스턴스는 본질적으로 ConfigIO에 대한 Monad 인스턴스와 동일하지만, IO가 임의의 모나드 인자 m으로 대체되었다는 점만 다릅니다:

instance [Monad m] : Monad (ReaderT ρ m) where
  pure x := fun _ => pure x
  bind result next := fun env => do
    let v ← result env
    next v env

다음 단계는 runIO의 사용을 제거하는 것입니다. Lean은 모나드 타입이 일치하지 않는 경우를 만나면, 실제 모나드를 예상되는 모나드로 변환하기 위해 MonadLift라는 타입 클래스를 자동으로 사용하려고 시도합니다. 이 과정은 강제 변환의 사용과 유사합니다. MonadLift는 다음과 같이 정의됩니다:

class MonadLift (m : Type u → Type v) (n : Type u → Type w) where
  monadLift : {α : Type u} → m α → n α

monadLift 메서드는 모나드 m에서 모나드 n으로 변환합니다. 이 과정을 “들어올리기(lifting)”라고 부르는 이유는 내장된 모나드의 액션을 받아 이를 감싸는 모나드의 액션으로 만들기 때문입니다. 이 경우, IO에서 ReaderT Config IO로 “끌어올리는(lift)” 데 사용될 것입니다만, 이 인스턴스는 어떤 내부 모나드 m에 대해서도 동작합니다:

instance : MonadLift m (ReaderT ρ m) where
  monadLift action := fun _ => action

monadLift의 구현은 runIO의 구현과 매우 유사합니다. 실제로 runIO를 사용하지 않고 showFileName과 showDirName을 정의하는 것으로 충분합니다.

def showFileName (file : String) : ConfigIO Unit := do
  IO.println s!"{(← read).currentPrefix} {file}"

def showDirName (dir : String) : ConfigIO Unit := do
  IO.println s!"{(← read).currentPrefix} {dir}/"

원래의 ConfigIO에서 ReaderT의 사용으로 번역해야 할 마지막 연산이 하나 남아 있는데, 바로 locally입니다. 이 정의는 ReaderT로 직접 번역될 수 있지만, Lean 표준 라이브러리는 더 일반화된 버전을 제공합니다. 표준 버전은 withReader라고 불리며, MonadWithReader라는 타입 클래스의 일부입니다:

class MonadWithReader (ρ : outParam (Type u)) (m : Type u → Type v) where
  withReader {α : Type u} : (ρ → ρ) → m α → m α

MonadReader에서와 마찬가지로, 환경 ρ는 outParam입니다. withReader 연산은 익스포트되어 있어서, 그 앞에 타입 클래스 이름을 붙여 쓰지 않아도 됩니다:

export MonadWithReader (withReader)

ReaderT에 대한 인스턴스는 locally의 정의와 본질적으로 동일합니다:

instance : MonadWithReader ρ (ReaderT ρ m) where
  withReader change action :=
    fun cfg => action (change cfg)

이러한 정의를 갖추면 dirTree의 새 버전을 다음과 같이 작성할 수 있습니다:

partial def dirTree (path : System.FilePath) : ConfigIO Unit := do
  match ← toEntry path with
    | none => pure ()
    | some (.file name) => showFileName name
    | some (.dir name) =>
      showDirName name
      let contents ← path.readDir
      withReader (·.inDirectory)
        (doList (contents.qsort dirLT).toList fun d =>
          dirTree d.path)

locally를 withReader로 바꾼 것을 제외하면 이전과 동일합니다.

사용자 정의 ConfigIO 타입을 ReaderT로 대체해도 이 절에서는 코드 줄 수를 크게 줄이지 못했습니다. 하지만 표준 라이브러리의 구성 요소를 사용해 코드를 다시 작성하면 장기적인 이점이 있습니다. 먼저, ReaderT에 대해 아는 독자는 ConfigIO에 대한 Monad 인스턴스를 이해하기 위해 모나드 자체의 의미로 거슬러 올라가는 시간을 들일 필요가 없습니다. 대신, 자신의 초기 이해를 확신할 수 있습니다. 다음으로, 모나드에 추가 효과(예를 들어 각 디렉터리의 파일 수를 세어 마지막에 그 개수를 출력하는 상태 효과)를 더하는 작업은 코드 변경을 훨씬 적게 요구하는데, 이는 라이브러리에서 제공하는 모나드 트랜스포머와 MonadLift 인스턴스들이 서로 잘 어우러져 작동하기 때문입니다. 마지막으로, 표준 라이브러리에 포함된 타입 클래스 집합을 사용하면, 모나드 트랜스포머가 적용된 순서와 같은 세부 사항을 신경 쓸 필요 없이 다양한 모나드와 함께 작동할 수 있도록 다형적 코드를 작성할 수 있습니다. 일부 함수가 어떤 모나드에서든 작동하는 것과 마찬가지로, 다른 함수들은 특정 구체적인 모나드가 상태나 예외를 제공하는 방식을 구체적으로 설명하지 않고도, 특정 종류의 상태나 특정 종류의 예외를 제공하는 어떤 모나드에서든 작동할 수 있습니다.

6.1.4. 연습문제🔗

6.1.4.1. 도트파일 표시 제어하기🔗

이름이 점 문자('.')로 시작하는 파일은 일반적으로 소스 제어 메타데이터나 설정 파일처럼 보통 숨겨져야 하는 파일을 나타냅니다. 점(.)으로 시작하는 파일 이름을 표시하거나 숨기는 옵션을 추가하여 doug를 수정하십시오. 이 옵션은 -a 명령줄 옵션으로 제어되어야 합니다.

6.1.4.2. 시작 디렉터리를 인자로 전달하기🔗

doug를 수정하여 시작 디렉터리를 추가 명령줄 인자로 받도록 하십시오.