型レベルステートマシンでビジネスロジックのバグを構造的に不可能にする

概要¶

ビジネスロジックのバグ（特にステート管理の不整合）を型レベルで構造的に書けなくする Haskell ライブラリの実装記録。Functional Event Sourcing（Decider パターン）を基盤に、decide と evolve を同じ型定義から導出することでドリフトを不可能にする。

詳細¶

問題：手書き Decider が抱えるバグ¶

Functional Event Sourcing では Decider を手書きする：

data Decider cmd event state = Decider
  { decide      :: cmd -> state -> [event]
  , evolve      :: state -> event -> state
  , initialState :: state
  , isTerminal  :: state -> Bool
  }

手書きすると以下の問題が起きる： - decide と evolve のミスマッチ（枝の抜け漏れ） - evolve が静かにドリフトし、イベントのリプレイが壊れる

解決策：型レベルステートマシン DSL¶

ワークフローを 型レベルのエッジ定義 で記述し、decide と evolve を自動導出：

userReg :: Decider UserCmd UserEvent UserState
userReg = buildTransducer $ do
  from PotentialCustomer $
    onCmd inCtorStart $ do
      slot "email"         email
      slot "confirmCode"   confirmCode
      slot "registeredAt"  (...)
      emit wireRegistrationStarted
      goto Registering

  from RequiresConfirmation $
    onCmd inCtorConfirm $ do
      requireEq confirmCode confirmCode   -- コンファームコードの一致チェック
      slot "confirmedAt" (...)
      emit wireAccountConfirmed
      goto Confirmed

    onCmd inCtorResend $ do
      slot "confirmCode" code
      emit wireConfirmationResent
      goto RequiresConfirmation

    onCmd inCtorGdpr $ do
      slot "deletedAt" (...)
      goto Deleted

ポイント：evolve が存在しない。 エッジ定義から replay（逆方向）が自動生成されるため、decide と evolve が不一致になることが構造的に不可能。

3つの保証¶

ドリフト不可: decide と evolve が同一定義から導出 → 絶対に不一致にならない
Mermaid 図の自動生成: コードから直接ステートマシン図が生成 → コードレビューや設計ドキュメントで視覚的に検証可能
SMT ベースの CI チェッカー: ビジネス不変条件（「Confirmed 状態にはコード一致チェックなしに到達できない」「すべての開始登録は終端状態に到達する」「deletedAt は非終端頂点にセットされない」）を Z3 などの SMT ソルバーで証明または反例提示

なぜ重要か / いつ使うか¶

コーディングエージェントとの相性: 「AIが生成したコードでも絶対にバグを出荷しない」という目標で設計されている
複雑なワークフロー: ユーザー登録・決済・予約など、ステート遷移が多いドメインで威力を発揮
トレードオフ: Haskell 特有の型システムに依存。Go/TypeScript では型レベルの表現力が異なるため直接移植は難しいが、パターン（Decider + 単一型定義からの自動導出）は参考になる