In computer science and logic, a dependent type is a type which depends on a value. Dependent types play a central role in intuitionistic type theory and in the design of experimental functional programming languages like Dependent ML and Epigram. An example is the type of <math>n</math>-tuples of real numbers, which we may denote as <math>\mbox{Vec}({\mathbb R},n)</math>.

PropertyValue
dbpprop:abstract
  • In computer science and logic, a dependent type is a type which depends on a value. Dependent types play a central role in intuitionistic type theory and in the design of experimental functional programming languages like Dependent ML and Epigram. An example is the type of <math>n</math>-tuples of real numbers, which we may denote as <math>\mbox{Vec}({\mathbb R},n)</math>. This is a dependent type because the type depends on the value <math>n:{\mathbb N}</math>. Deciding 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 becomes undecidable. The Curry-Howard correspondence implies that types can be constructed that express arbitrarily complex mathematical properties. If the user can supply a constructive proof that a type is inhabited (i.e. , that a value of that type exists) then a compiler can then check the proof and convert it into executable computer code that computes the value by carrying out the construction. The proof checking feature makes dependently typed languages closely related to proof assistants. The code-generation aspect provides a powerful approach to formal program verification and proof-carrying code, since the code is derived directly from a mechanically verified mathematical proof.
  • 在计算机科学和逻辑中，依存类型是依存於值的类型。依存类型在直觉类型论和实验性的函数式编程语言如 Dependent ML 或 Epigram 的设计中扮演了关键性角色。 例如，实数 <math>n</math>-元组的类型，可以被稱为 <math>\mbox{Vec}({\mathbb R},n)</math>。因为該类型依存于值 <math>n:{\mathbb N}</math>，是一種依存類型。
dbpprop:hasPhotoCollection
dbpprop:reference
rdfs:comment
  • In computer science and logic, a dependent type is a type which depends on a value. Dependent types play a central role in intuitionistic type theory and in the design of experimental functional programming languages like Dependent ML and Epigram. An example is the type of <math>n</math>-tuples of real numbers, which we may denote as <math>\mbox{Vec}({\mathbb R},n)</math>.
  • 在计算机科学和逻辑中，依存类型是依存於值的类型。依存类型在直觉类型论和实验性的函数式编程语言如 Dependent ML 或 Epigram 的设计中扮演了关键性角色。 例如，实数 <math>n</math>-元组的类型，可以被稱为 <math>\mbox{Vec}({\mathbb R},n)</math>。因为該类型依存于值 <math>n:{\mathbb N}</math>，是一種依存類型。
rdfs:label
  • Dependent type
  • 依赖类型
owl:sameAs
skos:subject
foaf:page
is dbpprop:redirect of