交差点タイプ

型理論では、交差型は、型と型の両方を割り当てることができる値に割り当てることができます。この値には、交差型システムで交差型を割り当てることができます。^[1] 一般に、2 つの型の値の範囲が重なる場合、2 つの範囲の交差に属する値に、これら 2 つの型の交差型を割り当てることができます。このような値は、 2 つの型のいずれかを期待する関数に引数として安全に渡すことができます。たとえば、Javaでは、クラスはおよびインターフェースの両方を実装しています。したがって、型のオブジェクトは、型の引数を期待する関数と、型の引数を期待する関数に安全に渡すことができます。 ${\displaystyle \sigma}$${\displaystyle \tau}$${\displaystyle \sigma \cap \tau}$BooleanSerializableComparableBooleanSerializableComparable

交差型は複合データ型です。積型と同様に、オブジェクトに複数の型を割り当てるために使用されます。ただし、積型はタプルに割り当てられるため、各タプル要素には特定の積型コンポーネントが割り当てられます。比較すると、交差型の基になるオブジェクトは必ずしも複合であるとは限りません。交差型の制限された形式は、洗練型です。

交差型は、オーバーロードされた関数を記述するのに役立ちます。^[2]たとえば、が数値を引数として受け取り、数値を返す関数の型であり、が文字列を引数として受け取り、文字列を返す関数の型である場合、これら2つの型の交差を使用して、与えられた入力の型に基づいて、どちらか一方を実行する（オーバーロードされた）関数を記述できます。 number => numberstring => string

Ceylon、Flow、Java、Scala、TypeScript、Whiley（交差型を持つ言語の比較を参照）などの現代のプログラミング言語は、交差型を使用してインターフェース仕様を組み合わせ、アドホックポリモーフィズムを表現します。パラメトリックポリモーフィズムを補完する交差型は、以下のTypeScriptの例に示すように 、横断的な関心事によるクラス階層の汚染を回避し、定型コードを削減するために使用できます。

交差型の型理論的研究は、交差型分野と呼ばれます。^[3] 注目すべきことに、プログラムの終了は交差型を使用して正確に特徴付けることができます。^[4]

TypeScriptは交差型をサポートしており^[5] 、型システムの表現力を向上させ、潜在的なクラス階層のサイズを削減します。これは以下のように実証されています。

Chicken次のプログラム コードは、 、 、または のいずれかの型のオブジェクトを返すメソッドを持つクラス 、、を定義しますCow。さらに、関数 およびは、それぞれおよび型の引数を必要とします。 RandomNumberGeneratorproduceEggMilknumbereatEggdrinkMilkEggMilk

クラスEgg {プライベートkind : "Egg" }クラスMilk {プライベートkind : "Milk" }      
      

// 卵を生産する
class Chicken { produce () { return new Egg (); } }         

// ミルクを生産する
class Cow { produce () { return new Milk (); } }         

// 乱数を生成します
class RandomNumberGenerator { produce () { return Math . random (); } }        

// egg
関数が必要ですeatEgg ( egg : Egg ) { return "I ate an egg." ; }   
     


// ミルクが必要です
function drinkMilk ( milk : Milk ) { return "ミルクを飲みました。" ; }   
     

次のプログラム コードは、指定されたオブジェクト のメンバー関数を呼び出すアドホック多態関数を定義します。関数には、交差型コンストラクタ を介して接続されたと という2 つの型注釈があります。具体的には、型の引数に適用された場合は型 のオブジェクトを返し、 型の引数に適用された場合は型 のオブジェクトを返します。理想的には、は (おそらく偶然に) メソッドを持つオブジェクトには適用できないはずです。 animalToFoodproduceanimalanimalToFood((_: Chicken) => Egg)((_: Cow) => Milk)&animalToFoodChickenEggCowMilkanimalToFoodproduce

// 鶏が与えられると卵が産まれ、牛が与えられると牛乳が産まれます
。let animalToFood : (( _ : Chicken ) => Egg ) & (( _ : Cow ) => Milk ) = function ( animal : any ) { return animal . produce (); };           
       
         
    

最後に、次のプログラム コードは、上記の定義の 型安全な使用を示しています。

varチキン=新しいチキン();    
var cow =新しいCow ();    
var randomNumberGenerator =新しいRandomNumberGenerator ();    

console.log ( chicken.produce ( )); // Egg { } 
console.log ( cow.produce ()) ; //ミルク{ } 
コンソール.log ( randomNumberGenerator.produce ( ) ) ; //0.2626353555444987 

