6.1. Combining IO and Reader🔗

리더 모나드가 유용한 경우 중 하나는 애플리케이션의 “현재 설정”이라는 개념을 여러 재귀 호출을 거쳐 전달해야 할 때다. 그런 프로그램의 예로 tree가 있다. 이 프로그램은 현재 디렉터리와 그 하위 디렉터리의 파일을 재귀적으로 출력하고 문자로 트리 구조를 나타낸다. 이 장의 tree 버전은 북아메리카 서부를 장식하는 웅장한 더글러스 전나무에서 이름을 따 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. Implementation🔗

내부적으로 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 {} -- 두 필드 모두 기본값
  | ["--ascii"] => some {useASCII := true}
  | _ => none

main 함수는 설정을 사용해 디렉터리 내용을 표시하는 내부 작업 함수 dirTree를 감싸는 래퍼다. main은 dirTree를 호출하기 전에 명령줄 인수를 처리해야 한다. 또한 운영 체제에 적절한 종료 코드를 반환해야 한다:

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. Using a Custom Monad🔗

이 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의 인스턴스와 다른 점은 do 표기를 IO 모나드에서 사용해 bind가 반환하는 함수의 본문으로 삼고, next를 result가 반환한 값에 직접 적용하지 않는다는 것이다. 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는 표준 라이브러리의 일반 Lean IO 동작을 호출하므로 Config가 필요하지 않다. 일반 IO 동작은 설정 인수를 무시하는 runIO를 사용해 실행할 수 있다:

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

이 구성 요소를 사용하면 showFileName과 showDirName이 ConfigIO 모나드를 통해 설정 인수를 암시적으로 받도록 고칠 수 있다. 이 함수들은 중첩 동작으로 설정을 가져오고, runIO를 사용해 실제로 IO.println 호출을 실행한다:

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와 비슷하게 내부 모나드의 동작을 변환된 모나드로 “끌어 올리는” 연산자

6.1.3. Adding a Reader to Any Monad🔗

IO에 리더 효과를 추가하는 일은 ConfigIO에서 IO α를 함수 타입으로 감싸 수행했다. 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에는 표준 라이브러리에 정의된 유용한 기능이 많으며, 환원 불가능한 정의를 사용하면 그 기능이 가려지기 때문이다. 이 기능이 ConfigIO에서 직접 작동하게 만들 책임을 지는 대신 ConfigIO가 ReaderT Config IO와 동일하게 동작하게 하는 편이 쉽다.

직접 작성한 currentConfig는 리더에서 환경을 가져왔다. 이 효과는 모든 ReaderT 사용에 대해 read라는 이름의 일반적인 형태로 정의할 수 있다:

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 모나드로 변환한다. 내부 모나드의 동작을 감싸는 모나드의 동작으로 만드는 과정이라서 이를 “끌어 올리기”라고 한다. 이 경우에는 IO에서 ReaderT Config IO로 “끌어 올리는” 데 사용하지만, 이 인스턴스는 어떤 내부 모나드 m에도 작동한다:

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

monadLift의 구현은 runIO의 구현과 매우 비슷하다. 실제로 showFileName과 showDirName을 runIO 없이 정의하는 것만으로 충분하다:

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. Exercises🔗

6.1.4.1. Controlling the Display of Dotfiles🔗

이름이 점 문자('.')로 시작하는 파일은 보통 소스 제어 메타데이터나 설정 파일처럼 숨겨야 하는 파일을 나타낸다. 점으로 시작하는 파일 이름을 표시하거나 숨기는 옵션을 doug에 추가하라. 이 옵션은 -a 명령줄 옵션으로 제어하라.

6.1.4.2. Starting Directory as Argument🔗

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