[解決済み] Scala型プログラミングリソース

質問

によると この質問 によると、Scalaの型システムは チューリング完全 . 新規参入者が型レベルプログラミングの力を活用するために、どのようなリソースが利用できますか？

私がこれまでに見つけたリソースは以下の通りです。

• Daniel Spiewak の スカラの国の高い魔法使い
• Apocalisp の Scala における型レベルプログラミング
• イェスパーの HList

これらのリソースは素晴らしいものですが、基本的なことが欠けているように感じ、その上に強固な基盤を築いていません。たとえば、型定義の紹介はどこにあるのでしょうか。型に対してどのような操作を行うことができるのでしょうか。

何か良い入門資料はないでしょうか？

どのように解決するのですか？

概要

型レベルプログラミングは、従来の値レベルプログラミングと多くの類似点がある。しかし、実行時に計算が行われる値レベルのプログラミングと異なり、型レベルのプログラミングでは、コンパイル時に計算が行われる。ここでは、値レベルのプログラミングと型レベルのプログラミングの類似点を挙げてみる。

パラダイム

型レベルプログラミングには、オブジェクト指向と関数型の2つの主要なパラダイムがあります。ここからリンクされているほとんどの例は、オブジェクト指向のパラダイムに従っています。

オブジェクト指向のパラダイムにおける型レベルプログラミングの非常にシンプルで良い例は、apocalisp の ラムダ計算の実装 で見ることができます。

// Abstract trait
trait Lambda {
  type subst[U <: Lambda] <: Lambda
  type apply[U <: Lambda] <: Lambda
  type eval <: Lambda
}

// Implementations
trait App[S <: Lambda, T <: Lambda] extends Lambda {
  type subst[U <: Lambda] = App[S#subst[U], T#subst[U]]
  type apply[U] = Nothing
  type eval = S#eval#apply[T]
}

trait Lam[T <: Lambda] extends Lambda {
  type subst[U <: Lambda] = Lam[T]
  type apply[U <: Lambda] = T#subst[U]#eval
  type eval = Lam[T]
}

trait X extends Lambda {
  type subst[U <: Lambda] = U
  type apply[U] = Lambda
  type eval = X
}

この例からわかるように、型レベルプログラミングのためのオブジェクト指向パラダイムは次のように進みます。

• 最初に：様々な抽象的な型フィールドを持つ抽象的なtraitを定義します（抽象的なフィールドとは何かは後述します）。これは、実装を強制することなく、ある特定の型フィールドがすべての実装に存在することを保証するためのテンプレートです。ラムダ計算の例で言えば、これは trait Lambda で、以下の型が存在することを保証しています。 subst , apply そして eval .
• 次ページ：抽象traitを拡張するサブtraitを定義し、様々な抽象型フィールドを実装する
  • 多くの場合、これらのサブトレートは引数でパラメータ化されます。ラムダ計算の例では、サブタイプは trait App extends Lambda で、これは二つの型にパラメータ化されています ( S と T のサブタイプである必要があります。 Lambda ), trait Lam extends Lambda を1つの型にパラメータ化したもの( T )、そして trait X extends Lambda (これはパラメータ化されていません)。
  • の型フィールドは、サブストラクトの型パラメータを参照することで実装されることが多く、ハッシュ演算子でその型フィールドを参照することもあります。 # (これはドット演算子に非常に似ています。 . というドット演算子に非常に似ています）。traitでは App のラムダ計算の例では、タイプ eval は次のように実装されている。 type eval = S#eval#apply[T] . これは、本質的に eval の型は trait のパラメータである S を呼び出すこと、そして apply をパラメータ T を加えたものです。注意 S が保証されているのは eval のサブタイプであることが指定されているため、この型が保証されています。 Lambda . 同様に eval の結果は apply のサブタイプとして指定されているので Lambda のサブタイプであると指定されているため、抽象的な特性である Lambda .

Functionalパラダイムは、traitにまとめられていないパラメータ化された型コンストラクタをたくさん定義することで成り立っています。

値レベルプログラミングと型レベルプログラミングの比較

• 抽象クラス
  • の値レベルを指定します。 abstract class C { val x }
  • タイプレベル。 trait C { type X }
• パス依存型
  • C.x (オブジェクトCのフィールド値/関数xを参照する)
  • C#x (特質Cのフィールド型xを参照)
• 関数シグネチャ(実装なし)
  • 値レベルの def f(x:X) : Y
  • タイプレベル。 type f[x <: X] <: Y (これは型コンストラクタと呼ばれ、通常抽象的な特質で発生します)
• 関数実装
  • 値レベルの def f(x:X) : Y = x
  • タイプレベル。 type f[x <: X] = x
• 条件式
  • こちらをご覧ください
• 等質性の確認
  • 値レベルの a:A == b:B
  • タイプレベル。 implicitly[A =:= B]
  • value-level: 実行時にユニットテストを介してJVMで発生します(すなわち、実行時エラーはありません)。
    • は本質的にアサートです。 assert(a == b)
  • type-level: コンパイラで型チェックが行われます (つまり、コンパイラのエラーはありません)。
    • は本質的には型比較である：例えば implicitly[A =:= B]
    • A <:< B の場合のみ、コンパイルされます。 A のサブタイプである場合 B
    • A =:= B の場合のみ、コンパイルされます。 A のサブタイプである場合 B と B のサブタイプです。 A
    • A <%< B として表示可能な場合のみコンパイルされます。 A として見ることができる場合のみコンパイルされます。 B (として見ることができます。 A のサブタイプに暗黙のうちに変換されます。 B )
    • 例
    • その他の比較演算子

型と値の間の変換

• 多くの例では、traitによって定義された型は抽象的であると同時に密封されていることが多いため、直接インスタンス化することも匿名サブクラスを介してインスタンス化することもできません。そのため、一般的には null をプレースホルダー値として使用するのが一般的です。

