Curry-Howard同型に基づいたScalaのunpacked union型

翻訳者によるメモ。 Scalaの将来のバージョン（「Don Giovanni」）は、ユニオン型のサポートを発表しました。 Shapelessの作成者として狭いサークルで広く知られているMiles Sabinは、 この 2011年の記事で、今すぐ結合タイプを作成する方法を示しています。
UPD この記事で紹介されているアプローチでは、実際のタイプの統合を取得することはできず、さらに、コンパイル時間に大きな影響を与える可能性があります。 また、記事で使用されている交差のタイプ（ A with B ）は、可換性の性質がないため、従来のものとは異なります。 これらの問題やその他の問題を解決するDottyパイロットプロジェクトの詳細は、EPFLのScalaコンパイラーの開発者であるDmitry Petrashko darkdimius による素晴らしいプレゼンテーションに記載されています。

Scalaには非常に表現力豊かな型システムがあります。 ただし、（少なくともプリミティブとして）切望されているすべての要素が含まれているわけではありません。 このカテゴリに該当する本当に便利なタイプがいくつかあります。これらは、高ランク（高ランク）および再帰構造タイプの多態性関数のタイプです。 しかし、次の投稿でそれらについて詳しく説明します。今日は、Scalaでユニオン型を作成する方法を紹介します。 説明の過程で、Curry-Howard同型にいくつかの光を当て、それを目的に使用する方法を示します。



それでは、手始めに、ユニオン型とは何ですか？ ユニオンのタイプは、多くの点であなたが期待するものです。2つ（またはそれ以上、ただし私は2つだけに制限します）タイプのユニオンです。 このタイプの値には、結合された各タイプのすべての値が含まれます。 これが意味することは、例を理解するのに役立ちますが、最初に表記法を導入します。 すぐに明らかになる理由から、操作記号OR： T ∨ U Uして、タイプTとU和集合を書き留めますT ∨ U したがって、 Int型とString型の結合は、 Intとして記述されます。 このタイプのユニオンの値には、 Intタイプのすべての値とStringタイプのすべての値が含まれます。

しかし、これは具体的にどういう意味ですか？ つまり、Scalaでそのような型を直接表現できれば、たとえば次のように書くことができます。

 def size(x: Int ∨ String) = x match { case i: Int => i case s: String => s.length } size(23) == 23 // OK size("foo") == 3 // OK size(1.0) //  OK,   

言い換えると、 sizeメソッドは、 Int型またはString型（そのサブタイプNullおよびNothingを含む）の引数を受け入れ、それ以外は受け入れNothing 。

このタイプのプールを使用することと標準のEitherを使用することの違いを強調することが重要です。 和型として知られるEither 、サブタイプをサポートしない言語のユニオン型に類似しています。 Eitherを使用して例を書き換えると、次のようになります。

 def size(x: Either[Int, String]) = x match { case Left(i) => i case Right(s) => s.length } size(Left(23)) == 23 // OK size(Right("foo")) == 3 // OK 

Either[Int, String]の型Either[Int, String]は、ユニオン型Int ∨ Stringモデル化できます。これは、それらと値の間に対応（同型）があるためです。 ただし、Etherタイプは、ボックス化されていない型システムプリミティブとしてではなく、ボックス化された表現の追加レイヤーであることによってこれを達成することは絶対に明らかです。 Eitherよりも優れたものを作成できますEither ？ パッケージングを必要とせず、予想されるすべての静的保証を使用せずに、Scalaでユニオン型を表す方法を見つけることができますか？

できることはわかっていますが、結果に至る途中で、 Curry-Howard同型を使用して1次の論理を迂回する必要があります。 この同型は、型システム内の型間の関係は、論理システム内のステートメント間の関係のイメージと見なすことができることを示しています（逆も同様です）。 話している型システムと選択した論理システムに応じて、このステートメントをさまざまな方法で解釈できますが、説明ではほとんどの詳細を無視し、簡単な例に焦点を当てます。

Scalaのようなサブタイプを持つ型システムのコンテキストでカリーハワード同型を示します。 交差のタイプ（ A with B ）と論理積（ A ∧ B ）の間に対応があることに気付くかもしれません。 私の仮定的なタイプの統一（ A ∨ B ）と論理的分離（上記で示唆されたようにA∨B）; サブタイプ（ A <: B ）と論理的含意（ A ⇒ B ）の間。 次の表の左の列には、Scalaで実行されるサブタイプの関係があります（ただし、言語で直接表現されない共用体型の場合）。 ⇒ 。 いずれの場合も、このような置換は論理的に正しい式を提供します。

（AとB）<：A	（A∧B）⇒A
（AとB）<：B	（A∧B）⇒B
A <：（A∨B）	A⇒（A∨B）
B <：（A∨B）	B⇒（A∨B）

