アプリカティブ関手

アプリカティブ関手 （applicative functor）とは関手に pure と seq の2つの追加の操作を持ったもののことです。pure は Monad でも同じ演算子が用いられています。それもそのはずで、実は Monad は Applicative を継承しているからです。seq は map とよく似た演算子です：これによって、ある関数をデータ型の中身を変換するために使用することができます。しかし、seq では、関数自体がデータ型に含まれています：f (α → β) → (Unit → f α) → f β 。Functor.map が無条件に関数適用するのに対して、関数を f 型の下に持つことで、Applicative インスタンスは関数の適用方法を制御することができます。2番目の引数には Unit → で始まる型を指定することで、関数が適用されない場合に seq の定義をショートカットできるようにしています。

この短絡的なふるまいの真価は、Applicative Option のインスタンスで見ることができます：

instance : Applicative Option where
  pure x := .some x
  seq f x :=
    match f with
    | none => none
    | some g => g <$> x ()

このケースにおいて、seq に適用する関数が無ければ、引数を計算する必要もないので x が呼ばれることはありません。同じことが Except の Applicative インスタンスにも当てはまります：

instance : Applicative (Except ε) where
  pure x := .ok x
  seq f x :=
    match f with
    | .error e => .error e
    | .ok g => g <$> x ()

この短絡的な挙動は関数自体というよりも、関数を 取り囲む Option や Except の構造にのみ依存します。

モナドは文を順次実行するという概念を純粋関数型言語に取り込むための方法とみなすことができます。ある文の結果はそれ以降の文の実行に影響を及ぼすことができます。これは bind の型：m α → (α → m β) → m β に見ることができます。最初の文の結果の値は、次に実行する文を計算する関数への入力となります。bind の連続した使用は命令型プログラミング言語における文の列のようなものです。bind は強力であり、条件分岐やループのような制御構造を実装することも十分可能です。

このアナロジーに従うと、Applicative は副作用を持つ言語での関数適用を捉えたものと言えます。KotlinやC#のような言語では、関数の引数は左から右に評価されます。先に評価された引数によって実行される副作用は、その後の引数によって実行される副作用よりも先に発生します。しかし、関数は引数の特定の値に依存するカスタムの短絡演算子を実装するほど強力ではありません。

通常、seq は直接呼び出されません。その代わりに <*> という演算子が使われます。この演算子は第二引数を fun () => ... で包み、seq の呼び出しを単純化します。つまり、E1 <*> E2 は Seq.seq E1 (fun () => E2) の構文糖衣です。

seq を複数の引数で使えるようにするにあたって、Leanでの複数の引数を持つ関数が、実際には「残りの引数を待つ別の関数」を返す「単一の引数を持つ関数」であるということは重要な特徴です。言い換えると、seq の最初の引数が複数の引数を持っている場合、 seq の結果は2個目以降の残りの引数を待っていることになります。例えば、some Plus.plus は Option (Nat → Nat → Nat) 型を持ちます。ここで引数を一つ与えると、some Plus.plus <*> some 4 となり、型は Option (Nat → Nat) となります。これ自身も seq と一緒に使えるため、some Plus.plus <*> some 4 <*> some 7 は Option Nat 型を持ちます。

すべての関手がアプリカティブにはなりません。Pair は組み込みの直積型 Prod のようなものです：

structure Pair (α β : Type) : Type where
  first : α
  second : β

Except と同じように、Pair は Type → Type → Type 型を持ちます。これは Pair α が Type → Type 型を持ち、Functor インスタンスの定義が可能であることを意味します：

instance : Functor (Pair α) where
  map f x := ⟨x.first, f x.second⟩

これは Functor の約定に従います。

チェックする2つの特性は id <$> Pair.mk x y = Pair.mk x y と f <$> g <$> Pair.mk x y = (f ∘ g) <$> Pair.mk x y です。最初の特性は、左辺の評価を逐一評価し、それが右辺の形に評価されることが確認できればOKです：

id <$> Pair.mk x y
===>
Pair.mk x (id y)
===>
Pair.mk x y

2つ目は、両辺を逐一評価し、同じ結果が得られることを確認します：

f <$> g <$> Pair.mk x y
===>
f <$> Pair.mk x (g y)
===>
Pair.mk x (f (g y))

(f ∘ g) <$> Pair.mk x y
===>
Pair.mk x ((f ∘ g) y)
===>
Pair.mk x (f (g y))

