IOとReaderを組み合わせる

リーダモナドが有用なケースの1つに、深い再帰呼び出しを通して渡されるアプリケーションの「現在の設定値」の概念があります。このようなプログラムの例は tree で、これはカレントディレクトリとサブディレクトリにあるファイルを再帰的に表示し、その木構造を文字で示します。この章で登場する tree は、北米の西海岸を彩る強大な米松（Douglas Fir）にちなんで doug と呼ぶことにし、ディレクトリ構造を示すときにUnicodeの罫線素片、もしくはそれに相当するASCII文字のどちらかを選べるオプションを提供します。

例として、以下のコマンドは doug-demo というディレクトリにディレクトリ構造といくつかの空のファイルを作成しています：

$ cd doug-demo
$ mkdir -p a/b/c
$ mkdir -p a/d
$ mkdir -p a/e/f
$ touch a/b/hello
$ touch a/d/another-file
$ touch a/e/still-another-file-again

ここで doug を実行すると以下の結果となります：

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

実装

内部的には、doug はディレクトリ構造を再帰的に走査しながら設定値を下方に渡しています。この設定は2つのフィールドを含みます：useASCII はUnicodeの罫線素片とASCIIの縦棒とダッシュ文字のどちらを構造の表示に用いるかを決定し、currentPrefix は出力の各行の先頭につける文字列を保持します。カレントディレクトリが深くなるにつれて、そのディレクトリを接頭辞文字列に蓄積していきます。この設定値は以下の構造体です：

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

この構造体は両方のフィールドにデフォルト定義を持ちます。デフォルトの Config はUnicodeによる表示を行い、接頭辞を付けません。

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 はコマンドライン引数を処理しなければなりません。またこの関数はOSに適切な終了コードを返さなければなりません：

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

すべてのパスがディレクトリツリーに表示されるべきではありません。特に、. や .. という名前のファイルはスキップされるべきです。これらはファイル そのもの というより実際にはナビゲーションのための機能であるからです。

表示すべきファイルは2種類です：通常のファイルとディレクトリです：

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.toList fun d =>
      dirTree newConfig d.path

toEntry の呼び出しは 入れ子になったアクション です。match のように矢印が他の意味を持ちえない位置では括弧を省略することができます。ファイル名がツリーの要素に対応していない場合（例えば .. の場合）、dirTree は何もしません。ファイル名が通常のファイルを指している場合、dirTree は補助関数を呼び出して現在の設定値をもとにファイルを表示します。ファイル名がディレクトリを指している場合、補助関数を呼び出してディレクトリ名を表示し、その中身についてはディレクトリに入ったことを考慮して接頭辞を拡張した新しい設定のもとで再帰的に表示を行います。

ファイルとディレクトリの名前を表示するには、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かUnicodeの設定を考慮する 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

カスタムのモナドを使う

この実装で doug は動作してくれますが、手動で設定値を渡すのは冗長でエラーになりやすいです。例えば、間違った設定値が 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 記法を使用する点です。results によって発生する任意の IO の作用は next が呼び出される前に発生しなければなりませんが、これは IO モナドの bind 演算子によって保証されています。Config IO は宇宙多相ではありませんが、これはベースにした IO 型も宇宙多相ではないからです。

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 を必要としない標準ライブラリから普通の 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 と System.FilePath.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.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. 手動でモナドのインスタンスを書くのは同じことの繰り返しであり、リーダの作用を別のモナドに追加するテクニックは余分な文書化とコミュニケーションを要するデザインパターンである

モナド変換子 （monad transformer）と呼ばれるテクニックを使えば、これらすべての欠点を解決することができます。モナド変換子はモナドを引数に取り、新しいモナドを返します。モナド変換子の構成は以下の通りです：

1. このモナド変換子自体の定義、これは通常型から型への関数
2. 内部の型がすでにモナドであると仮定した Monad インスタンス
3. 内側のモナドから変換後のモナドにアクションを「持ち上げる」演算子、これは runIO に似ている

リーダを任意のモナドに付与する

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 α

ここでは 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 へ変換します。このプロセスは埋め込まれたモナドのアクションをその外側のモナドのアクションに変換することから「持ち上げ（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 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.toList fun d =>
          dirTree d.path)

locally を withReader に置き換えた以外は、以前のものと同じです。

カスタムの ConfigIO 型を ReaderT 型に置き換えても、この節のコード量はそこまで大幅には減りませんでした。しかし、標準ライブラリのコンポーネントを使用してコードを書き直すことには長期的な利点があります。まず ReaderT について知っている読者は ConfigIO の Monad インスタンスをモナドそのものの意味から逆算してじっくり時間をかけて理解する必要がありません。そのため ConfigIO への理解が容易になります。次に、モナドにさらなる作用（各ディレクトリ内のファイルをカウントして最後にカウントを表示する状態の作用など）を追加する場合、ライブラリで提供されているモナド変換子と MonadLift インスタンスがうまく連携して動くため、コードの変更量がはるかに少なくなります。最後に、標準ライブラリにある型クラスたちを使うことで、モナド変換子の適用順などの細かいことを気にすることなく、様々なモナドで動作するように多相なコードを書くことができます。一部の関数がどのモナドでも動作するように、関数がある種の状態や例外などの任意のモナドに対して、それらの具体的なモナドが状態や例外を提供する 方法 を具体的に記述することなく動作することができます。

演習問題

ドットのファイルの表示の制御

ファイル名がドット文字（'.'）で始まるファイルは通常、ソース管理のメタデータや設定ファイルなど、通常は隠すべきファイルを表します。doug にドットで始まるファイル名を表示または非表示にするオプションを追加してください。このオプションは -a コマンドラインオプションで制御します。

開始するディレクトリを引数に

doug を修正してコマンドライン引数に追加で開始ディレクトリを受け取るようにしてください。