refined を使って分数の制約を型で表してみる

値の制約を型レベルで表現するライブラリ refined を最近知った。ドメインの不変条件を型としてコンパイル時に成立させられるのは、すごく良さそうな気がする。特に複雑なドメインモデルの中でこそ価値が高まる期待もあるが、まずは「ゼロじゃない整数」と「分数」からなる小さなドメインで試してみる。

やったこと

• 「分母は非ゼロ」という「制約」をrefinedで表現して分数型Rationalを実装する。
• プロパティベースのテストとの相性も軽く見てみる。

準備等

依存関係は以下の感じ

    compilerPlugin("org.spire-math" %% "kind-projector" % "0.9.4"),
    "org.typelevel" % "cats-core_2.12" % "1.0.0-RC2",
    "org.typelevel" % "cats-laws_2.12" % "1.0.0-RC2",
    "eu.timepit" %% "refined"            % "0.8.5",
    "eu.timepit" %% "refined-cats"       % "0.8.5",
    "eu.timepit" %% "refined-scalacheck" % "0.8.5",
    "org.scalacheck" %% "scalacheck" % "1.13.5" % "test",
    "org.scalatest" %% "scalatest" % "3.0.4" % "test"

パッケージオブジェクトには以下のようなコードを書いている。

package object ratio1 extends NonZeroIntModule with RationalModule {
  implicit class T2mapper[A](val t: (A, A)) extends AnyVal {
    def map[R](f: A => R): (R, R) = (f(t._1), f(t._2))
    def foldMap[R, B](f: A => R)(g: (R, R) => B): B = g.tupled(t map f)
  }
}

非ゼロ整数 --- NonZeroInt

まず分母の型の非ゼロ整数から。

refined でInt Refined Not[Equal[_0]]と書けるが、ここでは二つの型エイリアスに分けた。val one: NonZeroInt = refineMV[NonZero](1)のように書ける。

type NonZero    = Not[Equal[_0]]
type NonZeroInt = Int Refined NonZero

refined の中ではshapelessが活用されている。_0をW.`0`.Tとしても同じだが、_0は shapeless のNatで定義されていて、WはWitnessのエイリアスになっている。

プロパティ

NonZeroInt自体にも乗算の交換則、結合法則、単位元の法則が成立する。以下ようなプロパティとした。

property("Group: communitativity") = forAll(double(genNZInt)) { case (n1, n2) =>
  n1 * n2 === n2 * n1
}
property("Group: associativity") = forAll(triple(genNZInt)) { case (n1, n2, n3) =>
  (n1 * n2) * n3 === n1 * (n2 * n3)
}
property("Group: identity element") = forAll(genNZInt) { n1 =>
  one * n1 === one * n1 && one * n1 === n1
}

比較で使っている catsの===演算子は、refined-cats で提供されているEqインスタンスをインポートすれば使えるようになる。

プロダクトコード

上記プロパティを満たす乗算演算子*を以下のように定義した。NonZeroInt同士の乗算はNonZeroIntとなるので、〜.toOption.getして返している。

implicit class NonZeroIntOps(val nz: NonZeroInt) {
  def *(r: NonZeroInt): NonZeroInt =
    refineV[NonZero]((nz, r).foldMap(_.value)(_ * _)).toOption.get
}

上の方で少し触れたrefineMVは、マクロを用いてリテラルからNonZeroIntを生成して直接返すが、refineVはバリデートした値をEitherに入れて返す。

ちなみにRefType[Refined].unsafeWrap[Int, NonZero](x)のように書けば、Eitherを介さずNonZeroIntを作ることもできるが、0を持たせることもできてしまうためここでは避けた。

全体的には以下のようになる。

trait NonZeroIntModule {
  type NonZero    = Not[Equal[_0]]
  type NonZeroInt = Int Refined NonZero

  object NonZeroInt {
    val one: NonZeroInt = refineMV[NonZero](1)
  }
  implicit class NonZeroIntOps(val nz: NonZeroInt) {
    def *(r: NonZeroInt): NonZeroInt =
      refineV[NonZero]((nz, r).foldMap(_.value)(_ * _)).toOption.get
  }
}