  • 例 val x:A = null ここで A は気になるタイプ

• 型消しのため、パラメータ化された型はすべて同じに見えます。さらに、(上記のように) あなたが扱っている値は、すべて null であることが多いので、（matchステートメントなどで）オブジェクトの型を条件付けることは効果的ではありません。

コツは暗黙の関数と値を使うことです。ベースケースは通常暗黙の値であり、再帰的ケースは通常暗黙の関数である。実際、型レベルプログラミングは暗黙知を多用します。

この例を考えてみましょう ( metascalaから引用 と アポカリプス ):

sealed trait Nat
sealed trait _0 extends Nat
sealed trait Succ[N <: Nat] extends Nat

ここでは自然数のペアノ符号化を行っています。つまり、非負の各整数に対して型があります。0に対しては特別な型、すなわち _0 という特別な型があり、0 より大きな整数はそれぞれ Succ[A] であり、ここで A はより小さい整数を表す型である。例えば、2を表す型は、以下のようになります。 Succ[Succ[_0]] (となります（0を表す型には2回後継が適用されます）。

より便利に参照するために、様々な自然数の別名を付けることができます。例を挙げます。

type _3 = Succ[Succ[Succ[_0]]]

(これは val を関数の結果であると定義するのと同じです)。

さて、値レベルの関数を定義したいとすると def toInt[T <: Nat](v : T) を定義し、引数として値を取るとします。 v に準拠し、かつ Nat でエンコードされた自然数を表す整数を返します。 v の型にエンコードされた自然数を表す整数を返します。例えば、値が val x:_3 = null ( null タイプの Succ[Succ[Succ[_0]]] を含む)、私たちは toInt(x) を返すように 3 .

を実装するには toInt を実装するために、以下のクラスを利用します。

class TypeToValue[T, VT](value : VT) { def getValue() = value }

後述するように、オブジェクトはクラス TypeToValue に対して、それぞれの Nat から _0 まで _3 で、それぞれ対応する型の値表現が格納されます (つまり TypeToValue[_0, Int] は値 0 , TypeToValue[Succ[_0], Int] は値を格納します 1 など）。注意 TypeToValue は2つのタイプでパラメータ化されています。 T と VT . T は、値を割り当てようとしている型に対応します（この例では。 Nat ) と VT は、代入する値のタイプに対応します (この例では Int ).

ここで、以下の2つの暗黙の定義を行う。

implicit val _0ToInt = new TypeToValue[_0, Int](0)
implicit def succToInt[P <: Nat](implicit v : TypeToValue[P, Int]) = 
     new TypeToValue[Succ[P], Int](1 + v.getValue())

そして toInt を以下のように実装します。

def toInt[T <: Nat](v : T)(implicit ttv : TypeToValue[T, Int]) : Int = ttv.getValue()

を理解するために toInt がどのように機能するかを理解するために、いくつかの入力に対してそれが何をするかを考えてみましょう。

val z:_0 = null
val y:Succ[_0] = null

を呼び出すと toInt(z) を呼び出すと、コンパイラは暗黙の引数として ttv 型の TypeToValue[_0, Int] (ただし z は _0 ). これは、オブジェクト _0ToInt を見つけると、それは getValue メソッドを呼び出すと、このオブジェクトの 0 . 注意すべき重要な点は、どのオブジェクトを使うかをプログラムに指定せず、コンパイラが暗黙のうちにそれを見つけていることです。

では、次に toInt(y) . このとき、コンパイラは暗黙の引数を探します。 ttv 型の TypeToValue[Succ[_0], Int] (ただし y は Succ[_0] ). これは，関数 succToInt という関数があり、これは適切な型のオブジェクトを返すことができます ( TypeToValue[Succ[_0], Int] ) を返し、それを評価します。この関数自身は暗黙の引数( v ) を受け取ります。 TypeToValue[_0, Int] (つまり TypeToValue ここで、最初の型パラメータは一つ少ない Succ[_] ). コンパイラは _0ToInt (の評価で行われたように）。 toInt(z) の評価で行ったように）、そして succToInt は新しい TypeToValue オブジェクトを構築します。 1 . ここでも重要なのは、私たちはこれらの値に明示的にアクセスできないので、コンパイラはこれらの値をすべて暗黙的に提供していることです。

作業のチェック

型レベルの計算が期待通りに行われているかどうかを確認する方法はいくつかあります。ここでは、いくつかのアプローチを紹介します。2つの型を作る A と B が等しいことを確認します。そして、以下のようにコンパイルされることを確認します。

• Equal[A, B]
  • with: 特質 Equal[T1 >: T2 <: T2, T2] ( apocolispより引用 )
• implicitly[A =:= B]

あるいは、型を（上記のように）値に変換し、その値の実行時チェックを行うこともできます。例 assert(toInt(a) == toInt(b)) , ここで a はタイプ A と b は、タイプ B .

追加リソース

利用可能なコンストラクトの完全なセットは、以下のセクションにあります。 scala リファレンスマニュアル (pdf) .

アドリアン・ムーア は、型構成子や関連するトピックについて、scala の例とともにいくつかの学術論文を掲載しています。

• より高い種類のジェネリック (pdf)
• Scalaのためのコンストラクタ多相性型。理論と実践 (pdf) (Moorsによる前回の論文を含む博士論文）
• 型コンストラクタ多相性推論

アポカリプス は、scalaでの型レベルプログラミングの例をたくさん紹介しているブログです。

• Scalaの型レベルプログラミング は、ブーリアン、自然数（上記）、2進数、非均質リストなどを含む、いくつかの型レベルプログラミングの素晴らしいガイド付きツアーです。
• その他のScalaのタイプハッカリー は上記のラムダ計算の実装です。

ScalaZ は、様々な型レベルのプログラミング機能を用いてScala APIを拡張する機能を提供する、非常に活発なプロジェクトである。非常に興味深いプロジェクトであり、多くの人に支持されています。

MetaScala はScalaのための型レベルライブラリで、自然数、ブーリアン、単位、HListなどのメタ型を含んでいます。によるプロジェクトです。 Jesper Nordenberg (彼のブログ) .

は ミチド（ブログ） には、Scalaにおける型レベルプログラミングの素晴らしい例があります（他の回答から）。

• Scalaによるメタプログラミング パート1：追加
• Scalaのメタプログラミング 第2部：乗算
• Scalaのメタプログラミング Part III: 部分的な関数の適用
• Scalaのメタプログラミング。条件付きコンパイルとループのアンローリング
• SKI計算のScala型レベルエンコーディング。

デバシシュ ゴッシュ (ブログ) にも関連する記事があります。

• scala における高次の抽象化
• 静的型付けでスタートダッシュ
• Scala は型クラスを暗黙的に定義します．
• scala の型クラスへのリファクタリング
• 一般化された型制約の使用
• スカラ型システムの単語をどのように使うか
• 抽象型メンバの選択

(このテーマについて調べてみたところ、以下のようなことがわかりました。私はまだ初心者なので、この答えに不正確な点があれば指摘してください)