Idrisでビジネスロジックを書く場合どのように証明を書けるのか気になった

背景

最近、輪読会でIdrisの勉強をしました。
教材はプログラング言語Idrisに入門させたい（v0.9）を使ったのですが、ド・モルガンの法則等の証明はとても興味深かったです。

証明を書くことで、単体テスト等で確認していたことがコンパイラで賄える点は非常に便利だと感じました。ただビジネスロジックを書くうえで証明を使うイメージができなかったため、輪読会中に例として挙がった承認フローを用いて書いてみました。

前提

• Idris2（0.8.0）

承認フローの要件

今回は以下のような承認フローを題材にします。

ルールをまとめると以下のとおりです。

• 申請はスムーズに通れば 下書き → 提出済 → 審査中 → 承認済 の順に進む
• 申請が 審査中 の場合、 承認 されるか 差戻し になる
  • 差戻し された場合は 再提出 して、提出済 に戻る
• 申請は 承認済 ・ キャンセル済 でなければキャンセルできる
• 承認済 と キャンセル済 は終端状態

このルールを「コンパイル時に保証する」のが今回の目標です。

状態の定義

まずは申請が取りうる状態を定義します。

data Status = Draft       -- 下書き
            | Submitted   -- 提出済
            | UnderReview -- 審査中
            | Approved    -- 承認済
            | Rejected    -- 差戻し
            | Cancelled   -- キャンセル済

キャンセル可能な状態を型で定義する

状態遷移の前に、キャンセル可能な状態を型として定義します。

data Cancellable : Status -> Type where
  CanDraft       : Cancellable Draft
  CanSubmitted   : Cancellable Submitted
  CanUnderReview : Cancellable UnderReview
  CanRejected    : Cancellable Rejected

Cancellable は「その状態からキャンセルできる」ことを表す型です。Approved と Cancelled に対するコンストラクタが存在しないため、これらの状態からはキャンセルできないことが型レベルで表現されています。

状態遷移を型で定義する

次に状態遷移を型で表現します。

data Transition : Status -> Status -> Type where
  Submit      : Transition Draft       Submitted
  StartReview : Transition Submitted   UnderReview
  Approve     : Transition UnderReview Approved
  Reject      : Transition UnderReview Rejected
  Resubmit    : Transition Rejected    Submitted
  Cancel      : Cancellable s -> Transition s Cancelled

命題としての読み方（Curry-Howard対応）

ここで重要なのが、Curry-Howard対応という考え方です。

Idris	論理
型	命題
値	証明

この対応で読むと：

• Transition Draft Submitted という型は「Draft → Submitted への遷移は正当である」という命題
• Submit という値はその命題の証明

コンストラクタが存在する遷移は正当、存在しない遷移は不正と定義しているわけです。

Transition Draft Submitted    → Submit で構築できる    → 正当な遷移
Transition Draft Approved     → 構築する手段がない     → 不正な遷移

不正な遷移は値を構築する手段がないので、そもそもコンパイルが通りません。

Cancel の定義

Cancel : Cancellable s -> Transition s Cancelled

命題として読むと「状態 s がキャンセル可能（Cancellable s）であるならば、s から Cancelled への遷移は正当である（Transition s Cancelled）」となります。

Cancel は Cancellable s 型の値を引数として要求するコンストラクタです。Cancellable Approved や Cancellable Cancelled のコンストラクタは存在しないため、これらの状態から Cancel を構築することはできません。これにより「承認済・キャンセル済からのキャンセルは不可」が型レベルで強制されます。

Refl とは

以降の証明で繰り返し登場する Refl について先に説明します。

Refl は等式型 Equal の唯一のコンストラクタです。

data Equal : a -> b -> Type where
  Refl : Equal x x

Refl : Equal x x は「同じ値同士は等しい」という自明な証明です。x は暗黙引数なので、コンパイラが型推論で自動的に決定します。なお、Idris2では = は Equal の中置記法として使えるため、x = x と書くこともできます。

証明1: 遷移元の厳密性

ここからは、定義した状態遷移に対する証明を書いていきます。

承認済に至る直前は必ず審査中

approvedNeedsReview : Transition s Approved -> s = UnderReview
approvedNeedsReview Approve = Refl

1行目は型シグネチャで、「Transition s Approved 型の値が存在するなら、s = UnderReview である」という命題です。

2行目がその証明になっています。ここを段階的に見ていきましょう。

まず引数 Transition s Approved にマッチするコンストラクタを探します。

コンストラクタ	型	マッチするか
Submit	Transition Draft Submitted	2番目が Approved でない。✗
StartReview	Transition Submitted UnderReview	2番目が Approved でない。✗
Approve	Transition UnderReview Approved	✓
Reject	Transition UnderReview Rejected	2番目が Approved でない。✗
Resubmit	Transition Rejected Submitted	2番目が Approved でない。✗
Cancel	Cancellable s -> Transition s Cancelled	2番目が Approved でない。✗

Approve しかマッチしません。Approve : Transition UnderReview Approved なので、パターンマッチした瞬間にコンパイラは s = UnderReview と確定します。