しかし Applicative インスタンスを定義しようとしてもうまくいきません。pure の定義が必要になります：

def Pair.pure (x : β) : Pair α β := _

don't know how to synthesize placeholder
context:
β α : Type
x : β
⊢ Pair α β

スコープ内に β 型の値（つまり x ）があり、アンダースコアからのエラーメッセージは、次のステップとしてコンストラクタ Pair.mk を使用することを示唆しています：

def Pair.pure (x : β) : Pair α β := Pair.mk _ x

don't know how to synthesize placeholder for argument 'first'
context:
β α : Type
x : β
⊢ α

残念ながら、α 型を利用する余地はありません。なぜなら、pure は Applicative (Pair α) のインスタンスを定義するために、αとして 可能なすべての型 に対して機能する必要がありますが、これは不可能です。極端な話、呼び出し元は α を値を全く持たない Empty にすることもあるかもしれないのです。

非モナドなアプリカティブ関手

フォームへのユーザ入力のバリデーションにあたっては、いちいち1つずつエラーを報告するのではなく、まとめて一度にエラーを出すことが一般的に最善と考えられています。これによってユーザはフィールドごとにエラーをうんざりしながら修正することなく、コンピュータに受け入れられるために何が必要かを概観することができます。

理想的には、ユーザ入力のバリデーションは、それを行う関数の型に現れます。この関数はチェックが行われたことを体現するデータ型を返却すべきです。例えば、テキストボックスに数値が含まれているかどうかをチェックする関数は、実際の数値型を返すべきです。バリデーションのルーチンは、入力がバリデーションを通過しなかったことを例外を投げることで表現できます。しかし、例外には大きな欠点があります：最初のエラーでプログラムが終了してしまうため、エラーのリストを蓄積することができないのです。

一方で、エラーのリストを蓄積し、リストが空でなければ失敗にする一般的な設計パターンにも問題があります。入力データの各部分をバリデーションする if 文の長くネストされた列はメンテナンス性に欠け、出てきたエラーメッセージから何個かのエラーをいともたやすく見落とすでしょう。理想的には、バリデーションは新しい値を返しつつエラーメッセージを自動的に追跡して蓄積するようなAPIを使って動作するものであってほしいでしょう。

Validate というアプリカティブ関手はまさにそんなAPIを実装する1つの方法を提供します。Except モナドのように、Validate によってバリデーションされたデータを正確に特徴づける新しい値を構築することができます。しかし一方で Except と異なり、リストが空かどうかをチェックし忘れるリスク無しに複数のエラーを蓄積することができます。

ユーザ入力

ユーザ入力の例として、次のような構造を考えてみましょう：

structure RawInput where
  name : String
  birthYear : String

実装ビジネスロジックは以下の通りです：

名前は空であってはならない
誕生年は非負の数値でなければならない
誕生年は1900より大きく、かつバリデーションを行った年以下でなければならない

これらをデータ型として表現するには、部分型 と呼ばれる新しい機能が必要になります。このツールがあれば、バリデーションのフレームワークをエラーを追跡するアプリカティブ関手を使って書くことができ、バリデーションルールもこのフレームワークで実装することができます。

部分型

これらの条件を表現するにあたって最も簡単なのは、Subtype と呼ばれるLeanの型を1つ追加することです：

structure Subtype {α : Type} (p : α → Prop) where
  val : α
  property : p val

