FOLIOでのrefined活用法 - ドメインを型で形式知化し、契約を型で表すことで認知漏れを防ぐ

FOLIOアドベントカレンダー2021 12日目です。

FOLIOではrefinedというライブラリを採用しているので、活用事例とその目的について考えていこうと思います。

お品書きは以下です。

  • refinedとは
  • ドメイン知識の形式知化
  • 契約を型で表すことによる認知漏れリスクへの対策
  • プラットフォームとしてのrefined
  • まとめ

refinedとは

refined はScalaでrefinement typeを表現するためのライブラリで、Haskellの 同名ライブラリ のScala版として開発されました。

refinement type（篩型, ふるい型) はざっくりいうと、「値が0以上である」とか「長さが1以上である」といった制約を型で表現し、静的に保証するための概念で、1991年にFreemanらによってRefinement Types for MLで提案されました。

利用方法

refinedでは制約を val a: Int Refined Positive のように、元の型に対して特定の述語を追加する形で表現します。

この制約付きの型に対応する値を生成するためには二種類の方法があります。

1つ目の方法はマクロを使った方法です。

import eu.timepit.refined.auto._

val a: Int Refined Positive = 1
val b: Int Refined Positive = -1 // コンパイル時に値が検証されるためエラー

この方式は便利ですが当然ながらコンパイル時に値が特定可能な場合（数値をリテラルで初期化する場合等）でのみ利用が可能です。

2つ目の方法はランタイムに値を検証するメソッドを呼ぶ方法です。制約を満たさない場合はEitherや例外の形でエラーが返されます。

val i = 10
val a: Either[String, Int Refined Positive] = refineV[Positive](i)

 なお Int Refined Positive の場合は下記のように PosInt.from や PosInt.unsafeFrom のようなメソッドを使うことも可能です。

val i = 10
val a: Either[String, PosInt] = PosInt.from(i)

val j = -10
val b: PosInt = PosInt.unsafeFrom(j) // 制約を満たしていないため実行時例外

余談ですが PosIntのような型はRefinedTypeOps を継承すれば作成可能です。FOLIOでは正の値(>0)を表現する PosInt の他に、非負の値(>= 0)を表現する NonNegInt 、これらの BigDecimal 版である PosBigDecimal , NonNegBigDecimal などをよく利用しています。

その他の使い方については refinedのREADME や さらなる型安全性を求めて ~ Refinement TypeをScalaで実現する ~ - Visional Engineering Blog にとても分かりやすい解説があります。

ドメイン知識の形式知化

FOLIOの中でも筆者が所属するチームは口座残高や株式売買に関わるシステムを担当することが多く、現金残高・証券残高・証券残高評価額・平均取得単価・約定単価・約定数量・約定金額・実現損益・実現損益前日比・含み損益・含み損益前日比など一目には違いが分かりにくい”お金や数量を表現する値”がたくさん存在しています。

複雑なドメインと戦いながらロボアド基盤をリプレースするときにした工夫 でも(20ページ目などで)発表したのですが、これらの概念を全体的に把握するだけでも一定のハードルがあります。

また、これらの概念を理解したとしても、それらが実際に取る値を理解するという次のハードルがあります。 証券残高評価額が非負の値を取るとしても、証券残高評価額の前日比は正負両方の値を取ります。現金残高は一見すると非負の値を取りそうですが業務フローによってはシステム的に負の残高を許容することもあります。

こういった知識を持たないまま開発を行うと、想定していない計算が行われたり重要なエッジケースがテストされないまま本番稼働を迎えるリスクがあります。

refinedを使うと以下のように暗黙的に持っていた不変条件に関する知識を宣言的に明示することができます。

case class OrderAmount(value: PosBigDecimal) // この場合は注文金額は0にはならない
case class OrderAmount(value: NonNegBigDecimal) // この場合は注文金額は0になりうる

上記のようなクラスを新しく作成する場合にドメインに関する知識を宣言的に表明することで、ドメイン層のクラスをチームで共有可能な知識置き場にすることができます。

契約を型で表すことによる認知漏れリスクへの対策

