Scala 3 で一般の再帰型を作る

> 再帰型（英: recursive type）とは、型の定義中にそれ自身の型が出現するような再帰する型のこと。
> 
> 出典: [再帰データ型 - Wikipedia](https://ja.wikipedia.org/wiki/%E5%86%8D%E5%B8%B0%E3%83%87%E3%83%BC%E3%82%BF%E5%9E%8B)

Scala で一般の equirecursive type を作る方法を述べる。特に、[Scala 3 の match type](https://docs.scala-lang.org/scala3/reference/new-types/match-types.html) を利用すると equirecursive type がキャスト無しで実現できることを述べる。

## 再帰データ型

まず、**データ型 `D` が再帰データ型である**とは、 `D` の定義が `D` に言及することである。

Scala ではリスト構造を表現するために [`scala.collection.immutable.List`](https://www.scala-lang.org/api/2.13.3/scala/collection/immutable/List.html) という単方向連結リスト構造をよく使う。`List` は実際には共変型引数 `A` を持つ `List[+A]` として定義されているが、簡単のため `A = Int` と特殊化し、`List[Int]` のことを考えてみることにする。
```scala
type ListInt = List[Int]
```

`ListInt` は、非常に大雑把に言えば [^recursive-type-1] 次のような `enum` で定義されている。

```Scala
// Scala 3
enum ListInt:
  case NilInt extends ListInt
  case Cons(head: Int, tail: ListInt) extends ListInt
```

[^recursive-type-1]: [実際の定義](https://github.com/scala/scala/blob/v2.13.3/src/library/scala/collection/immutable/List.scala#L79) では、**i)** Scala 2 でも `List` が使えるように `sealed abstract class` と `final case class ` + `case object` の組み合わせで定義されており **ii)** `List` は様々な親 trait を持ち **iii)** `Nil` は `List[Nothing]` を継承する `case object` になっている。

つまり、`ListInt` の値は `NilInt` であるか `Cons` であるかのどちらかであると宣言されている。ここで、 `case Cons` の定義は `ListInt` に言及している。`ListInt` というデータ型がどのようなものであるかの定義のために `ListInt` が言及されているので、`List[A]` は再帰データ型である。

`ListInt` の値は `Nil` / `Cons` の呼び出しをネストすることで構築される。例えば、 `[1, 2, 3, 4]` のようなリスト構造を `ListInt` で表現したければ、

```scala
Cons(1, Cons(2, Cons(3, Cons(4, Nil))))
```

と書けばよい。Scala の標準ライブラリでは `Cons` は `::` という名前で定義されており、[`:` で終わる識別子は中値演算子として利用したときに右結合的になると規定されている](https://www.scala-lang.org/files/archive/spec/2.13/06-expressions.html#infix-operations)から、上の `Cons(1, ...)` という式は

```scala
1 :: 2 :: 3 :: 4 :: Nil
```

と書けるようになっている。

## 再帰型

さて、前節では `ListInt` 型の値を考えてみたが、この構造は Scala 3 のタプル型 (普通のタプル型 + 空タプルを表す [`EmptyTuple`](https://www.scala-lang.org/api/3.2.2/scala/EmptyTuple$.html)) を利用すれば次のようにも表現できそうである。

```scala
(1, (2, (3, (4, EmptyTuple)))): (Int, (Int, (Int, (Int, EmptyTuple.type))))
```

しかし、「`Int` のリスト」であるからには、`(Int, (Int, (Int, (Int, EmptyTuple.type))))` という「4要素のリスト」のみでなく、どのような「深さ」のタプルでもすべて「`Int` のリスト」として扱えて欲しい。この事情を表現するには、 Scala 3 の和型 (union type) が利用できそうである。

> Scala 3では、`A | B`と書くことで型と型をひっつけて、「そのどっちかの型」を表現する型を簡単に書けるようになった。
> [Scala3のUnion Types / Intersection Typesを試してみた - Lambda カクテル](https://blog.3qe.us/entry/2022/11/29/224250)

そこで、`TupleIntList` を次のように定義してみる。

```Scala
// 再帰的な型定義。
// EmptyTuple はもちろん、 (Int, EmptyTuple)、(Int, (Int, EmptyTuple)) …
// などがすべて TupleIntList の部分型であってほしい。
type TupleIntList = EmptyTuple | (Int, TupleIntList)
```

これは、「型エイリアスは再帰的であってはならない」としてコンパイラに拒否される。

```scala
type TupleIntList = EmptyTuple | (Int, TupleIntList)
//   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
//   illegal cyclic type reference: alias EmptyTuple | (Int, TupleIntList) of ... (caught cyclic reference) ... refers back to the type itself
```

もし `TupleIntList` が再帰的な型エイリアスとして定義できていたら、 `TupleIntList` は、型方程式 $\alpha = ()\ \vert\ (\mathrm{Int}, \alpha)$ の解になっていたはずだ。$\alpha = ()\ \vert\ (\mathrm{Int}, \alpha)$ のような、左辺の型変数が右辺に現れているような (「再帰的な」) 型方程式を満たす型のことを**再帰型**と呼ぶ。

## 再帰データ型では満たせない型方程式 α = τ がある

前節では、型方程式 $\alpha = ()\ \vert\ (\mathrm{Int}, \alpha)$ の解 $\alpha$ が `Int` 型の `List` を表現できる型であることと、単純な型エイリアスでは解 $\alpha$ を構築できないことを見た。では、再帰的な `enum` は $\alpha = ()\ \vert\ (\mathrm{Int}, \alpha)$ の解になり得るだろうか？

まず、`IntList` の定義を `EmptyTuple` とタプル型を明示的に利用した再帰データ型 `ListIntTuple` へと書き直してみる。

```Scala
// Scala 3
enum ListIntTuple:
  case NilInt(empty: EmptyTuple) extends ListIntTuple
  case Cons(consed: (Int, ListIntTuple)) extends ListIntTuple
```

しかし、例えば `EmptyTuple` は `ListIntTuple` の部分型ではない。$\alpha = ()\ \vert\ (\mathrm{Int}, \alpha)$ なら、和型の定義から $() \lt: \alpha$ であるはずであるから、$\mathrm{ListIntTuple} \neq ()\ \vert\ (\mathrm{Int}, \mathrm{ListIntTuple})$ である。そもそも、Scala 3 の型付け規則では $\mathrm{ListIntTuple} = \mathrm{\text{ListIntTuple.NilInt}}\ \vert\ \mathrm{\text{ListIntTuple.Cons}}$ すら成り立たない。

```scala
// Scala 3
enum ListIntTuple:
  case NilInt(empty: EmptyTuple) extends ListIntTuple
  case Cons(consed: (Int, ListIntTuple)) extends ListIntTuple

def main(args: Array[String]): Unit = {
  summon[ListIntTuple =:= (ListIntTuple.NilInt | ListIntTuple.Cons)]
//^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
// Cannot prove that ListIntTuple =:= ListIntTuple.NilInt | ListIntTuple.Cons.
}
```

一般に、どのような (標準ライブラリの外で) `class` や `enum` を新しく定義したとしても、それが `EmptyTuple` をサブタイプとして持つことはない [^insoluble-rec-type-1]。よって、$\mathrm{ListIntTuple} = ()\ \vert\ (\mathrm{Int}, \mathrm{ListIntTuple})$ は `class` や `enum` を解として持たない。特に、**再帰データ型の範囲では解けない、$\alpha = \tau$** ($\tau$ は $\alpha$ を含むかもしれない型) **の形をした型方程式が存在する**。

[^insoluble-rec-type-1]: `case object EmptyTuple` は `scala.Tuple`、`scala.Product`、`trait Equals`、`AnyRef` しか親 trait に持たない。Scala の `enum` や `class` は公称的 (nominal) な型を定義し、新しく定義した型は、その型を明示的に `extends` する `class` か `Nothing` しかサブタイプのクラスを持たないので、`EmptyTuple` が新しく定義した型のサブタイプになることはない。

一方、等式 ($=$) で結ぶのを諦めて同型性 ($\cong$) [^insoluble-rec-type-2]を見てみると、似たような関係を `ListIntTuple` が満たしていることが分かる。まず$$\mathrm{ListIntTuple} \cong \mathrm{\text{ListIntTuple.NilInt}}\ \vert\ \mathrm{\text{ListIntTuple.Cons}}$$で、$$\mathrm{\text{ListIntTuple.NilInt}} \cong \(\)$$$$\mathrm{\text{ListIntTuple.Cons}} \cong \(\mathrm{Int},  \mathrm{\text{ListIntTuple}}\)$$ の二つも言えるから、$$\mathrm{ListIntTuple} \cong ()\ \vert\ (\mathrm{Int}, \mathrm{ListIntTuple})$$であることがわかる。

[^insoluble-rec-type-2]: 「情報量を一切落とすことが無く相互変換できる」こと。より形式的には、型 `A`、`B` が同型であるとは、「関数 `f: A => B` と `g: B => A` が存在して、どのような `a: A` と `b: B` に対しても `g(f(a)) = a` かつ `f(g(b)) = b` が成り立つ」として定義される。型 $A$ と $B$ が同型であることを $A \cong B$ と書く。

`ListIntTuple` のような、**再帰的な同型関係を成り立たせる型のことを isorecursive type (同型再帰型) と呼ぶ**[^insoluble-rec-type-3]。一方、**再帰的な等式を成り立たせる型のことは equirecursive type (等再帰型[^insoluble-rec-type-4]) と呼んで**区別[^insoluble-rec-type-5]する。

[^insoluble-rec-type-3]: https://web.archive.org/web/20201203022142/https://www.cs.cornell.edu/courses/cs4110/2012fa/lectures/lecture27.pdf
[^insoluble-rec-type-4]: 一般的な呼び方ではない。日本語文献では「同値再帰型」と呼ばれがちなようだが、「同値」というのが "equal value" ではなく "equivalent" と取れてしまい紛らわしいので、この呼び名は本稿では避ける。

[^insoluble-rec-type-5]: これら二つの概念は相互排他的ではない。実際、型はそれ自身に同型であるから、等再帰型は同型再帰型であると言える。また、上で紹介したような「再帰データ型」は、満たしている等式が異なるだけで等再帰型である可能性もある。例えば、`trait RecursiveList[A] { val head: A; val tail: Option[RecursiveList[A]] }` という「リスト」の定義は、Scala 3 の交差型を使った型方程式 $\alpha = \alpha\ \\&\ \\{ \mathrm{\text{val head: A; val tail: Option[}} \alpha \mathrm{\text{]}} \\}$ を[満たす](https://scastie.scala-lang.org/BakaSyV6TzSzkIz4Tu1JVA)等再帰型であるとも言える (公称性が交差型を使うことで記述できている)。

## 等再帰型を提供するインターフェース

(二階の) 型コンストラクタ `F[_]` とは、型`A`を適用することで一階の型[^equirecursive-provider-1]が得られるようなものであった。例えば `List` や `Option` 等はその一例である。さて、型方程式 $\alpha = \tau$ を満たすような$\alpha$ を等再帰型と呼ぶのであった。$\tau$ は $\alpha$ を言及している可能性がある一階の型だから、適当な型コンストラクタ $F$ について $\alpha = F(\alpha)$ となるはずである。よって、$\alpha = \tau$ の形の型方程式は、型コンストラクタ $F(-)$ を一つ持ってくると記述できるはずである。

[^equirecursive-provider-1]: それ以上型を適用できない型。proper type とも。

さて、Scala には generalized type constraints ([説明している Qiita 記事](https://qiita.com/xfan/items/655f61726c16f149ba0a)) が存在している。Generalized type constrait の一種である [`=:=[_, _]`](https://www.scala-lang.org/api/current/scala/$eq$colon$eq.html) は、二つの型 (具体的な型でなくてもよく、型変数を含んでいても良い) の等価性を値レベルに送り出すものであり、「`=:=[A, B]`の値があるということは `A` と `B` が型として (つまり、Scala コンパイラが等価性を証明できる形として、どこか過去のタイミングで) **等しかった**はずだ」という保証を与えるものである。実際、`=:=[A, B]` の値がスコープ内にある時、Scalaコンパイラに `A` と `B` をまったく同じ型であると考えるよう指示することが[できる](https://scastie.scala-lang.org/xq0sNrM6RW2MKrHalabLEQ)。

$F$ を型コンストラクタであるとする。もし $X$ が $F(X) = X$ を満たす型ならば、`=:=[X, F[X]]` の値が作成できるはずである。一般に、「$F(X) = X$ という型方程式の解 $X$」をパス依存型として提供する次のようなインターフェースが書ける[^equirecursive-provider-2]。

[^equirecursive-provider-2]: この機構は、Scalaz の newtype pattern を実現する機構である `Tag` の仕組みとその利点を解説した記事 [Filaed Experiments: The High Cost of AnyVal subclasses...](https://failex.blogspot.com/2017/04/the-high-cost-of-anyval-subclasses.html) から着想を得た。

```scala
trait EquirecursiveType[F[_]] {
  type Solution
  def evidence: Solution =:= F[Solution]
}
```

`t: EquirecursiveType[F]` があったとき、`t.evidence: t.Solution =:= F[t.Solution]` となる。この `trait EquirecursiveType` を介することで、利用側は `t.Solution` がどのように構成されたかを**知ることなく**、`t.Solution` が $F(X) = X$ の解であるという事実 (`t.evidence`) にのみ基づいてコードを書くことを強制される。

したがって、`EquirecursiveType[F]` の値を生成することができれば、我々は (`F` で定義される) equirecursive type を記述できたことになる。

## Scala 3 での `EquirecursiveType[F]` の実装

Scala 3 では、任意の `F` についての `EquirecursiveType[F]` を `match` type で実装することができる。次のように実装すればよい [^scala3-equirecursive-1] ([Scastie](https://scastie.scala-lang.org/mBvPlySRSOKR1TQzobNghg))。

```scala
type Rec[F[_], Dummy] = Dummy match {
  // case _ => のみだと type alias として扱われてしまうので、
  //   Dummy = false という特別ケースを追加する。
  // ここで false を選んだことは本質的ではないし、
  //   マッチ結果は false でなくともなんでも良い。
  case false => false
  case _ => F[Rec[F, Dummy]]
}

// この `: EquirecursiveType[F]` は外してはならない。
// この型注釈には、パス依存型の実装を外部から見えなくして、
// `=:=` を使わないと `Solution` が `F[Solution]` に展開されないように制御する役目がある。
def equirecursiveTypeImpl[F[_]]: EquirecursiveType[F] = new EquirecursiveType[F] {
  type Solution = Rec[F, true]
  // Solution と F[Solution] はコンパイラからすると同じ型なので、
  // =:= の summon が通る
  def evidence = summon[Solution =:= F[Solution]]
}
```

[^scala3-equirecursive-1]: [Scala 3 の Match Types で再帰型を表現する.](https://zenn.dev/110416/articles/9f6996c2f543a1) や [Defining a type in a recursive way in Dotty - Question - Scala Users](https://users.scala-lang.org/t/defining-a-type-in-a-recursive-way-in-dotty/6798/8) 等を参考にした。

## まとめ

- 型方程式 $\alpha = \tau$ ($\tau$ は $\alpha$ を含んでいる可能性がある) を満たす型 $\alpha$ のことを等再帰型 (equirecursive type) と呼ぶ。
- `class` や `enum` 等の仕組みでは一般の等再帰型を作ることはできないが、 Scala 3 の `match` type を使うとできる。
- 関連型 `Solution` と、`=:=` を用いて `Solution` の再帰性を証明する値を `trait` で提供することで、等再帰型の実装を隠蔽することができる。