カリー-ハワード同型の本質は、機械的な置換プロセスが常に正しいことです-正しい型の式は常に正しい論理式に書き換えられ、逆の場合も同様です。 そしてこれは、結合、分離、含意のためだけに行われません。 また、否定（今日の考慮事項で重要な操作）や一般性と存在の量指定子を含む論理式への対応を一般化することもできます。

否定の追加は、私たちにとって何を意味しますか？ 2つのタイプの組み合わせ（つまり、 A with B ）には、同時にAとBの両方Aインスタンスである値があります。 同様に、タイプA否定（ ¬[A]と書く）には、タイプAインスタンスではない値が必要であると仮定できますA 否定はScala言語で直接表現することもできませんが、そうではないと仮定してどこに行けばいいのでしょうか？

その場合、Curry-Howard同型とDe Morganの法則を使用して、交差と否定のタイプからユニオンタイプの定義を取得できます。 それがどうなるかはここにあります...

まず、De Morganの平等を思い出してください。

 (A ∨ B) ⇔ ¬(¬A ∧ ¬B) 

次に、Curry-Howard同型を適用します（Scalaの同値=:=操作を使用）。

 (A ∨ B) =:= ¬[¬[A] with ¬[B]] 

これをScalaに書き込む方法を見つけることができれば、目標は達成され、さまざまな種類の統一が可能になります。 では、Scalaで型否定を表現できますか？

残念ながら、できません。 しかし、できることは、変換されたコンテキストで否定を記述できるようにすべての型を変換することです。 次に、すべてを元の未修正のコンテキストで機能させる方法を見つける必要があります。

一部の読者は、以前に連結と組み合わせた交差タイプ、分離と組み合わせたユニオンタイプ、および含意と組み合わせたサブタイプ比を使用してカリーハワード同型を説明したときに少し驚いたかもしれません。 通常、製品タイプ、つまり (A, B)接続詞をモデル化し、和のタイプ（ Either[A, B] ）は選言をモデル化し、関数タイプは含意をモデル化します。 製品、合計、関数を使用して前の表を書き換えると、次のようになります。

（A、B）=> A	（A∧B）⇒A
（A、B）=> B	（A∧B）⇒B
A => [A、B]のいずれか	A⇒（A∨B）
B =>どちらか[A、B]	B⇒（A∨B）

左側では、サブタイプの関係に関する正確性はもはや期待されていません。代わりに、関数のシグネチャのみに基づいて関数型を実装できるかどうかを判断できるようにするパラメトリックの原則を観察する必要があります。 明らかに、左の列のすべての関数シグネチャを実装できます。 最初の2つのケースでは、関数の引数としてペア(A, B)があるため、 _1または_2を使用してこのペアからタイプAまたはB値を簡単に取得できます。

 val conj1: ((A, B)) => A = p => p._1 val conj2: ((A, B)) => B = p => p._2 

2番目と3番目のケースでは、関数の引数はそれぞれタイプAとB値であるため、コンストラクターLeft[A]とRight[B]を使用してEither[A, B]型Either[A, B]結果を取得できます。

 val disj1: A => Either[A, B] = a => Left(a) val disj2: B => Either[A, B] = b => Right(b) 

この形式で、カリー-ハワード同型は通常、サブタイプのない言語で表現されます。 ただし、共用体タイプと交差タイプは、本質的にサブタイプに基づいています。 したがって、考慮されたマッピングは、決して組合を助けません。 しかし、それは否定の助けになります。これはパズルの欠けている部分です。

サブタイプの有無にかかわらず、ScalaでNothingとして表される最小のタイプ（ボトムタイプ）は論理falseにマップされます。 たとえば、次の等式はすべて真です。

A =>どちらか[A、Nothing]	A⇒（A∨false）
B =>どちらか[Nothing、B]	B⇒（false∨B）

これは、左側のすべての関数シグネチャが実現可能であり、右側の論理式が真であるという事実に基づいています（James Airyの投稿では、一致する製品/接続のケースを表示しない理由を説明しています）。 次のシグネチャを持つ関数に対応するものについて考えてみましょう。

 A => Nothing 

カリー-ハワード同型性の右側の論理的な側面では、このシグネチャは数式¬Aます。これは¬Aと同等¬A 。 それは非常に直感的に合理的なようです-タイプNothingの値がないため、シグネチャA => Nothingを実装できません（例外をスローすることを除き、この場合は許可されません）。

この署名を型否定の表現として使用するとどうなるか見てみましょう。

 type ¬[A] = A => Nothing 

そして、De Morganの法則の文脈でそれを適用して、関連付けのタイプを取得します。

 type ∨[T, U] = ¬[¬[T] with ¬[U]] 

