In computer science and logic, a dependent type is a type whose definition depends on a value. A "pair of integers" is a type. A "pair of integers where the second is greater than the first" is a dependent type because of the dependence on the value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifiers like "for all" and "there exists". In functional programming languages like Agda, ATS, Coq, Epigram and Idris, dependent types prevent bugs by allowing extremely expressive types.

Property Value
dbo:abstract
  • In computer science and logic, a dependent type is a type whose definition depends on a value. A "pair of integers" is a type. A "pair of integers where the second is greater than the first" is a dependent type because of the dependence on the value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifiers like "for all" and "there exists". In functional programming languages like Agda, ATS, Coq, Epigram and Idris, dependent types prevent bugs by allowing extremely expressive types. Two common examples of dependent types are dependent functions and dependent pairs. A dependent function's return type may depend on the value (not just type) of an argument. A function that takes a positive integer "n" may return an array of length "n". (Note that this is different from polymorphism and generic programming, both of which include the type as an argument.) A dependent pair may have a second value that depends on the first. It can be used to encode a pair of integers where the second one is greater than the first. Dependent types add complexity to a type system. Deciding the equality of dependent types in a program may require computations. If arbitrary values are allowed in dependent types, then deciding type equality may involve deciding whether two arbitrary programs produce the same result; hence type checking may become undecidable. (en)
  • En Informatique et en Logique, un type dépendant est un type qui peut dépendre d'une valeur définie dans le langage typé. Les langages Agda et Gallina (de l'assistant de preuve Coq) sont des exemples de langages à type dépendant. (fr)
  • 依存型の中でも、依存関数と依存ペアは特によく使われている。依存関数の戻り値の型は、引数の型だけではなく引数の値に応じて変化する。例えば、整数"n"を引数に取る依存関数は長さ"n"の配列を返すことができる。 (これは、型そのものを引数として取ることができるというポリモーフィズムとは別の概念である。) 依存ペアでは、2番目の型が1番目の値に応じて変化する。依存ペアを使うと、2番目の値が1番目の値よりも大きいような整数の対をエンコードすることができる。 依存型を入れた型システムは、より複雑になる。プログラム中に出現する2つの依存型が等しいかどうかを判定するとき、プログラムの一部を実行する必要があるかもしれない。特に、依存型に任意の式を含めることが許される場合、型の同値性判定は任意に与えられた2個のプログラムが同じ結果をもたらすかどうかを判定する問題を含んでしまう。したがって、この場合は型検査は決定不能となってしまう。 (ja)
  • 在计算机科学和逻辑中,依赖类型(或依存类型,dependent type)是指依赖于值的类型,其理论同时包含了数学基础中的类型论和计算机编程中用以减少程序错误的类型系统两方面。在 Per Martin-Löf 的直觉类型论中,依赖类型可对应于谓词逻辑中的全称量词和存在量词;在依赖类型函数式编程语言如 ATS、Agda、Dependent ML、Epigram、F* 和 Idris 中,依赖类型系统通过极其丰富的类型表达能力使得程序规范得以借助类型的形式被检查,从而有效减少程序错误。 依赖类型的两个常见实例是依赖函数类型(又称依赖乘积类型、Π-类型)和依赖值对类型(又称依赖总和类型、Σ-类型)。一个依赖类型函数的返回值类型可以依赖于某个参数的具体值,而非仅仅参数的类型,例如,一个输入参数为整型值n的函数可能返回一个长度为n的数组;一个依赖类型值对中的第二个值可以依赖于第一个值,例如,依赖类型可表示这样的类型:它由一对整数组成,其中的第二个数总是大于第一个数。 依赖类型增加了类型系统的复杂度。由于确定两个依赖于值的类型的等价性需要涉及具体的计算,若允许在依赖类型中使用任意值的话,其类型检查将会成为不可判定问题;换言之,无法确保程序的类型检查一定会停机。 由于Curry-Howard同构揭示了程序语言的类型论与证明论的直觉逻辑之间的紧密关联性,以依赖类型系统为基础的编程语言大多同时也作为构造证明与可验证程序的辅助工具而存在,如 Coq 和 Agda(但并非所有证明辅助工具都以类型论为基础);近年来,一些以通用和系统编程为目的的编程语言被设计出来,如 Idris。 一些以证明辅助为主要目的的编程语言采用强函数式编程(total functional programming),这消除了停机问题,同时也意味着通过它们自身的核心语言无法实现任意无限递归,不是图灵完全的,如 Coq 和 Agda;另外一些依赖类型编程语言则是图灵完全的,如 Idris、由 ML 衍生而来的 ATS 和 由 F# 衍生而来的 F*。 (zh)
  • Зависимый тип в информатике и логике — тип, который зависит от некоторого значения. Зависимые типы играют ключевую роль в интуиционистской теории типов и построении функциональных языков программирования таких как ATS, Agda и Epigram. К примеру, тип, описывающий n-кортежи действительных чисел является зависимым, так как он «зависит» от величины n. Решение о равенстве зависимых типов в программе может потребовать вычислений. Если в зависимых типах допущено использование произвольных значений, то решение о равенстве типов может включать в себя проверку равенства результата работы двух произвольных программ. Таким образом проверка типа становится неразрешимой задачей. Изоморфизм Карри — Ховарда позволяет строить типы для выражения сколь угодно сложных математических свойств. Если предоставлено конструктивное доказательство того, что тип «заселён» (то есть, существует хотя бы одно значение этого типа), компилятор сможет проверить это доказательство и превратить его в исполняемый код, вычисляющий значение. Наличие проверки доказательств делает зависимо-типизированные языки схожими с программным обеспечением автоматизации доказательств (например, интерактивный доказатель теорем Coq). (ru)
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 1949487 (xsd:integer)
dbo:wikiPageRevisionID
  • 740493581 (xsd:integer)