分数 --- Rational

非ゼロ整数ができたので、これを分母とする分数を作る。手順としては、プロパティを少し書いて、対応するプロダクトコードを少し書くサイクルを、等値性、群、環、体の順に繰り返す。

等値性

1/2、2/4、12/24 など約分して等しいものは等しくなるようにする。

プロパティ

分子nと分母dの両方に0でない整数mをかけても、もとの分数と等しいことを以下のようなプロパティで表現する。

property("Rational: equality") = forAll(nzIntGen, intGen, nzIntGen) { (m, n, d) =>
  Rational(n, d) === Rational(n * m.value, d * m)
}

[-100, 100]の範囲で、intGen: Gen[Int]を scalacheck で定義。nzIntGen: Gen[NonZeroInt]は、refined-scalacheck で提供されるnumeric#chooseRefinedNumを使って実装した。

val intGen: Gen[Int] = chooseNum(-100, 100)
val nzIntGen: Gen[NonZeroInt] =
  chooseRefinedNum(refineMV[NonZero](-100), refineMV[NonZero](100))

プロダクトコード

以下のように、コンパニオンオブジェクトのapplyに分子分母が与えられた時点で約分している。

trait RationalModule {
  case class Rational(n: Int, d: NonZeroInt)
  object Rational {
    def apply(num: Int, denom: NonZeroInt): Rational =
      (new Rational(_, _)) tupled reduce(num, denom)

    def gcd(a: Int, b: Int): Int = if (b == 0) a else gcd(b, a % b)
    def reduce(n0: Int, nz: NonZeroInt): (Int, NonZeroInt) = {
      val f = (b: Int) => (n0, b).map(_ / gcd(n0, b))
      f(nz.value) match { case (n, d) => (n, refineV[NonZero](d).toOption.get) }
    }
  }
  implicit val eqRational: Eq[Rational] = (x, y) => x == y
}

約分して分母が0になることはないため、ここでも〜.toOption.getを使っているが、NonZeroIntの場合と同様にunsafeWrapは避けた。

加算と群

加算演算子+を実装する。加算に関しては群の公理が成り立つ。

プロパティ

交換則、結合法則、零元、反数からなる群のプロパティを追加。

property("Group: communitativity") = forAll(double(gen)) { case (r1, r2) =>
  r1 + r2 == r2 + r1
}
property("Group: associativity") = forAll(triple(gen)) { case (r1, r2, r3) =>
  (r1 + r2) + r3 == r1 + (r2 + r3)
}
property("Group: identity element") = forAll(gen) { r1 =>
  zero + r1 == zero + r1 && zero + r1 === r1
}
property("Group: inverse element") = forAll(gen) { r1 =>
  val inv = r1.negate
  r1 + inv === inv + r1 && inv + r1 === zero
}

gen: Gen[Rational]はcatsの Apply を使って
(intGen, nzIntGen).mapN(Rational(_, _))として生成する。

プロダクトコード

以下のように+演算子、反数のnegate、0元を追加。

case class Rational(n: Int, d: NonZeroInt) {
  def +(r: Rational): Rational = apply(r.d.value * n + d.value * r.n, d * r.d)
  def negate: Rational = apply(n * (-1), d)
}
object Rational {
  val zero: Rational = apply(0, ratio1.one)
  //...
}

乗算と環

交換則、結合法則、単位元、分配法則からなる環のプロパティを追加。群の「反数」に対応する「逆数」は、次の「体」の実装まで待つことになるが、分配法則はここで成立する。

プロパティ

property("Ring: communitativity") = forAll(double(gen)) { case (r1, r2) =>
  r1 * r2 == r2 * r1
}
property("Ring: associativity") = forAll(triple(gen)) { case (r1, r2, r3) =>
  (r1 * r2) * r3 == r1 * (r2 * r3)
}
property("Ring: unity") = forAll(gen) { r1 =>
  one * r1 === one * r1 && one * r1 === r1
}
property("Ring: distributivity(1)") = forAll(triple(gen)) { case (r1, r2, r3) =>
  r1 * (r2 + r3) == r1 * r2 + r1 * r3
}
property("Ring: distributivity(2)") = forAll(triple(gen)) { case (r1, r2, r3) =>
  (r1 + r2) * r3 == r1 * r3 + r2 * r3
}