これで、Scala REPLを使用して型を確認できます。

 scala> type ¬[A] = A => Nothing defined type alias $u00AC scala> type ∨[T, U] = ¬[¬[T] with ¬[U]] defined type alias $u2228 scala> implicitly[Int <:< (Int ∨ String)] <console>:11: error: Cannot prove that Int <:< ((Int) => Nothing with (String) => Nothing) => Nothing. implicitly[Int <:< (Int ∨ String)] 

REPLは、ソリューションがまだ受信されていないことを示しています。 implicitly[Int <:< (Int ∨ String)]な式implicitly[Int <:< (Int ∨ String)]は、 IntがIntのサブタイプであることを証明できるかどうかをコンパイラーに尋ねます。これは、共用体のタイプに当てはまります。

何が悪かったのですか？ 問題は、 A => Nothingとして指定された型否定を使用するために、 <:<演算子の右側の型を関数型に変換したことです。 これは、ユニオンのタイプ自体が関数のタイプであることを意味します。 しかし、これは明らかに、INTがユニオン型のサブタイプであることとは異なり、REPLからのエラーメッセージが表示されます。 エラーを排除するには、 <:<演算子の左側を、右側の型のサブタイプになる型に変換する必要もあります。

これはどのような変革ですか？ 二重否定はどうですか？

 type ¬¬[A] = ¬[¬[A]] 

コンパイラーの言うことを見てみましょう：

 scala> type ¬¬[A] = ¬[¬[A]] defined type alias $u00AC$u00AC scala> implicitly[¬¬[Int] <:< (Int ∨ String)] res5: <:<[((Int) => Nothing) => Nothing, ((Int) => Nothing with (String) => Nothing) => Nothing] = <function1> scala> implicitly[¬¬[String] <:< (Int ∨ String)] res6: <:<[((String) => Nothing) => Nothing, ((Int) => Nothing with (String) => Nothing) => Nothing] = <function1> 

ビンゴ！ ¬¬[Int]と¬¬[String]は両方とも、 ¬¬[Int]サブタイプです。

次に、毎回肯定的な答えを返すだけではないことを確認する必要があります。

 scala> implicitly[¬¬[Double] <:< (Int ∨ String)] <console>:12: error: Cannot prove that ((Double) => Nothing) => Nothing <:< ((Int) => Nothing with (String) => Nothing) => Nothing. 

それで、私たちはほとんど終わりました、最後の仕上げをすることは残っています。 所有するサブタイプの関係は、取得したいサブタイプと同型です（タイプ¬¬[T]は¬¬[T]と同型であるため）。 しかし、私たちはまだ必要な未修正の型と同じ関係を表現する方法がありません。

この問題を解決するには、 ¬[T] 、 ¬¬[T]および¬¬[T]ファントムタイプを検討し、これらのタイプの値を直接操作するのではなく、必要なサブタイプの関係を表すためだけに使用します。 テストケースでこれがどのように発生するかを次に示します。

 def size[T](t: T)(implicit ev: (¬¬[T] <:< (Int ∨ String))) = t match { case i: Int => i case s: String => s.length } 

これは一般化された型制約を使用します。これは、 sizeメソッドの型引数として推定されるTがその二重否定がInt∨Stringのサブタイプであることをコンパイラが証明することを要求します。 次のREPLセッションが示すように、この条件は、 TがIntまたはString場合にのみ満たされます。

 scala> def size[T](t: T)(implicit ev: (¬¬[T] <:< (Int ∨ String))) = | t match { | case i: Int => i | case s: String => s.length | } size: [T](t: T)(implicit ev: <:<[((T) => Nothing) => Nothing, ((Int) => Nothing with (String) => Nothing) => Nothing])Int scala> size(23) res8: Int = 23 scala> size("foo") res9: Int = 3 scala> size(1.0) <console>:13: error: Cannot prove that ((Double) => Nothing) => Nothing <:< ((Int) => Nothing with (String) => Nothing) => Nothing. 

そして今、最後のトリック。 構文に関しては、暗黙の証明パラメーターはtheくて重いように見えますが、これをT型のパラメーターのコンテキスト制約に変換することで修正できます。

 type |∨|[T, U] = { type λ[X] = ¬¬[X] <:< (T ∨ U) } def size[T: (Int |∨| String)#λ](t: T) = t match { case i: Int => i case s: String => s.length } 

できた！ 言語自体を変更することなく、Scalaでunion型のunpacked、staticly type-safe表現を取得しました！

当然、Scalaがユニオン型をプリミティブとしてサポートする方が良いでしょう。 しかし、少なくとも私たちが得た解決策は、Scalaコンパイラがこれを行うために必要なすべての情報を持っていることを示しています。 今ではマーティンとアドリアーンを悩ませているだけなので、統一のタイプを直接利用できます。