完全な定義

ようやく関連する言語機能をすべて紹介したので、本節ではLeanの標準ライブラリにある Functor と Applicative 、Monad の正真正銘完全な定義について説明します。理解促進のために細部に至るまで省略しません。

関手

Functor クラスの完全な定義では、宇宙多相とデフォルトメソッドの実装が用いられています：

class Functor (f : Type u → Type v) : Type (max (u+1) v) where
  map : {α β : Type u} → (α → β) → f α → f β
  mapConst : {α β : Type u} → α → f β → f α :=
    Function.comp map (Function.const _)

この定義において、Function.comp は関数合成のことで、よく ∘ という演算子として記述されます。Function.const は 定数関数 （constant function）で、引数を2つ取り、2つ目を無視する関数です。この関数に1つだけ引数を適用することで常に同じ値を返す関数が出来上がります。これは関数を要求するAPIに対して、プログラムとしては引数ごとに異なる計算結果を返す必要がない場合に有用です。Function.const の定義を簡潔にすると以下のようになります：

def simpleConst  (x : α) (_ : β) : α := x

この関数に1つ引数を適用した上で List.map の関数の引数として使うとその便利さがよくわかるでしょう：

#eval [1, 2, 3].map (simpleConst "same")

["same", "same", "same"]

この関数は実際には以下のシグネチャを持ちます：

Function.const.{u, v} {α : Sort u} (β : Sort v) (a : α) (a✝ : β) : α

ここでは型引数 β は明示的な引数であるため、Functor.mapConst のデフォルトの定義ではこの引数に _ を与えることでプログラムの型チェックが通るような Function.const に渡される一意な型を見つけるようにLeanに指示します。(Function.comp map (Function.const _) : α → f β → f α) は fun (x : α) (y : f β) => map (fun _ => x) y と等価です。

Functor クラスは u+1 と v のうち大きい方の宇宙に存在します。ここで、 u は f の引数として受け入れられる宇宙レベルで、v は f が返す宇宙です。Functor 型クラスを実装する構造体が何故 u よりも大きな宇宙に存在しなければならないかということを説明するために、まず簡略化したクラス定義から始めます：

class Functor (f : Type u → Type v) : Type (max (u+1) v) where
  map : {α β : Type u} → (α → β) → f α → f β

この型クラスの構造体型は以下の帰納型と等価です：

inductive Functor (f : Type u → Type v) : Type (max (u+1) v) where
  | mk : ({α β : Type u} → (α → β) → f α → f β) → Functor f

Functor.mk の引数として渡される map メソッドの実装には Type u 上の2つの型を引数に取る関数を含みます。これは関数自体の型が Type (u+1) 上にあることを意味するため、Functor も少なくとも u+1 のレベルでなければなりません。同様に、関数の他の引数は f を適用して作られた型を持つことから、Functor も少なくとも v のレベルでなければなりません。本節のすべての型クラスはこの性質を共有しています。

アプリカティブ関手

Applicative 型クラスは実際にはいくつかの小さなクラスから構成されており、それぞれに関連するメソッドが含まれています。最初は Pure と Seq で、それぞれ pure と seq を含んでいます：

class Pure (f : Type u → Type v) : Type (max (u+1) v) where
  pure {α : Type u} : α → f α

class Seq (f : Type u → Type v) : Type (max (u+1) v) where
  seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β

これらに加えて、Applicative は　SeqRight とこれに似た SeqLeft クラスにも依存しています：

class SeqRight (f : Type u → Type v) : Type (max (u+1) v) where
  seqRight : {α β : Type u} → f α → (Unit → f β) → f β

class SeqLeft (f : Type u → Type v) : Type (max (u+1) v) where
  seqLeft : {α β : Type u} → f α → (Unit → f β) → f α

オルタナティブとバリデーションについての節で紹介した seqRight 関数は作用の観点から理解するのが最も簡単です。E1 *> E2 は脱糖すると SeqRight.seqRight E1 (fun () => E2) となります。これは最初に E1 、次に E2 を実行し、E2 の結果のみを返却するものとして理解できます。E1 から発生する作用によって E2 が実行されなかったり、複数回実行されることがあり得ます。実際、f が Monad インスタンスを持つ場合、E1 *> E2 は do let _ ← E1; E2 と等価ですが、seqRight は　Validate のようなモナドではない型でも使用できます。

これのいとこである seqLeft は一番左の式の値を返すという点を除けば非常に似ています。E1 <* E2 は SeqLeft.seqLeft E1 (fun () => E2) に脱糖されます。SeqLeft.seqLeft は f α → (Unit → f β) → f α 型を持ち、これが f α を返すことを除けば seqRight とそっくりです。E1 <* E2 は最初に E1 を、次に E2 を実行し、最初の E1 の結果を返すプログラムだと理解できます。もし f が Monad インスタンスを持つ場合、E1 <* E2 は do let x ← E1; _ ← E2; pure x と等価です。一般的に、seqLeft はバリデーションやパーサのような処理にて、値そのものを変化させずに値に対する追加の条件を指定するのに便利です。