前述したコードの書き方は不変条件の表明を通した、いわゆる契約プログラミングの実践の一例と言えると思います。

Scalaには契約プログラミング用のメソッドとしてrequireやensuringなどが用意されている ので、これらの手法とrefinedを使った手法では何が違うのか考えてみたいと思います。

契約を型で表すことのメリット

refinedを使って契約を型で表現する手法では、fromやunsafeFromのような契約の検査を行うコードを明示的に書く必要があります。これはプライマリコンストラクタ等に require(value > 0) を記述するような手法と異なる点です。

後者の方式でも契約違反が発生した場合に後続の処理を停止させることは可能です。一方でこの処理が契約違反になる可能性があるかどうかについてはプログラマが注意を払う必要があります。

case class Fee(value: BigDecimal) {
  require(value > 0)
}

case class Cash(value: BigDecimal) {
  require(value >= 0)

  def calc(f: Fee): Cash =  Cash(value - f.value) // これは契約を満たさない可能性があるが、プログラマがそれを認識しているとは限らない
}

例のcalcメソッドのような処理を書く際に不変条件を意識できなかったとすると、これはエッジケースの認知漏れにつながる可能性があります。 もしかすると考慮漏れが発生しており設計・仕様へのフィードバックが必要な状態かもしれませんし、あるいは仕様の（暗黙の）範囲内で（設計書には書いてないけど）エラーハンドリングを行う必要があるかもしれません。

脱線: 負にならないとされているものが負になったらどうしようもないしエラーをハンドリングする必要があるのか？という疑問がありそうなので少しだけ背景の解説を入れておきます。例えば全口座を処理するバッチではエラーがあった場合に即座にプロセスを終了させると全口座の処理がストップしてしまいます。こうなると復旧が長時間化し、障害規模も単一口座から全口座へ広がってしまいます。これを避けるため該当口座の処理をskipし次口座の処理を開始、全口座処理終了後にskipされた口座についてエラーを報知するといったエラーハンドリングを行う場合があります。*1

バグや仕様の不整合でしか起こり得ないケースなのか、データによってはあり得るケースなのかによって対応は分かれると思いますが、どちらにせよそういうエッジケースがあるということを認知しなければ対応は始まりません。ここを認知しなければエラーハンドリングや適切なテストも行われず、仕様の考慮漏れを起こしたまま本番環境にデプロイされてしまう可能性も出てきてしまいます。

一方でrefinedを使って契約を型で表現する手法では、ある値がNonNegBigDecimalなのかPosBigDecimalなのかを何らかの検証を通して保証する必要があります。

case class Fee(value: PosBigDecimal)

case class Cash(value: NonNegBigDecimal) {

  def calc(c: Cash, f: Fee): Cash =  {
    // NonNegかどうかの検査をしないとCashのインスタンスを作れない。
   // プログラマは負になる場合が仕様の範囲でありえるかどうか考え、エラーハンドルを行うか異常終了させるか検討する必要が出てくる。
    // 下記コードでは契約違反の場合は例外になる。
    val nonNeg = NonNegBigDecimal.unsafeFrom(c.value.value - f.value.value)
    Cash(nonNeg)
  }
}