この構造体には2つの型パラメータがあります：1つはデータの型を表す暗黙パラメータ α で、もう1つは α に対する述語を表す明示的なパラメータ p です。述語（predicate）とは実際の文を生成するために値に置き換えることができる変数を持つ論理的な文であり、GetElem のパラメータが検索に用いる添え字が範囲内であることの意味を記述するのはその一例です。Subtype の場合、述語は α の値の中で述語が成り立つ部分集合を切り出します。この構造体の2つのフィールドはそれぞれ α の値と、その値が述語 p を満たす根拠です。Leanは Subtype に対して特別な構文を持っています。p が α → Prop 型を持つ場合、Subtype p 型は {x : α // p x} と書くこともでき、型が自動的に推論される場合は {x // p x} と書くことさえもできます。

正の整数を帰納的な型として表現することは明快で、プログラムしやすいです。しかし、これには重要な欠点があります。Nat と Int はLeanプログラムにおいては普通の帰納型の構造を持っていますが、コンパイラはこれらを特別に扱い、高速な任意精度の数値ライブラリを使用して実装します。これは後から追加されるユーサ定義型には当てはまりません。しかし、Nat の部分型を0以外の数に制限することで、コンパイル時に0を除きながら効率的な表現を使用することができます：

def FastPos : Type := {x : Nat // x > 0}

最も小さい正の整数はもちろん1です。さて、これは帰納型のコンストラクタではなく、角括弧で構成される構造体のインスタンスです。第1引数は基礎となる Nat で、第2引数はその Nat が0より大きいという根拠です：

def one : FastPos := ⟨1, by simp⟩

OfNat のインスタンスは Pos のインスタンスと非常によく似ていますが、n + 1 > 0 という根拠を提供するために短いタクティクによる証明を使う点が異なります：

instance : OfNat FastPos (n + 1) where
  ofNat := ⟨n + 1, by simp_arith⟩

simp_arith タクティクは simp に算術的な等式を追加したバージョンです。

部分型は諸刃の剣です。これによってバリデーションルールの効率的な表現を可能にしますが、これらのルールを維持する負担をライブラリのユーザに移し、ユーザは重要な不変量に違反していないことを証明しなければなりません。一般的には、ライブラリの内部で使用し、すべての不変量が満たされていることを自動的に保障するAPIをユーザに提供し、必要な証明はライブラリの内部で行うのが良いでしょう。

ある α 型の値が {x : α // p x} の部分型に含まれるかどうかを調べるには、通常 p x という命題が決定可能である必要があります。等式と順序クラスについての節では、決定可能な命題を if と一緒に使用する方法について説明しました。if を決定可能な命題で使用する場合、名前を指定することができます。then ブランチでは、その名前は命題が真であることの根拠に束縛され、else ブランチでは命題が偽であることの根拠に束縛されます。これは、与えられた Nat が正であるかどうかをチェックする時に便利です：

def Nat.asFastPos? (n : Nat) : Option FastPos :=
  if h : n > 0 then
    some ⟨n, h⟩
  else none

then ブランチでは、h は n > 0 という根拠に束縛され、この根拠は Subtype のコンストラクタの第2引数として使うことができます。

入力のバリデーション

バリデーションされたユーザ入力は、以下の技術を駆使してビジネスロジックを表現した構造体です：

構造体の型自体はバリデーションチェックが行われた年をエンコード。そのため CheckedInput 2019 は CheckedInput 2020 と同じ型ではありません。
誕生年は String ではなく Nat で表現
名前と誕生年のフィールドの許容される値を制約するために部分型を使用

structure CheckedInput (thisYear : Nat) : Type where
  name : {n : String // n ≠ ""}
  birthYear : {y : Nat // y > 1900 ∧ y ≤ thisYear}

入力のバリデータは現在の年と RawInput を引数に取り、チェック済みの入力か、少なくとも1つのバリデーション失敗のどちらかを返すべきです。これは Validate 型で表されます：

inductive Validate (ε α : Type) : Type where
  | ok : α → Validate ε α
  | errors : NonEmptyList ε → Validate ε α

見た目は Except によく似ています。唯一の違いは、error コンストラクタに複数の失敗を含めることができる点です。

Validateは関手です。これに関数をマッピングすることで、Except の Functor インスタンスと同じように、成功した値の場合はその値が変換されます：

instance : Functor (Validate ε) where
  map f
   | .ok x => .ok (f x)
   | .errors errs => .errors errs

Validate の Applicative インスタンスには Except のインスタンスと重要な違いがあります：Except のインスタンスは最初に遭遇したエラーで終了するのに対して、Validate のインスタンスは関数と引数のブランチの両方からのすべてのエラーを蓄積することに注意を払っています：

instance : Applicative (Validate ε) where
  pure := .ok
  seq f x :=
    match f with
    | .ok g => g <$> (x ())
    | .errors errs =>
      match x () with
      | .ok _ => .errors errs
      | .errors errs' => .errors (errs ++ errs')

.errors を NonEmptyList のコンストラクタと一緒に使うと少し冗長になります。reportError のような補助関数によって可読性が上がります。このアプリケーションでは、エラーのレポートはフィールド名とメッセージの組み合わせで構成されます：

def Field := String

def reportError (f : Field) (msg : String) : Validate (Field × String) α :=
  .errors { head := (f, msg), tail := [] }

Validate の Applicative インスタンスでは、各フィールドのチェック手順を個別に記述し、組み合わせることができます。名前のチェックでは、文字列が空でないことを確認し、その根拠を Subtype という形で返します。これは if の根拠による束縛のバージョンを使用しています：

def checkName (name : String) : Validate (Field × String) {n : String // n ≠ ""} :=
  if h : name = "" then
    reportError "name" "Required"
  else pure ⟨name, h⟩

then ブランチでは、h は name = "" という根拠に束縛され、else ブランチでは ¬name = "" という根拠に束縛されます。

バリデーションエラーによってはほかのチェックが不可能になってしまうケースも存在します。例えば、混乱したユーザが誕生年として数字の代わりに "syzygy" と書いた場合、誕生年のフィールドが1900年より大きいかどうかをチェックしても無意味です。数値の許容範囲をチェックすることは、そもそもフィールドに実際に数値が含まれていることを確認した後でのみ意味があります。これは関数 andThen を使って表現することができます：

def Validate.andThen (val : Validate ε α) (next : α → Validate ε β) : Validate ε β :=
  match val with
  | .errors errs => .errors errs
  | .ok x => next x

この関数の型シグネチャは Monad インスタンスの bind として使用するのに適していますが、そうしないのにはれっきとした理由があります。それについては Applicative の約定を説明する節で説明します。

誕生年が数字であることを確認するには、String.toNat? : String → Option Nat という組み込み関数が便利です。先に String.trim を使って先頭と末尾の空白を除去するととてもユーザフレンドリになります：

def checkYearIsNat (year : String) : Validate (Field × String) Nat :=
  match year.trim.toNat? with
  | none => reportError "birth year" "Must be digits"
  | some n => pure n

提供された年が予想される範囲内であることをチェックするには、if の根拠提供の形式をネストして使用します：

def checkBirthYear (thisYear year : Nat) : Validate (Field × String) {y : Nat // y > 1900 ∧ y ≤ thisYear} :=
  if h : year > 1900 then
    if h' : year ≤ thisYear then
      pure ⟨year, by simp [*]⟩
    else reportError "birth year" s!"Must be no later than {thisYear}"
  else reportError "birth year" "Must be after 1900"

最後に、これら3つの要素を seq を使って結合します：

def checkInput (year : Nat) (input : RawInput) : Validate (Field × String) (CheckedInput year) :=
  pure CheckedInput.mk <*>
    checkName input.name <*>
    (checkYearIsNat input.birthYear).andThen fun birthYearAsNat =>
      checkBirthYear year birthYearAsNat

checkInput をテストしてみると、実際に複数のフィードバックを返してくれることがわかるでしょう：

#eval checkInput 2023 {name := "David", birthYear := "1984"}

Validate.ok { name := "David", birthYear := 1984 }

#eval checkInput 2023 {name := "", birthYear := "2045"}

Validate.errors { head := ("name", "Required"), tail := [("birth year", "Must be no later than 2023")] }

#eval checkInput 2023 {name := "David", birthYear := "syzygy"}

Validate.errors { head := ("birth year", "Must be digits"), tail := [] }

checkInput による入力のバリデーションは、Monad に対する Applicative の重要な利点を示しています。なぜなら、>>= は最初のステップの値に基づいて残りのプログラムを変更するのに十分なパワーを提供するため、最初のステップから渡される値を 受け取らなくてはならないからです 。もし値を受け取らなかった場合（例えばエラーが発生した場合）、>>= はプログラムの残りの部分を実行することができません。Validate はどんな時でもプログラムの残りの部分を実行することが有用である理由を示しています：それ以前のデータが不要なケースでは、プログラムの残りの部分を実行することで有用な情報（この場合はより多くのバリデーションエラー）を得ることができます。Applicative の <*> は結果を再結合する前に両方の引数を実行することができます。同様に、>>= は逐次実行を強制します。各ステップは、次のステップを実行する前に完了しなければなりません。一般的にはこれは便利ですが、プログラムの実際のデータ依存関係から自然に生まれる異なるスレッドの並列実行を不可能にしてしまいます。Monad のようなより強力な抽象化によって、API利用者が利用できる柔軟性は向上しますが、API実装者が利用できる柔軟性は低下します。

Functional Programming in Lean 日本語訳

アプリカティブ関手

非モナドなアプリカティブ関手

ユーザ入力

部分型

入力のバリデーション