dbp:id
  • dependent+product
  • dependent+product+type
  • dependent+sum
  • dependent+sum+type
  • dependent+type
  • dependent+type+theory
dbp:title
  • dependent product
  • dependent product type
  • dependent sum
  • dependent sum type
  • dependent type
  • dependent type theory
dct:subject
http://purl.org/linguistics/gold/hypernym
rdf:type
rdfs:comment
  • En Informatique et en Logique, un type dépendant est un type qui peut dépendre d'une valeur définie dans le langage typé. Les langages Agda et Gallina (de l'assistant de preuve Coq) sont des exemples de langages à type dépendant. (fr)
  • 依存型の中でも、依存関数と依存ペアは特によく使われている。依存関数の戻り値の型は、引数の型だけではなく引数の値に応じて変化する。例えば、整数"n"を引数に取る依存関数は長さ"n"の配列を返すことができる。 (これは、型そのものを引数として取ることができるというポリモーフィズムとは別の概念である。) 依存ペアでは、2番目の型が1番目の値に応じて変化する。依存ペアを使うと、2番目の値が1番目の値よりも大きいような整数の対をエンコードすることができる。 依存型を入れた型システムは、より複雑になる。プログラム中に出現する2つの依存型が等しいかどうかを判定するとき、プログラムの一部を実行する必要があるかもしれない。特に、依存型に任意の式を含めることが許される場合、型の同値性判定は任意に与えられた2個のプログラムが同じ結果をもたらすかどうかを判定する問題を含んでしまう。したがって、この場合は型検査は決定不能となってしまう。 (ja)
  • In computer science and logic, a dependent type is a type whose definition depends on a value. A "pair of integers" is a type. A "pair of integers where the second is greater than the first" is a dependent type because of the dependence on the value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifiers like "for all" and "there exists". In functional programming languages like Agda, ATS, Coq, Epigram and Idris, dependent types prevent bugs by allowing extremely expressive types. (en)
  • 在计算机科学和逻辑中,依赖类型(或依存类型,dependent type)是指依赖于值的类型,其理论同时包含了数学基础中的类型论和计算机编程中用以减少程序错误的类型系统两方面。在 Per Martin-Löf 的直觉类型论中,依赖类型可对应于谓词逻辑中的全称量词和存在量词;在依赖类型函数式编程语言如 ATS、Agda、Dependent ML、Epigram、F* 和 Idris 中,依赖类型系统通过极其丰富的类型表达能力使得程序规范得以借助类型的形式被检查,从而有效减少程序错误。 依赖类型的两个常见实例是依赖函数类型(又称依赖乘积类型、Π-类型)和依赖值对类型(又称依赖总和类型、Σ-类型)。一个依赖类型函数的返回值类型可以依赖于某个参数的具体值,而非仅仅参数的类型,例如,一个输入参数为整型值n的函数可能返回一个长度为n的数组;一个依赖类型值对中的第二个值可以依赖于第一个值,例如,依赖类型可表示这样的类型:它由一对整数组成,其中的第二个数总是大于第一个数。 依赖类型增加了类型系统的复杂度。由于确定两个依赖于值的类型的等价性需要涉及具体的计算,若允许在依赖类型中使用任意值的话,其类型检查将会成为不可判定问题;换言之,无法确保程序的类型检查一定会停机。 (zh)
  • Зависимый тип в информатике и логике — тип, который зависит от некоторого значения. Зависимые типы играют ключевую роль в интуиционистской теории типов и построении функциональных языков программирования таких как ATS, Agda и Epigram. К примеру, тип, описывающий n-кортежи действительных чисел является зависимым, так как он «зависит» от величины n. (ru)
rdfs:label
  • Dependent type (en)
  • Type dépendant (fr)
  • 依存型 (ja)
  • Зависимый тип (ru)
  • 依赖类型 (zh)
rdfs:seeAlso
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
is dbo:wikiPageRedirects of
is dbp:paradigm of
is rdfs:seeAlso of
is foaf:primaryTopic of