console.log ( animalToFood ( chicken ) ); //卵{} 
console.log ( animalToFood ( cow ) ); //ミルク{} 
//console.log(animalToFood(randomNumberGenerator)); // エラー: 'RandomNumberGenerator' 型の引数は 'Cow' 型のパラメータには割り当てられません

console . log ( eatEgg ( animalToFood ( Chicken ))); // 卵を食べました。 
//console.log(eatEgg(animalToFood(cow))); // エラー: 'Milk' 型の引数は 'Egg' 型のパラメータに代入できません
console . log ( drinkMilk ( animalToFood ( cow ))); // 牛乳を飲みました。 
//console.log(drinkMilk(animalToFood(chicken))); // エラー: 'Egg' 型の引数は 'Milk' 型のパラメータに代入できません

上記のプログラム コードには次のプロパティがあります。

• 1 行目から 3 行目では、それぞれのタイプのオブジェクト、、を作成しchickenますcow。randomNumberGenerator
• 5 行目から 7 行目では、以前に作成されたオブジェクトについて、呼び出し時のそれぞれの結果 (コメントとして提供) を出力しますproduce。
• 9 行目 (または 10 行目) は、 (または)animalToFoodに適用されたメソッドの型安全な使用を示しています。chickencow
• 11 行目をコメント解除すると、コンパイル時に型エラーが発生します。の実装はのメソッドanimalToFoodを呼び出すことができますが、の型注釈によりそれが許可されません。 これは の意図された意味と一致しています。producerandomNumberGeneratoranimalToFoodanimalToFood
• 13 行目 (resp. 15) は、(resp. )animalToFoodに適用すると、 (resp. )型のオブジェクトが生成されることを示しています。chickencowEggMilk
• 14 行目 (resp. 16) は、(resp. )animalToFoodに適用しても、 (resp. )型のオブジェクトが生成されないことを示しています。したがって、コメントを解除すると、14 行目 (resp. 16) はコンパイル時に型エラーになります。cowchickenEggMilk

上記の最小限の例は、継承を使用して実現できます。たとえば、クラスChickenとをCow基本クラスから派生させることで実現できAnimalます。ただし、より大規模な設定では、これは不利になる可能性があります。クラス階層に新しいクラスを導入することは、横断的な関心事に対して必ずしも正当化されるわけではなく、外部ライブラリを使用する場合など、まったく不可能な場合もあります。上記の例は、次のクラスを使用して拡張できると考えられます。

• Horseメソッドを持たないクラスproduce。
• を返すメソッドSheepを持つクラス。produceWool
• 一度だけ使用でき、 を返すメソッドPigを持つクラス。produceMeat

これには、produce メソッドが使用可能かどうか、produce メソッドが食品を返すかどうか、produce メソッドを繰り返し使用できるかどうかを指定する追加のクラス (またはインターフェース) が必要になる場合があります。全体として、これによりクラス階層が汚染される可能性があります。

上記の最小限の例は、ダックタイピングが与えられたシナリオを実現するのにあまり適していないことをすでに示しています。クラスにはメソッドが含まれていますが、オブジェクトは の有効な引数であってはなりません。上記の例は、ダックタイピングを使用して実現できます。たとえば、クラスに新しいRandomNumberGeneratorフィールドを導入し、対応する型のオブジェクトが の有効な引数であることを示すことによって実現できます。ただし、これにより、それぞれのクラスのサイズが増加するだけでなく (特に に似たメソッドがさらに導入されるため)、 に関して非ローカルなアプローチでもあります。 producerandomNumberGeneratoranimalToFoodargumentForAnimalToFoodChickenCowanimalToFoodanimalToFoodanimalToFood

上記の例は、関数のオーバーロードを使用して実現できます。たとえば、2 つのメソッドとを実装します。TypeScript では、このようなソリューションは、提供されている例とほぼ同じです。Java などの他のプログラミング言語では、オーバーロードされたメソッドの個別の実装が必要です。これにより、コードの重複または定型コードが発生する可能性があります。 animalToFood(animal: Chicken): EgganimalToFood(animal: Cow): Milk

上記の例は、ビジター パターンacceptを使用して実現できます。各動物クラスは、インターフェイスを実装するオブジェクトを受け入れるメソッドを実装する必要がありますAnimalVisitor(非ローカルの定型コードを追加)。関数は、の実装のメソッドanimalToFoodとして実現されます。残念ながら、入力型 (または) と結果型 (または)の間の接続は表現が困難です。 visitAnimalVisitorChickenCowEggMilk

