In the area of mathematical logic and computer science known as type theory, a kind is the type of a type constructor or, less commonly, the type of a higher-order type operator. A kind system is essentially a simply typed lambda calculus "one level up", endowed with a primitive type, denoted and called "type", which is the kind of any data type which does not need any type parameters. .

Property Value
dbo:abstract
  • 数理論理学や計算機科学の型理論として知られる分野において、カインドは型コンストラクタの型、もしくはより一般的ではないが高階型演算子の型です。カインドシステムは本質的には、基本型という で表記され「型」と呼ばれる型を持っている「一階上の」単純型付きラムダ計算で、基本型とは型パラメータを必要としない任意のデータ型のカインドです。 カインドは「(データ)型の型」という紛らわしい説明がされることもありますが、むしろ実際にはアリティ指定子です。文法的には、多相型を型コンストラクタと見なすのが自然で、従って多相でない型は零項の型コンストラクタと見なせます。しかし全ての零項の型コンストラクタ、従って全ての単相的な型は、同一の最も単純なカインドすなわち を持ちます。 高階型演算子はプログラミング言語にはめったにないので、ほとんどのプログラミング言語では実際には、カインドはデータ型とパラメータ多相を実装するのに使われるコンストラクタの型を区別するために使われます。HaskellやScalaのような、プログラム的にアクセス可能な方法でパラメータ多相の情報を提供する型システムを持つ言語において、明示的もしくは暗黙的にカインドは現れます。 (ja)
  • Род в теории типов (англ. kind) — тип конструктора типов, или более формально, тип ти́пового оператора высшего порядка. Система родо́в естественным образом представляется как родительское (вышестоящее) просто типизированное лямбда-исчисление, снабжённое примитивным типом, обозначаемым «*» (читается «тип»), формирующим род мономорфных типов данных. Более наглядно, род представляет собой тип типов, или метатип — аналогично тому как множество значений формирует тип, — множество типов формирует род. При этом вхождение типов в более общие типы (в качестве подтипов) отличается от принадлежности типов роду — деление разнообразных типов на рода происходит на более абстрактном уровне. Например, типы «натуральное», «целое» и «вещественное» являются подтипами более общего типа «число»; все четыре типа представляют непосредственные значения, и поэтому принадлежат к роду «*». Другие рода формируются из разнообразных операций над типами — подобно тому как в арифметике различают числа и операции над числами. Синтаксически естественно было бы считать все полиморфные типы конструкторами типов; и, соответственно, все мономорфные — нульарными конструкторами типов. Однако, все нульарные конструкторы, то есть все мономорфные типы, в действительности принадлежат к единому роду, а именно к «*». Из-за того, что ти́повые операторы высших порядков нетипичны для большинства языков программирования, в практике программирования рода́ используются для того, чтобы отличать типы данных от типов конструкторов, используемых для реализации параметрического полиморфизма. Рода́ явным или неявным образом появляются в языках с полными системами типов, таких как Haskell и Scala. (ru)
  • In the area of mathematical logic and computer science known as type theory, a kind is the type of a type constructor or, less commonly, the type of a higher-order type operator. A kind system is essentially a simply typed lambda calculus "one level up", endowed with a primitive type, denoted and called "type", which is the kind of any data type which does not need any type parameters. A kind is sometimes confusingly described as the "type of a (data) type", but it is actually more of an arity specifier. Syntactically, it is natural to consider polymorphic types to be type constructors, thus non-polymorphic types to be nullary type constructors. But all nullary constructors, thus all monomorphic types, have the same, simplest kind; namely . Since higher-order type operators are uncommon in programming languages, in most programming practice, kinds are used to distinguish between data types and the types of constructors which are used to implement parametric polymorphism. Kinds appear, either explicitly or implicitly, in languages whose type systems account for parametric polymorphism in a programatically accessible way, such as Haskell and Scala. (en)
dbo:wikiPageID
  • 20627460 (xsd:integer)
dbo:wikiPageRevisionID
  • 720848856 (xsd:integer)
dct:subject
rdfs:comment
  • 数理論理学や計算機科学の型理論として知られる分野において、カインドは型コンストラクタの型、もしくはより一般的ではないが高階型演算子の型です。カインドシステムは本質的には、基本型という で表記され「型」と呼ばれる型を持っている「一階上の」単純型付きラムダ計算で、基本型とは型パラメータを必要としない任意のデータ型のカインドです。 カインドは「(データ)型の型」という紛らわしい説明がされることもありますが、むしろ実際にはアリティ指定子です。文法的には、多相型を型コンストラクタと見なすのが自然で、従って多相でない型は零項の型コンストラクタと見なせます。しかし全ての零項の型コンストラクタ、従って全ての単相的な型は、同一の最も単純なカインドすなわち を持ちます。 高階型演算子はプログラミング言語にはめったにないので、ほとんどのプログラミング言語では実際には、カインドはデータ型とパラメータ多相を実装するのに使われるコンストラクタの型を区別するために使われます。HaskellやScalaのような、プログラム的にアクセス可能な方法でパラメータ多相の情報を提供する型システムを持つ言語において、明示的もしくは暗黙的にカインドは現れます。 (ja)
  • In the area of mathematical logic and computer science known as type theory, a kind is the type of a type constructor or, less commonly, the type of a higher-order type operator. A kind system is essentially a simply typed lambda calculus "one level up", endowed with a primitive type, denoted and called "type", which is the kind of any data type which does not need any type parameters. . (en)
  • Род в теории типов (англ. kind) — тип конструктора типов, или более формально, тип ти́пового оператора высшего порядка. Система родо́в естественным образом представляется как родительское (вышестоящее) просто типизированное лямбда-исчисление, снабжённое примитивным типом, обозначаемым «*» (читается «тип»), формирующим род мономорфных типов данных. (ru)
rdfs:label
  • カインド (型理論) (ja)
  • Род (теория типов) (ru)
  • Kind (type theory) (en)
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
is dbo:wikiPageDisambiguates of
is dbo:wikiPageRedirects of
is foaf:primaryTopic of