Lean으로 배우는 함수형 프로그래밍

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를 감싸는 래퍼입니다. 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. 사용자 정의 모나드 사용하기🔗

이 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는 표준 라이브러리에 있는 일반적인 Lean IO 액션을 호출하는데, 이러한 액션에는 당연히 Config가 필요하지 않습니다. 일반적인 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

이 사용자 정의 모나드는 설정을 수동으로 전달하는 방식에 비해 여러 가지 장점이 있습니다:

  1. 변경을 원하는 경우를 제외하면 설정이 바뀌지 않고 그대로 전달되도록 보장하기가 더 쉽습니다

  2. 설정을 다음으로 넘겨주는 관심사가 디렉터리 내용을 출력하는 관심사와 더 명확하게 분리됩니다

  3. 프로그램이 커질수록 설정을 전달하는 것 외에는 설정에 대해 아무 일도 하지 않는 중간 계층이 점점 더 많아지며, 이러한 계층은 설정 로직이 바뀌더라도 다시 작성할 필요가 없습니다

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

  1. 프로그램이 발전하면서 모나드에 더 많은 기능이 필요해지면, locally나 currentConfig 같은 기본 연산자를 하나하나 수정해야 합니다

  2. 일반적인 IO 액션을 runIO로 감싸는 것은 코드를 번잡하게 만들고 프로그램의 흐름에서 주의를 흩뜨립니다

  3. 모나드 인스턴스를 직접 작성하는 일은 반복적이며, 다른 모나드에 리더 효과를 추가하는 기법은 문서화와 의사소통 비용을 수반하는 디자인 패턴입니다

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

  1. 트랜스포머 자체의 정의(일반적으로 타입에서 타입으로 가는 함수)

  2. 내부 타입이 이미 모나드라고 가정하는 Monad 인스턴스

  3. 내부 모나드의 액션을 변환된 모나드로 “끌어올리는(lift)” 연산자(runIO와 비슷함)

6.1.3. 임의의 모나드에 리더 추가하기🔗

ConfigIO에서는 IO α를 함수 타입으로 감싸서 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 α

ReaderT에는 표준 라이브러리에 정의된 유용한 기능이 많은데, 축약할 수 없는(non-reducible) 정의를 사용하면 이 기능들이 가려지므로 abbrev로 정의합니다. 이 기능들이 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로 “리프팅”하는 데 사용되지만, 이 인스턴스는 어떤 내부 모나드 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되어 있으므로, 그 앞에 타입 클래스 이름을 붙여 쓸 필요가 없습니다:

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을 수정하십시오.