この記事は Scala Advent Calendar 2021 の 20 日目の記事です．

はじめに

2021 年 5 月にリリースされた Scala 3 には，型システムや構文に大幅な改善が行われ，多くの新機能が追加されています．

今回はその中で，型システムにひっそりと追加された新機能である「カインド多相 (kind polymorphism)」について見ていきます．
この新機能が使われる場面は限られていますが，型システムの表現能力の向上に貢献している，型理論的には非常に面白い機能です．

カインドとは

まずはカインド (kind) のおさらいから．
そもそもカインドとは，型の型ともいうべき概念で，型の抽象化のレベルを表す概念です．
カインドの概念自体は Scala 2 の時代からありました．

Scala における型のカインドの例をいくつかみてみます．

型	カインド
`Boolean`	`*`
`Int`	`*`
`Option`	`* -> *`
`List`	`* -> *`
`Either`	`* -> * -> *`
`Map`	`* -> * -> *`
`List[Int]`	`*`
`Either[Boolean, Int]`	`*`
`({type T[A] = Either[A, Int]})#T`	`* -> *`

記号 * は，抽象化されていない，いわゆる普通の型を表します．

Option や List は，型パラメータを 1 つとる型なので，カインドは * -> * です．
Either や Map は，型パラメータを 2 つとる型なので，カインドは * -> * -> * です．

REPL の :kind コマンドでカインドを確認することもできます．
(Scala 3 から :kind コマンドがなくなっているので，Scala 2 でやってます...．)

% scala
Welcome to Scala 2.13.7 (OpenJDK 64-Bit Server VM, Java 1.8.0_312).
Type in expressions for evaluation. Or try :help.

scala> :k -v Int
Int's kind is A
*
This is a proper type.

scala> :k -v Option
Option's kind is F[+A]
* -(+)-> *
This is a type constructor: a 1st-order-kinded type.

高カインド型

Scala では，型パラメタをもつ型を型パラメタとする型を定義することもできます．
こういう型のことを，高カインド型 (higher-kinded type) とよびます．
これも Scala 2 の時代からあった概念です．

高階のカインドをもつ型の代表的な例として，以下の Functor のような型があります．

trait Functor[F[_]] {
  def map[A, B](fa: F[A])(f: A => B): F[B]
}

Functor 型のカインドは (* -> *) -> * です．
実際に REPL で確かめてみます．

scala> trait Functor[F[_]] {
     |   def map[A, B](fa: F[A])(f: A => B): F[B]
     | }
trait Functor

scala> :k -v Functor
Functor's kind is X[F[A]]
(* -> *) -> *
This is a type constructor that takes type constructor(s): a higher-kinded type.

Option 型のカインド * -> * のような 1 段階の抽象化を 1 階とよび，今回の Functor 型の (* -> *) -> * のような 2 段階の抽象化を 2 階とよびます．
一般的には，2 階以上のカインドを高階のカインドとよびます．

型	カインド	階数
`Option`	`* -> *`	1 階
`Either`	`* -> * -> *`	1 階
`Functor`	`(* -> ) -> `	2 階

カインド多相

ここから本題である，Scala 3 で導入されたカインド多相 (kind polymorphism) について見ていきます．

Language Rerefence には，以下のページに説明があります．

Kind Polymorphism - Scala 3 Language Rerefence

この機能の導入につながったプロポーザルは，以下のページに見つかります．

Proposal to add kind polymorphism to the language

カインド多相は，型パラメータのカインドの制約をなくす機能です．
Scala において，これまで型パラメータには Int や Option[Int] のような抽象化されていない型 (0 階のカインドの型) しか許されていませんでしたが，カインド多相を有効にする場合，型パラメータに Option や Functor など抽象化された型 (1 階以上のカインドの型) を指定できるようになります．

Launguage Reference にある例を題材に，具体的なケースで考えてみます．
次のような，型パラメータ T をもつメソッド f を考えます．

def f[T] = ...

このメソッド f のパラメータ T に入る型は，Int や List[Int] のような抽象化されていない型のみです．
List のような，1 階以上のカインドをもつ型を入れることはできません．

f[Int]             // OK
f[List]            // Error
f[Map]             // Error
f[[X] =>> String]  // Error

一方，カインド多相を用いることで，こうしたカインドに基づく制約を撤廃できます．
カインド多相を用いるには，次のように型パラメータの上限境界 (upper bound) として AnyKind を指定します．