Applicative の定義は Functor に加えてこれらすべてのクラスを継承しています：

class Applicative (f : Type u → Type v) extends Functor f, Pure f, Seq f, SeqLeft f, SeqRight f where
  map      := fun x y => Seq.seq (pure x) fun _ => y
  seqLeft  := fun a b => Seq.seq (Functor.map (Function.const _) a) b
  seqRight := fun a b => Seq.seq (Functor.map (Function.const _ id) a) b

Applicative の完全な定義には pure と seq の定義だけが必要です。というのも Functor ・SeqLeft ・SeqRight のすべてのメソッドにデフォルトの定義があるからです。Functor の mapConst メソッドには Functor.map によるデフォルトの実装があります。これらのデフォルト実装をオーバーライドして良いのは、挙動が同じなのにより効率的な新しい関数がある場合のみとすべきです。デフォルト実装はその実装について、自動生成コードと同じ正しさを持つことへの仕様とみなすべきでしょう。

seqLeft のデフォルト実装はとてもコンパクトです。いくつかの名前を糖衣構文や定義に置き換えると、別の視点が見えてきます。以下のデフォルト実装：

fun a b => Seq.seq (Functor.map (Function.const _) a) b

は以下になります：

fun a b => Seq.seq ((fun x _ => x) <$> a) b

(fun x _ => x) <$> a はどう解釈したらよいでしょうか？ここで、a は f α 型で、f は関手です。もし f が List の場合、(fun x _ => x) <$> [1, 2, 3] は [fun _ => 1, fun _ => 2, fun _ => 3] に評価されます。もし f が Option の場合、(fun x _ => x) <$> some "hello" は some (fun _ => "hello") に評価されます。どちらの場合も、関手の中の値は引数を無視してもとの値を返す関数に置き換えられます。これを seq と組み合わせると、この関数は seq の第2引数を破棄します。

seqRight のデフォルト実装は、const に追加の引数 id があることを除けば seqLeft に非常によく似ています。この定義も、最初に標準的な糖衣構文を導入し、次にいくつかの名前をその定義に置き換えることで同じように理解できます：

fun a b => Seq.seq (Functor.map (Function.const _ id) a) b
===>
fun a b => Seq.seq ((fun _ => id) <$> a) b
===>
fun a b => Seq.seq ((fun _ => fun x => x) <$> a) b
===>
fun a b => Seq.seq ((fun _ x => x) <$> a) b

(fun _ x => x) <$> a はどう解釈したらよいでしょうか？ここでも例が役に立ちます。(fun _ x => x) <$> [1, 2, 3] は [fun x => x, fun x => x, fun x => x] に評価され、(fun _ x => x) <$> some "hello" は some (fun x => x) に評価されます。言い換えると、(fun _ x => x) <$> a は a の全体的な形を保ちつつ、しかし各値を恒等関数に置き換えます。作用の観点からは、a の副作用は発生しますが、seq と一緒に使われることで、値が捨てられます。

モナド

Applicative を構成する操作がそれぞれの型クラスに分かれているように、Bind も独自のクラスを持ちます：

class Bind (m : Type u → Type v) where
  bind : {α β : Type u} → m α → (α → m β) → m β

Monad は Bind と共に Applicative を継承しています：

class Monad (m : Type u → Type v) extends Applicative m, Bind m : Type (max (u+1) v) where
  map      f x := bind x (Function.comp pure f)
  seq      f x := bind f fun y => Functor.map y (x ())
  seqLeft  x y := bind x fun a => bind (y ()) (fun _ => pure a)
  seqRight x y := bind x fun _ => y ()

クラスの階層全体から継承したメソッドとデフォルトのメソッドを走査すると、Monad インスタンスに必要な実装は bind と pure だけであることがわかります。つまり、Monad インスタンスは自動的に seq ・seqLeft ・seqRight ・map ・mapConst の実装を生成します。APIの教会から見ると、Monad インスタンスを持つ型は Bind ・Pure ・Seq ・Functor ・SeqLeft ・SeqRight のインスタンスを持つことになります。

演習問題

Option や Except などを例にして、Monad の map ・seq ・seqLeft ・seqRight のデフォルト実装を解釈してください。つまり、 bind と pure の定義をデフォルトの定義に置き換えて、map ・seq ・seqLeft ・seqRight を手で書けるように単純化してください。
map と seq のデフォルト実装が Functor と Applicative の約定を満たすことを手書き、もしくはテキストファイルで証明してください。この際には、通常の式の評価と同様に Monad の約定のルールを使用しても構いません。

Functional Programming in Lean 日本語訳

完全な定義

関手

アプリカティブ関手

モナド

演習問題