プロダクトコード

Rational に乗算演算子*を追加。

def *(r: Rational): Rational = apply(n * r.n, d * r.d)

逆数と体

体の要素として「逆数」を実装する。やっと分数=有理数らしくなるが、逆数をもつのは「０以外の要素〜」と条件がつくので、これまでと少しちがってくる。ここでは逆数がない場合の表現にEitherを使った。

プロパティ

property("Field: inverse element") = forAll(gen.suchThat(_ =!= zero)) { r =>
  val inv = r.invert.toOption.get
  r * inv === inv * r && inv * r === one
}
property("Field: inverse zero has no value") = Prop {
  zero.invert.isLeft
}

零元の場合とそうでない場合とでプロパティをわけ、前者にはPropを使った。

プロダクトコード

refineVからのmapでEither[String, Rational]を返している。

case class Rational(n: Int, d: NonZeroInt) {
  def invert: MaybeRational = refineV[NonZero](n).map(Rational(d.value, _))
  //...
} 
object Rational {
  type MaybeRational = Either[String, Rational]
  //...
}

零元の逆数を REPL でためすと以下のようになる。

scala> Rational.zero.invert
res1: ratio1.Rational.MaybeRational = Left(Predicate (0 == 0) did not fail.)

「述語0==0が失敗しなかった」というメッセージがやや分かりにくいが、内部で使う情報としては十分かもしれない。

ちなみにInt Refined Or[Negative, Positive]だと以下のようになる。

Left(Both predicates of ((0 < 0) || (0 > 0)) failed. Left: Predicate failed: (0 < 0). Right: Predicate failed: (0 > 0).)

テストログ

IntelliJ上のテスト実行結果は以下。

+ NonZeroInt.Group: communitativity: OK, passed 100 tests.
+ NonZeroInt.Group: associativity: OK, passed 100 tests.
+ NonZeroInt.Group: identity element: OK, passed 100 tests.

Process finished with exit code 0

+ Rational.Rational: equality: OK, passed 100 tests.
+ Rational.Group: communitativity: OK, passed 100 tests.
+ Rational.Group: associativity: OK, passed 100 tests.
+ Rational.Group: identity element: OK, passed 100 tests.
+ Rational.Group: inverse element: OK, passed 100 tests.
+ Rational.Ring: communitativity: OK, passed 100 tests.
+ Rational.Ring: associativity: OK, passed 100 tests.
+ Rational.Ring: unity: OK, passed 100 tests.
+ Rational.Ring: associativity(1): OK, passed 100 tests.
+ Rational.Ring: associativity(2): OK, passed 100 tests.
+ Rational.Field: inverse element: OK, passed 100 tests.
+ Rational.Field: inverse zero has no value: OK, proved property.

Process finished with exit code 0

逆数ができたので、- /の追加、MaybeRationalを扱うための演算子オーバーロードと若干の implicit クラスの追加で、連続的な四則演算が書けるようになるが、主旨から外れるので割愛する。

ソース

• gist: property(redefine+cats+scalacheck)
• gist: product_code(redefine+cats+scalacheck)

所感

• 複雑なドメインでも、自然と不変条件をキープした形でコードが書けそう。ドメインロジックの中にバリデーションや例外送出があると「関心事」の混在で扱いにくくなりがちだけど、型としてコンパイル時に前提を成立させられると色々やりやすそうな気はする。
• 単一の値にまつわるルール、制約、不変条件の置き場所はある程度（型で表現できる限りは）まとめられそう。
• リファインされた値から別のリファインされた値を作るときは、上述のように~.toOption.getするような形で一瞬アンセーフになるが、かなり局所化できてはいる。
• テストでは discipline も検討したが、非ゼロ整数の積算で"monoid law"を使おうとした時などに、合成のところですぐに桁あふれしてしまうので（これはこれで正しいが）、小さく試してみたい今回のような目的には厳しすぎるので避けた。