6
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 1 year has passed since last update.

ScalaAdvent Calendar 2023

Day 3

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

Last updated at Posted at 2023-12-03

再帰型(英: recursive type)とは、型の定義中にそれ自身の型が出現するような再帰する型のこと。

出典: 再帰データ型 - Wikipedia

Scala で一般の equirecursive type を作る方法を述べる。特に、Scala 3 の match type を利用すると equirecursive type がキャスト無しで実現できることを述べる。

再帰データ型

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

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

type ListInt = List[Int]

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

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

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

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

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

と書けばよい。Scala の標準ライブラリでは Cons:: という名前で定義されており、: で終わる識別子は中値演算子として利用したときに右結合的になると規定されているから、上の Cons(1, ...) という式は

1 :: 2 :: 3 :: 4 :: Nil

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

再帰型

さて、前節では ListInt 型の値を考えてみたが、この構造は Scala 3 のタプル型 (普通のタプル型 + 空タプルを表す EmptyTuple) を利用すれば次のようにも表現できそうである。

(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 カクテル

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

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

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

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 3
enum ListIntTuple:
  case NilInt(empty: EmptyTuple) extends ListIntTuple
  case Cons(consed: (Int, ListIntTuple)) extends ListIntTuple

しかし、例えば EmptyTupleListIntTuple の部分型ではない。$\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 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.
}

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

一方、等式 ($=$) で結ぶのを諦めて同型性 ($\cong$) 3を見てみると、似たような関係を 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})$$であることがわかる。

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

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

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

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

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

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 で実装することができる。次のように実装すればよい 9 (Scastie)。

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]]
}

まとめ

  • 型方程式 $\alpha = \tau$ ($\tau$ は $\alpha$ を含んでいる可能性がある) を満たす型 $\alpha$ のことを等再帰型 (equirecursive type) と呼ぶ。
  • classenum 等の仕組みでは一般の等再帰型を作ることはできないが、 Scala 3 の match type を使うとできる。
  • 関連型 Solution と、=:= を用いて Solution の再帰性を証明する値を trait で提供することで、等再帰型の実装を隠蔽することができる。
  1. 実際の定義 では、i) Scala 2 でも List が使えるように sealed abstract classfinal case class + case object の組み合わせで定義されており ii) List は様々な親 trait を持ち iii) NilList[Nothing] を継承する case object になっている。

  2. case object EmptyTuplescala.Tuplescala.Producttrait EqualsAnyRef しか親 trait に持たない。Scala の enumclass は公称的 (nominal) な型を定義し、新しく定義した型は、その型を明示的に extends する classNothing しかサブタイプのクラスを持たないので、EmptyTuple が新しく定義した型のサブタイプになることはない。

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

  4. https://web.archive.org/web/20201203022142/https://www.cs.cornell.edu/courses/cs4110/2012fa/lectures/lecture27.pdf

  5. 一般的な呼び方ではない。日本語文献では「同値再帰型」と呼ばれがちなようだが、「同値」というのが "equal value" ではなく "equivalent" と取れてしまい紛らわしいので、この呼び名は本稿では避ける。

  6. これら二つの概念は相互排他的ではない。実際、型はそれ自身に同型であるから、等再帰型は同型再帰型であると言える。また、上で紹介したような「再帰データ型」は、満たしている等式が異なるだけで等再帰型である可能性もある。例えば、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{]}} \}$ を満たす等再帰型であるとも言える (公称性が交差型を使うことで記述できている)。

  7. それ以上型を適用できない型。proper type とも。

  8. この機構は、Scalaz の newtype pattern を実現する機構である Tag の仕組みとその利点を解説した記事 Filaed Experiments: The High Cost of AnyVal subclasses... から着想を得た。

  9. Scala 3 の Match Types で再帰型を表現する.Defining a type in a recursive way in Dotty - Question - Scala Users 等を参考にした。

6
0
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
6
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?