このようなコードスタイルの場合、仕様上ありえない(バグ以外では成功する）のか、データとしては不正なものの厳密にはあり得ること（バグではなく仕様の範囲内）なのかをプログラマが考えるきっかけがうまれます。

計算結果がマイナスになりうるといったエッジケースを認知することさえできれば、エラーハンドリング用コードの追加は容易ですし、異常終了でよいとしても復旧用マニュアルの整備を含めた事前のリスク対応索の整備が可能です。(検討を行った結果、仕様上ありえないことが分かったならその理由をコメントに書いてunsafeFromを呼び出してもよいでしょう。) いずれにせよどういう事象がありえるのか？の分析を行う機会が得られれば何らかの対応を取ることが可能になります。

つまり、このような手法を使うことで

  • エッジケースがそもそもあるんじゃないか？といった点に気づくきっかけを得られる
  • （上記を通して）設計段階でも開発段階でもテスト段階でも気づかず、エッジケースが本番で発生し障害になるというリスクを低減できる

といった効果が得られると期待しています。

もちろんrequire等を使った契約プログラミングの「誤った計算が行われた状態で処理が進んでしまうことがない」といった利点もそのまま享受できます。

nullとOptionの関係に近いかもしれない

上記で例に上げたエッジケース（マイナスになりうる）などは設計段階でもたいていは拾われますし、熟練のプログラマなら「ドメインオブジェクトなんだから不変条件あるし、それのチェックは当然」 と当たり前のように気づけるかもしれません。なにより境界値分析などでテストケースに上がる部分でもあるので、上述のようなリスクが本番環境で顕在化することは実際にはあまり多くはないのかもしれません。

一方で、「必ず目を配りながらコードを書く必要がある」、「うっかり考慮を忘れると本番でエラーが発生しバッチ処理が異常終了する」といったことはプログラマとしては可能な限り避けたいものです。

これらと同じような問題を避ける手法として「nullをOptionで表現する」手法があると考えています。nullも設計段階で拾うべきですし熟練のプログラマならNullPointerExceptionなんて出さないかもしれませんし、テストケースで確実にテストされるべきですが、実際にはNullPointerExceptionで涙を流した人は多いのではないでしょうか。

値がないことをnullの代わりにOptionで表現することで予期せぬ場所で例外が出るのを防ぐことができたり、nullになりうる箇所が制限されることでデバッグや障害時の原因調査を迅速に行うことが可能です。同様のことは事前条件として value != null を書くことでも実現できますが、「値はnullではない」・「値はnullになりうる」という契約をOptionのような型で表現することで（mapとかgetOrElseみたいな面倒なコードと引き換えに）安全なコードを手に入れることができますし、「ここ値ない可能性ありますけどどうしましょう？」といった相談も自然にできるようになると思います。

nullをOptionにしてもテストシナリオの分析やテストが不要になるわけではないのと同様に、refinedで契約を型として表してもそれらが不要になるわけではありませんが上記と同じようなメリットを得られるのではないかと考えています。

余談: 顕在的契約計算あるいはHybrid Type Checkingについて

ちなみにrefinement typeを利用して契約計算を行う手法を顕在的契約計算やHybrid Type Checkingというようです。

後者の論文では動的な契約の検査の欠点として

dynamic checking provides only limited coverage – specifications are only checked on data values and code paths of actual executions. Thus, dynamic checking often results in incomplete and late (possibly post-deployment) detection of defects.

ということが挙げられています。動的な契約の検査は実行時にしか行われず、また与えられた値に対してのみの検査となるため、テストは通っていてもデプロイした後に契約を満たさない値が与えられてエラーが出る可能性があるということのようです。対照的に静的な型検査では網羅的な検査が事前に行われるためこのようなことは通常起こりません。

すべてを静的型で検査するぞ！うおー型安全！！！と行きたいところですが、残念ながら表現力豊かな型システムでは、ある型がある述語を満足するかを静的に検査するのが難しい（決定可能でなくなる）ケースがあったりリーズナブルな時間内に型検査を終わらせることが難しくなるようです。

しかし、明らかに型が合っているプログラムについては短時間で型検査を終わらせることは可能ですし、逆に明らかに型が合わないプログラムをエラーと判定することも短時間で可能そうです。 そこでHybridなアプローチとして静的に検証可能な範囲では静的な検査、実行時に行う必要があるような検査では動的な検査（契約違反なら例外）を挿入することで両者の欠点を補いたいというモチベーションでHybrid Type Checkingが提案されていそうです。

このようなハイブリッドなアプローチを行うことで

  • 静的に検査可能な部分は静的に検査
    • 型検査を通した網羅性の担保
    • 実行時の検査実行によるオーバーヘッド削減
  • 動的な検査の強制

といったメリットを享受することが可能そうです。

refinedを使ったコードの場合

  • 静的にチェック可能な関係は静的にチェックされる
    • 例えば NonNegInt に PosInt は代入可能だが逆は不可といった単純なサブタイピング関係はコンパイル時にチェックされる
  • それ以外のものは動的なチェックとなるが検査は強制される
    • 例えばNonNegIntのfromやunsafeFromのどちらでも実行時の検査が行われる

といった特徴を持っていますので、これも一種の顕在的契約計算の理論に基づいたプログラミング方法といえるかもしれません。（顕在的契約プログラミングみたいな単語を連想しましたがググった感じそういう用語はなさそうでした。）

ただし実際にコードを書いてみると静的にチェック可能な部分は思ったより少ないかもしれません。（例えばPosInt + PosInt = PosInt であるということすら静的には保証できません。 参考: refinedでPosInt + PosInt を PosIntにしたい - だいたいよくわからないブログ ）

こういったものは研究が進んで実装的にこなれてきて業務的に使いやすい物が産まれるまで時間がかかりますし、現段階では無闇に静的にチェックする範囲を広げると辛いかもしれませんが、時代が進んでいくとこういった研究の恩恵も享受できるかもしれません。

プラットフォームとしてのrefined

ここまで、不変条件を宣言的に型として表明しそれを保証する利点を述べてきました。

しかし、refinedを使わずともファクトリーメソッドで必ずチェックするようにすればvalue object自体が契約を表明する型になるんでないの？という声もありそうです。 実際、ファクトリーメソッドでEitherを返すようにすればCashのインスタンスを作ろうとした段階でチェックが必要なことに気がつけます、

一応

  • refinedであれば静的な保証ですむ場合がある(例えばNonNegBigDecimalのvalueを別のクラスに詰め替える場合は動的な検査は不要)
  • より宣言的であり、ファクトリーメソッドの実装を見に行く必要がない
  • 値域を表明するための方法(Pos等以外にもGreater[5]やRegex["[0-9]+"]など)が確立されており、実装者による表現方法のブレが少ない

といったメリットがあると思いますし、refinedを使ってもファクトリーメソッドが使えなくなるわけではないのでapplyを直接呼び出すのが気になる人はrefinedとファクトリーメソッドの併用することも可能です。

とはいえ、refinedを使わずに自前でfrom, unsafeFrom相当のファクトリーメソッドを作成することはもちろん可能ですし十分実用可能な範囲だと思います。

じゃあrefined使う意味ないよねってことになると寂しいので、こういった保証にrefinedを使う副次的な利点としてrefined自体がScalaライブラリのエコシステム内で既に受け入れられているという点も挙げておきます。

例えば

といった有名どころのライブラリでrefinedを使ったクラスのサポートが行われています。

そのためjsonのデシリアライズ時やdbからのselect時にフィールドを一つずつ検査するコード（あるいは自前のファクトリーメソッドを自動でいい感じに呼んでくれる仕組み）を自分で書かずとも自動で検証を行ってくれます。

こういった点は自前でファクトリーメソッドを作る方法に比べたときの既存のライブラリを使うメリットと言えそうです。

コーディングスタイルによってはファクトリーメソッドで検証するから上記は不要だ！という人もいるかもしれませんが、ある程度マッピングを簡略化できるので便利に使える人もいるかも知れません。

まとめ

この記事ではScalaのrefinedというライブラリについて、およびFOLIOでの実用例について解説しました。

主なメリットは３つです。

  • ドメイン知識の形式知化
    • 似たような値がたくさんあるドメインに対する知識を型で表現するだけでなく、その不変条件も型で表現することでドメイン上の暗黙知を形式知に転換し、チームで共有可能にする。
  • 契約を型で表すことによる認知漏れリスクへの対策
    • 契約プログラミングにおけるランタイムの安全性に加え、エラーハンドリング自体がそもそも不足してしまうといったエッジケースの「認知漏れ」に起因するリスクを低減する。
  • プラットフォームとしてのrefinedの利便性
    • 様々なライブラリと連携した一括検査によって生産性を向上させる。

だいぶ長々と書きましたが、型で表現されてたら便利かもね！程度の話でした。

*1:もちろん明らかに何かおかしい場合は止めたほうがいいので全部そうするとは限りません。