def f[T <: AnyKind] = ...

これにより，型パラメータはカインドの制約から解放され，自由なカインドの型を指定できるようになります．

f[Int]             // OK
f[List]            // OK
f[Map]             // OK
f[[X] =>> String]  // OK

Any と AnyKind の関係

Scala 3 で導入された AnyKind は，あらゆるカインドの型を包含する概念であり，通常のデータ型を表す Any よりも真に広い範囲を表します．

\mathtt{Any} \subset \mathtt{AnyKind}

Scala 2 における Any は，Scala のすべてのデータ型を包含する，頂点に位置する型 (トップ型とよばれる) としての役割を担ってきました．
Scala 3 では，Any は引き続きすべての通常のデータ型を表しますが，その上位に位置する AnyKind が導入されたことで，Any はトップ型の座を奪われています．

トップ型が変わったことで，型パラメータで上限境界を省略した場合の考え方が Scala 2 と Scala 3 で異なるため，注意が必要です．

Scala 2 では，上限境界を指定せずに def f[T] と書いたときは，トップ型である Any が上限境界とみなされ def f[T <: Any] を意味していました．

Scala 3 では，上限境界を指定せずに def f[T] と書いたときは，トップ型である AnyKind ではなく従来通り Any が上限境界となり，def f[T <: Any] を意味します．
一方で， def f[T <: AnyKind] と書くことで，型パラメータ T のとりうる範囲が Any という制約を超えることができ，真のトップ型である AnyKind が上限境界になります．

Type 型の事例

Scala 3 でカインド多相が実際に使われている事例として，scala.quoted.Type 型があります．
Type はマクロで登場する型であり，次のように定義されています．

abstract class Type[T <: AnyKind]:
  type Underlying = T

少し脱線してメタプログラミングの話になってしまいますが，メタプログラミングで型情報を扱う際に Type 型が使われます．
例えば次のようなプログラムで Type 型を試してみることができます．

object Macro:
  inline def f[T](inline expr: T) =
    ${ impl('expr) }

  def impl[T: Type](expr: Expr[T])(using Quotes): Expr[T] =
    import quotes.reflect.*
    println(Type.show)
    println(expr.asTerm.show)
    println()
    expr

object Main:
  // value
  Macro.f { 1 + 2 }
  Macro.f { Option("a") }
  Macro.f { (x: Int) => x + x }

  // tycon
  Macro.f { Boolean }
  Macro.f { Option }
  Macro.f { Either }

実行例は次の通りです．コンパイル時に計算結果が出力されます．

% scalac Macro.scala Main.scala
scala.Int
3

scala.Option[java.lang.String]
scala.Option.apply[java.lang.String]("a")

scala.Function1[scala.Int, scala.Int]
((x: scala.Int) => x.+(x))

scala.Boolean.type
scala.Boolean

scala.Option.type
scala.Option

scala.util.Either.type
scala.Either

Girard のパラドックスの話

Haskell では GHC 7.4 から -XPolyKinds というオプションが追加されていて，このオプションでカインド多相を有効にできるようになっています．

Section 7.8. Kind polymorphism and promotion - The Glorious Glasgow Haskell Compilation System User's Guide, Version 7.4.1

この機能が導入された当時の会議録がこれです．

B. A. Yorgey, et al. Giving Haskell a Promotion (TLDI 2012)

会議録を見るとわかるように，こうしたカインド多相性は Girard のパラドックスの誘因になり，型システムのある種の健全性を壊す結果につながります．
型システムベースの定理証明系などの場合には，証明の健全性に関わるため，こうしたことが問題になります．

Scala の場合，カインド多相のプロポーザルでも Girard のパラドックスのことが言及されていましたが，Scala としてはこれを問題視しない立場をとっているようです．
Scala の型システムは定理証明系を目指しているわけではないですし，そうした潜在的な問題よりも享受できる恩恵が大きいことから，Scala 3 でカインド多相の導入を断行したものと思われます．

まとめ

Scala 3 で導入されたカインド多相について見てきました．
こういう自由度の高い機能は，型システムの表現能力を高める一方で型システムの健全性や決定可能性を損なう可能性のある両刀の剣ですが，Scala はその辺りのバランスをうまく取ってやっていると思います．

参考文献