kmizuの日記

プログラミングや形式言語に関係のあることを書いたり書かなかったり。

Scala 3で型レベル自然数をやってみたらすごく簡単になってた

Scala 3、正式リリースされてからそこそこ経ってますが皆さん使ってますか?実は自分は、主にIntellij IDEAのScala 3対応に不安もあってScala 2.13系列をずっと使い続けて来たのですが、最近はScala 3対応も進んできたようなので乗り換えを始めることにしました。で、手始めにということで型レベル自然数(型レベルペアノ数)を定義してみることにしました。

型レベル自然数は読んで字の如くで、型のレベルで自然数エンコーディングしちゃおうって技です。依存型のある言語なら最初からあるので、わざわざ型レベル自然数とか大仰な言い方しなくてもいいのですが、それはそれとして論より証拠。早速、Scala 3で型レベル自然数を定義してみます。

enum Nat {
  case Zero
  case Succ[A <: Nat](v: A)
}

定義はこれだけです。簡単ですね。Scala 2だと

sealed trait Nat
object Nat {
  case object Zero extends Nat
  case class Succ[A <: Nat](V: A) extends Nat
}

のように書かなければいけなかったのでとっても面倒でした。さてさて、とりあえずこれで型レベル自然数の定義はできたのですが、よく使う一桁の自然数は別名定義しておきたいですというわけで、次にこんなん書きます:

type _0 = Zero.type
type _1 = Succ[_0]
type _2 = Succ[_1]
type _3 = Succ[_2]
type _4 = Succ[_3]
type _5 = Succ[_4]
type _6 = Succ[_5]
type _7 = Succ[_6]
type _8 = Succ[_7]
type _9 = Succ[_8]

この辺はScala 2時代と変わらず面倒くさいです(もしお手軽に型エイリアスを大量生成できる技知ってる人いれば教えてください)。で、この次が本題なのですが、型レベルで自然数を表すからには当然加算や減算などの演算を定義したいですよね。これがScala 3になってかなり楽になりました。たとえば、足し算を表す型コンストラクPlusは次のようにかけます。

type Plus[A <: Nat, B <: Nat] = (A, B) match {
  case (x, Zero.type) => x // 右辺が0なら左辺の型を返す
  case (x, Succ[y]) =>  Succ[Plus[x, y]] // そうでなければxとyをPlusした型をSuccする
}

ここでは、

  • 型の別名付け機能: type Plus[...] = ...
  • 型のパターンマッチ: 型の別名定義内で型へのパターンマッチをできる

という二つの機能を使っていますが、再帰的な足し算の定義をそのまま素直に書き下せています。Scala 2だと型パターンマッチも型の別名定義中の「型の再帰」も素直にかけませんでしたから、この快適さにビックリです!

続いて掛け算(Multiply)を定義しましょう。掛け算は当然ながら足し算を使って定義できるので、以下のような感じでしょうか。

type Multiply[A <: Nat, B <: Nat] = (A, B) match {
  case (_, Zero.type) |  (Zero.type, _) => Zero.type // 両辺の片方が0なら0
  case (x, `_1`) | case (`_1`, x) => x // 両辺の片方が1なら1
  case (x, Succ[z])  =>  Plus[x, Multiply[x,y]] // y >= 2のとき、x  * y  = x + (x * (y - 1))
}

この型レベル演算がうまく行っているか確かめるためにmainメソッドをつけてみましょう。Scala 3ではクラスがなくてmainメソッドだけのプログラムも許されるようになりました(明らかにKotlilnを意識した仕様変更ですね)。

def main(args: Array[String]): Unit = {
  val one: _4 = null.asInstanceOf[Plus[_2, _2]]
  val six: _6 = null.asInstanceOf[Multiply[_2, _3]]
  val nine: _9 = null.asInstanceOf[Multiply[_3, _3]]
  println("Hello")
}

これらのプログラムにNat.scalaという名前をつけて保存し、

scala Nat.scala

としてみれば問題なくHelloが表示されます。さて、上記ではone, six, nineの型を正しく指定しましたが、次のように間違った型を指定するとどうなるでしょうか。

val wrong: _2 = null.asInstanceOf[Multiply[_4, _2]]

これを含めたプログラムをコンパイルすると次のようになります。

-- [E007] Type Mismatch Error: /home/mizushima/repo/scala-nats/Nat.scala:36:35 ---------------------------------------------
36 |  val wrong: _2 = null.asInstanceOf[Multiply[_4, _2]]
   |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |                  Found:    Nat.Succ[Nat.Succ[Nat.Succ[Nat.Succ[Nat.Succ[_3]]]]]
   |                  Required: _2
   |
   | longer explanation available when compiling with `-explain`
1 error found
Errors encountered during compilation

要求されていた(Required)な型は_2だけど、実際にはNat.Succ[Nat.Succ[Nat.Succ[Nat.Succ[Nat.Succ[_3]]]]] = _8 だよというエラーですね。というわけでScala 3になってこういうお遊びもやりやすくなたのでした。