オルタナティブ

失敗からの復帰

Validate は入力を受け付ける方法が複数ある場合にも使用することができます。RawInput の形式の入力に対して前節の方法の代わりに、レガシーなシステムからの慣習に則ったビジネスルールは以下のようになります：

すべての人間ユーザは、4桁の誕生年を記入しなければならない。
1970年より前に生まれたユーザは古い記録が不完全なため氏名を記入する必要はない。
1970年より後に生まれたユーザは氏名を記入しなければならない。
企業は誕生年を "FIRM" とし、会社名を記入すること。

1970年生まれの利用者に該当する規定はありません。これに該当する場合は入力を諦めるか、誕生年を偽るか、このサービスの会社に電話をかけるかのいずれかになるでしょう。この会社は、これはビジネス上許容できるコストだと考えています。

以下の帰納型は、これらの記述されたルールに基づいた値を表現しています：

abbrev NonEmptyString := {s : String // s ≠ ""}

inductive LegacyCheckedInput where
  | humanBefore1970 :
    (birthYear : {y : Nat // y > 999 ∧ y < 1970}) →
    String →
    LegacyCheckedInput
  | humanAfter1970 :
    (birthYear : {y : Nat // y > 1970}) →
    NonEmptyString →
    LegacyCheckedInput
  | company :
    NonEmptyString →
    LegacyCheckedInput
deriving Repr

しかし、このルールに対応するバリデータは3つのケースすべてに対応しなければならないため、前節のものより複雑になります。入れ子になった一連の if 式として書くこともできますが、3つのケースを個別に設計しそれらを組み合わせる方が簡単です。そのためには、エラーメッセージを保持しながら失敗から回復する手段が必要になります：

def Validate.orElse (a : Validate ε α) (b : Unit → Validate ε α) : Validate ε α :=
  match a with
  | .ok x => .ok x
  | .errors errs1 =>
    match b () with
    | .ok x => .ok x
    | .errors errs2 => .errors (errs1 ++ errs2)

この失敗からの復帰パターンは、Leanに OrElese という名前の型クラスとそれに伴う組み込みの構文があるほど一般的です：

class OrElse (α : Type) where
  orElse : α → (Unit → α) → α

式 E1 <|> E2 は OrElse.orElse E1 (fun () => E2) の省略形です。Validate の OrElse インスタンスを使うことで、この構文をエラー復帰に使用することができます：

instance : OrElse (Validate ε α) where
  orElse := Validate.orElse

LegacyCheckedInput のバリデータは各コンストラクタのバリデータから構築することができます。会社用のルールでは誕生年は文字列 "FIRM" でなければならず、名前は空であってはなりません。しかし、コンストラクタ LegacyCheckedInput.company は誕生年をまったく表現しないため、単に <*> を使ってバリデーションすることはできません。ポイントは引数を無視する <*> 関数を使うことです。

型にこの根拠を付与することなく、論理条件が成立することをチェックするには checkThat を使用します：

def checkThat (condition : Bool) (field : Field) (msg : String) : Validate (Field × String) Unit :=
  if condition then pure () else reportError field msg

この checkCompany の定義は checkThat を使用し、その結果の Unit 値を捨てています：

def checkCompany (input : RawInput) : Validate (Field × String) LegacyCheckedInput :=
  pure (fun () name => .company name) <*>
    checkThat (input.birthYear == "FIRM") "birth year" "FIRM if a company" <*>
    checkName input.name

しかし、この定義はかなり煩雑です。これをシンプルにするにあたって2つの方法があります。1つ目は、最初の <*> の使用を、最初の引数が返す値を自動的に無視する *> という特殊なバージョンに置き換えることです。この演算子も SeqRight と呼ばれる型クラスによって制御され、E1 *> E2 は SeqRight.seqRight E1 (fun () => E2) の糖衣構文です：

class SeqRight (f : Type → Type) where
  seqRight : f α → (Unit → f β) → f β

seqRight の実装には seq によるデフォルト実装：seqRight (a : f α) (b : Unit → f β) : f β := pure (fun _ x => x) <*> a <*> b () が存在します。

seqRight を使うことで、checkCompany はもっとシンプルになります：

def checkCompany (input : RawInput) : Validate (Field × String) LegacyCheckedInput :=
  checkThat (input.birthYear == "FIRM") "birth year" "FIRM if a company" *>
  pure .company <*> checkName input.name

さらなる簡略化も可能です。すべての Applicative に対して、pure F <*> E は f <$> E と等価です。言い換えると、pure で Applicative 内に置かれた関数を seq を使って適用するのはやりすぎであり、Functor.map を使って適用すればよかったのです。この簡略化は以下のようになります：

def checkCompany (input : RawInput) : Validate (Field × String) LegacyCheckedInput :=
  checkThat (input.birthYear == "FIRM") "birth year" "FIRM if a company" *>
  .company <$> checkName input.name

LegacyCheckedInput の残り2つのコンストラクタは、フィールドに部分型を使用しています。部分型をチェックする汎用的なツールがあれば、さらに読みやすくなるでしょう：

def checkSubtype {α : Type} (v : α) (p : α → Prop) [Decidable (p v)] (err : ε) : Validate ε {x : α // p x} :=
  if h : p v then
    pure ⟨v, h⟩
  else
    .errors { head := err, tail := [] }

関数の引数リストにて、引数 v と p を指定した後に [Decidable (p v)] という型クラスが来ていることがミソです。そうでなければ手動で指定した値ではなく、自動的な暗黙の引数を追加で参照することになります。Decidable インスタンスは、命題 p v を if を使ってチェックできるようにするものです。

人間についての2つのケースでは追加の道具は必要ありません：

def checkHumanBefore1970 (input : RawInput) : Validate (Field × String) LegacyCheckedInput :=
  (checkYearIsNat input.birthYear).andThen fun y =>
    .humanBefore1970 <$>
      checkSubtype y (fun x => x > 999 ∧ x < 1970) ("birth year", "less than 1970") <*>
      pure input.name

def checkHumanAfter1970 (input : RawInput) : Validate (Field × String) LegacyCheckedInput :=
  (checkYearIsNat input.birthYear).andThen fun y =>
    .humanAfter1970 <$>
      checkSubtype y (· > 1970) ("birth year", "greater than 1970") <*>
      checkName input.name

以上の3つのケースのバリデータは <|> を使って組み合わせることができます：

def checkLegacyInput (input : RawInput) : Validate (Field × String) LegacyCheckedInput :=
  checkCompany input <|> checkHumanBefore1970 input <|> checkHumanAfter1970 input

成功したケースでは、期待通りに LegacyCheckedInput のコンストラクタが返されます：

#eval checkLegacyInput ⟨"Johnny's Troll Groomers", "FIRM"⟩

Validate.ok (LegacyCheckedInput.company "Johnny's Troll Groomers")

#eval checkLegacyInput ⟨"Johnny", "1963"⟩

Validate.ok (LegacyCheckedInput.humanBefore1970 1963 "Johnny")

#eval checkLegacyInput ⟨"", "1963"⟩

Validate.ok (LegacyCheckedInput.humanBefore1970 1963 "")

最悪の入力においては、起こりうるすべての失敗が返されます：

#eval checkLegacyInput ⟨"", "1970"⟩

Validate.errors
  { head := ("birth year", "FIRM if a company"),
    tail := [("name", "Required"),
             ("birth year", "less than 1970"),
             ("birth year", "greater than 1970"),
             ("name", "Required")] }

`Alternative` クラス

多くの型が失敗と復帰の概念をサポートしています。様々なモナドでの算術式の評価についての節で定義した Many モナドや、Option 型はそのような型の1つです。どちらも失敗に対して理由を付与しません（一方で Except と Validate では何が間違っていたのかを示す必要があります）。

Alternative クラスはアプリカティブ関手に失敗と復帰のための演算子を追加したものとして記述されます：

class Alternative (f : Type → Type) extends Applicative f where
  failure : f α
  orElse : f α → (Unit → f α) → f α

Add α の実装者が HAdd α α α のインスタンスをタダで取得できるように、Alternative の実装者は OrElse インスタンスを何もせずに手に入れることができます：

instance [Alternative f] : OrElse (f α) where
  orElse := Alternative.orElse

Option に対する Alternative は引数のうち一番初めの非 none を保持するように実装されます：

instance : Alternative Option where
  failure := none
  orElse
    | some x, _ => some x
    | none, y => y ()

同様に、Many の実装は Many.union の一般的な構造に従っていますが、遅延評価のための Unit パラメータの配置が異なるため若干の違いがあります：

def Many.orElse : Many α → (Unit → Many α) → Many α
  | .none, ys => ys ()
  | .more x xs, ys => .more x (fun () => orElse (xs ()) ys)

instance : Alternative Many where
  failure := .none
  orElse := Many.orElse

他の型クラスと同様に、Alternative は Alternative を実装したアプリカティブ関手 すべて に対して機能する様々な操作を定義することができます。最も重要なもののの1つは guard で、これは決定可能な命題が偽の場合に failure を実行します：

def guard [Alternative f] (p : Prop) [Decidable p] : f Unit :=
  if p then
    pure ()
  else failure

これはモナドを使ったプログラムの実行を早期に終了させるのに非常に便利です。Many においては、ある自然数に対するすべての偶数の約数を計算する以下のプログラムのように、検索の分岐全体をフィルタリングするために使うことができます：

def Many.countdown : Nat → Many Nat
  | 0 => .none
  | n + 1 => .more n (fun () => countdown n)

def evenDivisors (n : Nat) : Many Nat := do
  let k ← Many.countdown (n + 1)
  guard (k % 2 = 0)
  guard (n % k = 0)
  pure k

20 に対して実行すると予想通りの結果を得ます：

#eval (evenDivisors 20).takeAll

[20, 10, 4, 2]

演習問題

バリデータの利便性向上

<|> を使用した Validate プログラムから返されるエラーは読みにくいものになります。というのも、あるエラーがエラーのリストに含まれているということは、ただ単にそのエラーがバリデーション中の経路の どこか で発生したということを意味します。より構造化されたエラーレポートがあれば、ユーザをより正確に導くことができます：

Validate.error 内の NonEmptyList をただの型変数に置き換え、Applicative (Validate ε) と OrElse (Validate ε α) インスタンスの定義を更新して Append ε インスタンスが利用可能であることだけを要求するようにしてください。
バリデーション中に発生するすべてのエラーを変換する関数 Validate.mapErrors : Validate ε α → (ε → ε') → Validate ε' α を定義してください。
エラーを表すデータ型 TypeError を使って、レガシーなバリデーションシステムを書き換えることで3つの選択肢を通してその経路を追跡できるようにしてください。
TypeError に蓄積された警告とエラーをユーザフレンドリに出力する関数 report : TreeError → String を書いてください。

inductive TreeError where
  | field : Field → String → TreeError
  | path : String → TreeError → TreeError
  | both : TreeError → TreeError → TreeError

instance : Append TreeError where
  append := .both

Functional Programming in Lean 日本語訳

オルタナティブ

失敗からの復帰

Alternative クラス

演習問題

バリデータの利便性向上

`Alternative` クラス