種類（型理論）

数理論理学とコンピュータサイエンスの分野である型理論では、種とは型コンストラクタの型、またはあまり一般的ではないが、高階型演算子の型を指します。種システムは、本質的には「1 レベル上」の単純な型付けのラムダ計算であり、「型」と表記され、その名前が付けられたプリミティブ型を備えています。プリミティブ型は、型パラメータを必要としない任意のデータ型の種です。 ${\displaystyle *}$

種類は「(データ) 型の型」と説明されて混乱を招くことがありますが、実際にはむしろ引数指定子です。構文的には、多態型を型コンストラクタと見なし、非多態型をヌル引数型コンストラクタと見なすのが自然です。ただし、すべてのヌル引数コンストラクタ、つまりすべての単態型は、同じ最も単純な種類、つまり を持ちます。 ${\displaystyle *}$

高階型演算子はプログラミング言語では一般的ではないため、ほとんどのプログラミング実務では、データ型と、パラメトリック多態性を実装するために使用されるコンストラクタの型を区別するために種類が使用されます。種類は、 C++、^[1]、 Haskell、Scalaなど、プログラムからアクセス可能な方法でパラメトリック多態性を考慮した型システムを持つ言語に、明示的または暗黙的に現れます。^[2]

• ${\displaystyle *}$「型」と発音される型は、 nullary型コンストラクタとして見られるすべてのデータ型の種類であり、このコンテキストでは適切な型とも呼ばれます。これには通常、関数型プログラミング言語の関数型が含まれます。
• ${\displaystyle *\rightarrow *}$単項 型コンストラクタの種類です。たとえば、リスト型コンストラクタなどです。
• ${\displaystyle *\rightarrow *\rightarrow *}$は、バイナリ型コンストラクタ（カリー化経由）の種であり、例えばペア型コンストラクタの種であり、関数型コンストラクタの種でもある（その適用の結果と混同しないでください。関数型自体が関数型であるため、種は）${\displaystyle *}$
• ${\displaystyle (*\rightarrow *)\rightarrow *}$は、単項型構成子から適切な型への高階型演算子の一種である。^[3]

(注: Haskell のドキュメントでは、関数の型と種類の両方に同じ矢印が使用されています。)

Haskell 98 ^[4]の種システムには、正確に2つの種が含まれます。

• ${\displaystyle *}$「タイプ」と発音されるものは、すべてのデータ型の種類です。
• ${\displaystyle k_{1}\rightarrow k_{2}}$は単項 型コンストラクタの種であり、 kind の型を受け取り、 kind の型を生成します。${\displaystyle k_{1}}$${\displaystyle k_{2}}$

居住型（Haskell では適切な型はこのように呼ばれます）は値を持つ型です。たとえば、図を複雑にする型クラスを4無視すると、は型 の値でありInt、は型（Int のリスト）[1, 2, 3]の値です。したがって、とは種 を持ちますが、や などの関数型も同様です。 [Int]Int[Int]${\displaystyle *}$Int -> BoolInt -> Int -> Bool

型構築子は 1 つ以上の型引数を受け取り、十分な引数が与えられた場合にデータ型を生成します。つまり、カリー化により部分適用をサポートします。 ^{[5] [6]}これは Haskell がパラメトリック型を実現する方法です。たとえば、型[](リスト) は型構築子です。これはリストの要素の型を指定するために 1 つの引数を受け取ります。したがって、[Int](Int のリスト)、[Float](Float のリスト)、さらには[[Int]](Int のリストのリスト)も[]型構築子の有効な適用です。したがって、[]は種類 の型です。 は種類 を持つため、これに適用すると種類 のになります。2タプルの構築子の種類、3 タプルの構築子の種類、などとなります。 ${\displaystyle *\rightarrow *}$Int${\displaystyle *}$[][Int]${\displaystyle *}$(,)${\displaystyle *\rightarrow *\rightarrow *}$(,,)${\displaystyle *\rightarrow *\rightarrow *\rightarrow *}$

標準 Haskell では、多態的な種類は許可されません。これは、Haskell でサポートされている型のパラメトリック多態性とは対照的です。たとえば、次の例をご覧ください。

データツリーz =リーフ|フォーク(ツリーz ) (ツリーz )           

の種は、 だけでなく など、z何でもかまいません。Haskell は、型が明示的に別のことを示さない限り (以下を参照)、デフォルトで種を常に と推論します。したがって、型チェッカーは、次の の使用を拒否します。 ${\displaystyle *}$${\displaystyle *\rightarrow *}$${\displaystyle *}$Tree

type FunnyTree = Tree [] -- 無効         

の種類が[]、の期待される種類(常に )と一致しないためです。 ${\displaystyle *\rightarrow *}$z${\displaystyle *}$

ただし、高階型演算子は許可されます。例:

データApp unt z = Z ( unt z )       

には種類があり、つまり単項データ コンストラクターであることが期待され、その引数 (型である必要がある) に適用され、別の型を返します。 ${\displaystyle (*\rightarrow *)\rightarrow *\rightarrow *}$unt

GHC には拡張機能 がありPolyKinds、これを と組み合わせることでKindSignatures多態的な種類が可能になります。例:

データTree ( z :: k ) = Leaf | Fork ( Tree z ) ( Tree z )型FunnyTree = Tree [] -- OK            
         

GHC 8.0.1以降では、型と種類が統合されました。^[7]

• システムF-オメガ
• 純粋な型システム