一方で、交差型は、クラス階層に新しいクラス (またはインターフェース) を導入することなく、関数に異なる型をローカルに注釈付けするために使用できます。他方、このアプローチでは、すべての可能な引数の型と結果の型を明示的に指定する必要があります。関数の動作を、統一インターフェース、パラメトリック多態性、またはダックタイピングのいずれかによって正確に指定できる場合、交差型の冗長な性質は不利になります。したがって、交差型は、既存の指定方法を補完するものと見なす必要があります。

従属交差型は、型が項変数に依存する可能性がある従属型です。^[6] 特に、項が従属交差型を持つ場合、項は型と型の両方を持ちます。ここで、は、項変数のすべての出現を項に置き換えた結果として得られる型です。 ${\displaystyle (x:\sigma )\cap \tau }$${\displaystyle \tau}$${\displaystyle x}$${\displaystyle M}$${\displaystyle (x:\sigma )\cap \tau }$${\displaystyle M}$${\displaystyle \sigma}$${\displaystyle \tau [x:=M]}$${\displaystyle \tau [x:=M]}$${\displaystyle x}$${\displaystyle \tau}$${\displaystyle M}$

Scalaはオブジェクトメンバーとして型宣言^[7]をサポートしています。これにより、オブジェクトメンバーの型が別のメンバーの値に依存することが可能になります。これはパス依存型と呼ばれます。^[8] たとえば、次のプログラムテキストは、シングルトンパターンをWitness実装するために使用できるScala特性を定義します。^[9]

特性Witness {型T val値: T {} }  
   
     

上記の特性は、値として型を割り当てることができるWitnessメンバーと、型の値を割り当てることができるメンバーを宣言します。次のプログラム テキストは、上記の特性のインスタンスとしてオブジェクトを定義します。オブジェクトは、型を として、値を として定義します。たとえば、 を実行すると、コンソールに が出力されます。TvalueTbooleanWitnessWitnessbooleanWitnessTBooleanvaluetrueSystem.out.println(booleanWitness.value)true

オブジェクトbooleanWitnessはWitnessを拡張します{型T = Boolean val値= true }    
     
     

を、型 のメンバーを持つオブジェクトの型 (具体的にはレコード型) とします。上記の例では、オブジェクトに従属交差型 を割り当てることができます。その理由は次のとおりです。オブジェクトには、型 がその値として割り当てられたメンバーがあります。は型なので、オブジェクトの型は です。さらに、オブジェクトには、型 の値が割り当てられているメンバーがあります。 の値は なので、オブジェクトの型は です。全体として、オブジェクトの型は交差型 です。したがって、自己参照を依存関係として表すと、オブジェクトは従属交差型 になります。 ${\displaystyle \langle {\textsf {x}}:\sigma \rangle }$${\displaystyle {\textsf {x}}}$${\displaystyle \sigma}$booleanWitness${\displaystyle (x:\langle {\textsf {T}}:{\text{Type}}\rangle )\cap \langle {\textsf {値}}:x.{\textsf {T}}\rangle }$booleanWitnessTBooleanBooleanbooleanWitness${\displaystyle \langle {\textsf {T}}:{\text{Type}}\rangle }$booleanWitnessvaluetrueBooleanbooleanWitness.TBooleanbooleanWitness${\displaystyle \langle {\textsf {値}}:{\textsf {booleanWitness.T}}\rangle }$booleanWitness${\displaystyle \langle {\textsf {T}}:{\text{Type}}\rangle \cap \langle {\textsf {値}}:{\textsf {booleanWitness.T}}\rangle }$booleanWitness${\displaystyle (x:\langle {\textsf {T}}:{\text{Type}}\rangle )\cap \langle {\textsf {値}}:x.{\textsf {T}}\rangle }$

あるいは、上記の最小限の例は、従属レコード型を使用して記述することもできます。^[10] 従属交差型と比較すると、従属レコード型は厳密により特殊化された型理論的概念を構成します。^[6]

型ファミリーの共通部分は、型が項変数に依存する可能性がある依存型です。特に、項が型 を持つ場合、型 の各項に対して、項は型 を持ちます。この概念は、暗黙のPi 型^[11]とも呼ばれ、引数が項レベルで保持されないことに注意してください。 ${\textstyle \bigcap _{x:\sigma }\tau }$${\displaystyle \tau}$${\displaystyle x}$${\displaystyle M}$${\textstyle \bigcap _{x:\sigma }\tau }$${\displaystyle N}$${\displaystyle \sigma}$${\displaystyle M}$${\displaystyle \tau [x:=N]}$${\displaystyle N}$