Dependent type
In computer science and logic, a dependent type is a type whose definition depends on a 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, F*, Epigram, and Idris, dependent types may help reduce bugs by enabling the programmer to assign types that further restrain the set of possible implementations.
Wikipage disambiguates
Comparision of programming languages with dependent typesComparison of dependently typed programming languagesDependent type theoryDependent typesDependent typingDependently-typedDependently-typed languageDependently-typed programming languageDependently typedDependently typed languageDependently typed programmingDependently typed programming languageSigma typeType-level programmingΛΠ-calculus
Wikipage redirect
ALF (proof assistant)Agda (programming language)AldorAutomathCalculus of constructionsCartesian closed categoryComma categoryComparision of programming languages with dependent typesComparison of dependently typed programming languagesConstructive set theoryContainer (type theory)CoqCurry–Howard correspondenceDTPDependencyDependent MLDependent type theoryDependent typesDependent typingDependently-typedDependently-typed languageDependently-typed programming languageDependently typedDependently typed languageDependently typed programmingDependently typed programming languageEpigram (programming language)F* (programming language)Fiber bundleFibred categoryFirst-class citizenFormal verificationFriCASFunction typeFunctional programmingGeneralized algebraic data typeGroupoidGuru (disambiguation)Haskell (programming language)Higher-order logic
Link from a Wikipage to another Wikipage
seeAlso
primaryTopic
Dependent type
In computer science and logic, a dependent type is a type whose definition depends on a 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, F*, Epigram, and Idris, dependent types may help reduce bugs by enabling the programmer to assign types that further restrain the set of possible implementations.
has abstract
En Informatique et en Logique, ...... de langages à type dépendant.
@fr
In computer science and logic, ...... ecking may become undecidable.
@en
Závislostní typ je v teorii ty ...... pečnost a korektnost programu.
@cs
Στην επιστήμη των υπολογιστών ...... ληθευμένη μαθηματική απόδειξη.
@el
Зависимый тип (англ. dependent ...... тивный доказатель теорем Coq).
@ru
依存型 (いぞんがた、英: dependent type) ...... 問題を含んでしまう。したがって、この場合ははとなってしまう。
@ja
在计算机科学和逻辑中，依赖类型（或依存类型，dependen ...... ML 衍生而来的 ATS 和 由 F# 衍生而来的 F*。
@zh
Link from a Wikipage to an external page
Wikipage page ID
page length (characters) of wiki page
Wikipage revision ID
1,020,096,930
Link from a Wikipage to another Wikipage
id
dependent+product
@en
dependent+product+type
@en
dependent+sum
@en
dependent+sum+type
@en
dependent+type
@en
dependent+type+theory
@en
title
dependent product type
@en
dependent product
@en
dependent sum type
@en
dependent sum
@en
dependent type theory
@en
dependent type
@en
wikiPageUsesTemplate
hypernym
type
comment
En Informatique et en Logique, ...... de langages à type dépendant.
@fr
In computer science and logic, ...... t of possible implementations.
@en
Závislostní typ je v teorii ty ...... tové typy kartézskému součinu.
@cs
Στην επιστήμη των υπολογιστών ...... ύπος εξαρτάται από την τιμή ν.
@el
Зависимый тип (англ. dependent ...... ак он «зависит» от величины n.
@ru
依存型 (いぞんがた、英: dependent type) ...... の値よりも大きいような整数の対をエンコードすることができる。
@ja
在计算机科学和逻辑中，依赖类型（或依存类型，dependen ...... 成为不可判定问题；换言之，无法确保程序的类型检查一定会停机。
@zh
label
Dependent type
@en
Type dépendant
@fr
Závislostní typ
@cs
Εξαρτώμενος τύπος
@el
Зависимый тип
@ru
依存型
@ja
依赖类型
@zh