前述の Refl を使って、この証明がどう組み立てられるか見てみましょう。

1. Approve にマッチ → s = UnderReview が確定
2. 返り値の型 s = UnderReview が UnderReview = UnderReview に確定
3. Refl : x = x の x にコンパイラが UnderReview を代入
4. Refl : UnderReview = UnderReview として構築完了

つまりパターンマッチで全ての場合を網羅した結果、Approve しかありえないとコンパイラが確認し、その情報から Refl が構築できることで証明が完成します。

審査中に至る直前は必ず提出済

reviewNeedsSubmission : Transition s UnderReview -> s = Submitted
reviewNeedsSubmission StartReview = Refl

上と同じパターンです。Transition s UnderReview にマッチするのは StartReview だけなので、s = Submitted が確定します。

提出済に至る前は下書きか差戻しのどちらか

submittedOrigin : Transition s Submitted -> Either (s = Draft) (s = Rejected)
submittedOrigin Submit   = Left Refl
submittedOrigin Resubmit = Right Refl

今回は Transition s Submitted にマッチするコンストラクタが Submit（Draft → Submitted）と Resubmit（Rejected → Submitted）の2つあります。遷移元が1通りに定まらないので、「AまたはB」を表す型である Either で表現しています。

• Submit にマッチ → s = Draft が確定 → Left Refl
• Resubmit にマッチ → s = Rejected が確定 → Right Refl

証明2: 終端状態の証明

承認済からは遷移できない

approvedIsTerminal : Transition Approved s -> Void
approvedIsTerminal (Cancel prf) impossible

Void は「値を構築する手段が一切ない型」で、いわゆる矛盾に対応します。つまりこの型シグネチャは「Approved から遷移できると仮定すると矛盾が導ける」という命題です。

なぜ Cancel のケースを書く必要があるのか

Submit や Approve などのコンストラクタは遷移元が Draft や UnderReview といった具体的な型で固定されているため、Transition Approved s との照合で即座に除外されます。しかし Cancel : Cancellable s -> Transition s Cancelled の s は多相的なので、s = Approved となる可能性をコンパイラは構文だけでは排除できません。そのため Cancel のケースを明示的に書いて、到達不能であることを示す必要があります。

impossible とは

impossible は Refl のような値や関数ではなく、Idrisの組み込みキーワードです。パターンマッチの右辺に書くことで、「このパターンに到達する値は論理的に構築不可能である」とコンパイラに検証させます。もし実際には到達可能なパターンに impossible を書いた場合、コンパイルエラーになります。

今回のケースでは、Cancel は Cancellable Approved 型の値を要求しますが、Cancellable の定義に Approved に対するコンストラクタは存在しません。つまり Cancellable Approved 型の値は構築できず、Cancel prf というパターン自体が成立し得ないため、impossible が受理されます。結果として、Approved からの遷移は一切存在しないことが証明されます。

キャンセル済からも遷移できない

cancelledIsTerminal : Transition Cancelled s -> Void
cancelledIsTerminal (Cancel prf) impossible

同じ構造です。Cancellable Cancelled のコンストラクタも存在しないため、impossible で証明できます。

コード全容

以下は記事中で解説したコードの全容です。

ApprovalFlow.idr

module ApprovalFlow

-- 申請の状態
data Status = Draft
            | Submitted
            | UnderReview
            | Approved
            | Rejected
            | Cancelled

-- キャンセル可能な状態
data Cancellable : Status -> Type where
  CanDraft       : Cancellable Draft
  CanSubmitted   : Cancellable Submitted
  CanUnderReview : Cancellable UnderReview
  CanRejected    : Cancellable Rejected

-- 状態遷移を型レベルで定義
data Transition : Status -> Status -> Type where
  Submit      : Transition Draft       Submitted
  StartReview : Transition Submitted   UnderReview
  Approve     : Transition UnderReview Approved
  Reject      : Transition UnderReview Rejected
  Resubmit    : Transition Rejected    Submitted
  Cancel      : Cancellable s -> Transition s Cancelled

-- 証明1: 各状態への遷移元は厳密に決まっている
approvedNeedsReview : Transition s Approved -> s = UnderReview
approvedNeedsReview Approve = Refl

reviewNeedsSubmission : Transition s UnderReview -> s = Submitted
reviewNeedsSubmission StartReview = Refl

submittedOrigin : Transition s Submitted -> Either (s = Draft) (s = Rejected)
submittedOrigin Submit   = Left Refl
submittedOrigin Resubmit = Right Refl

-- 証明2: 終端状態の証明
approvedIsTerminal : Transition Approved s -> Void
approvedIsTerminal (Cancel prf) impossible

cancelledIsTerminal : Transition Cancelled s -> Void
cancelledIsTerminal (Cancel prf) impossible

終わりに

今回のコードでは、Idrisの依存型を使って承認フローの状態遷移を型レベルで定義し、以下をコンパイル時に証明しました。

• 各状態への遷移元が厳密に決まっていること
• 承認済・キャンセル済が終端状態であること

普段バリデーションや単体テストで確認している内容を、コンパイラで保証できる点は非常に魅力的だと思いました。