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.

Property Value
dbo:abstract
  • Závislostní typ je v teorii typů typ závisející na konkrétní hodnotě. Obecně se rozlišuje mezi závislostními typy součinovými a součtovými. Je-li nějaký typ z univerza typů, pak je součinový závislostní typ,přičemž je typ závisející na hodnotě .Naopak je součtový závislostní typ. Na lze nahlížet jako na funkci přiřazující hodnotám (typu ) typy (z ). Je-li konstantní, odpovídají součinové typyfunkčním typům () a součtové typy kartézskému součinu(). Závislostní typy byly zavedeny do teorie typů za účelem rozšíření Curry-Howardova isomorfismu z logiky výrokové na predikátovou, odpovídají totiž kvantifikátorům logiky prvního řádu. Používají se v některých programovacích jazycích pro silnou typovou kontrolu, zejména v kritikých aplikacích, kde je kladen velký důraz na bezpečnost a korektnost programu. (cs)
  • Στην επιστήμη των υπολογιστών και την , ένας εξαρτώμενος τύπος είναι ένας τύπος που εξαρτάται από μία τιμή. Οι εξαρτώμενοι τύποι διαδραματίζουν κεντρικό ρόλο στην και στον σχεδιασμό σαν την , την Agda και την . Ένα παράδειγμα είναι ο τύπος των ν-άδων από πραγματικούς αριθμούς. Αυτός είναι ένας εξαρτώμενος τύπος επειδή ο τύπος εξαρτάται από την τιμή ν. Ο έλεγχος ισότητας μεταξύ εξαρτώμενων τύπων σε ένα πρόγραμμα μπορεί να απαιτεί υπολογισμούς. Αν επιτραπεί η χρήση οποιονδήποτε τιμών στους εξαρτώμενους τύπους, τότε ο έλεγχος ισότητας τύπων μπορεί να περιέχει έλεγχο για το αν δύο τυχαία προγράμματα παράγουν το ίδιο αποτέλεσμα. Τότε ο γίνεται μη αποφασίσιμο πρόβλημα. Απόρροια του είναι ότι μπορούν να κατασκευαστούν τύποι που περιγράφουν οσοδήποτε πολύπλοκες μαθηματικές ιδιότητες. Αν ο χρήστης μπορεί να δώσει μια ότι ένας τύπος είναι κατοικήσιμος (δηλαδή ότι υπάρχει τιμή τέτοιου τύπου), τότε ένας μεταγλωττιστής μπορεί να ελέγξει την απόδειξη και να την μετατρέψει σε εκτελέσιμο κώδικα που υπολογίζει την τιμή ακολουθώντας την κατασκευή. Η δυνατότητα ελέγχου αποδείξεων καθιστά τις γλώσσες με εξαρτώμενους τύπους στενά συνδεδεμένες με . Η πλευρά παραγωγής κώδικα αποτελεί μια ισχυρή προσέγγιση στην , αφού ο κώδικας απορρέει απευθείας από μια μηχανικά επαληθευμένη μαθηματική απόδειξη. (el)
  • 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. Two common examples of dependent types are dependent functions and dependent pairs. The return type of a dependent function may depend on the value (not just type) of one of its arguments. For instance, a function that takes a positive integer may return an array of length , where the array length is part of the type of the array. (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 of which the type depends on the first value. Sticking with the array example, a dependent pair may be used to pair an array with its length in a type-safe way. 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 et Gallina (de l'assistant de preuve Coq) sont des exemples de langages à type dépendant. (fr)
  • 依存型 (いぞんがた、英: dependent type) とは、計算機科学と論理学において、値に依存する型のことである。数学の型理論の表現形式と計算機科学における型システムの特徴を併せ持つ。においては、全称量化子や存在量化子のような論理学における量化子をエンコードするために依存型が用いられている。、Agda、、などのいくつかの関数型プログラミング言語では、依存型を使った非常に表現力の強い型によって、バグを防止している。 依存型の中でも、依存関数と依存ペアは特によく使われている。依存関数の戻り値の型は、引数の型だけではなく引数の値に応じて変化する。例えば、整数"n"を引数に取る依存関数は長さ"n"の配列を返すことができる。 (これは、型そのものを引数として取ることができるというポリモーフィズムとは別の概念である。) 依存ペアでは、2番目の型が1番目の値に応じて変化する。依存ペアを使うと、2番目の値が1番目の値よりも大きいような整数の対をエンコードすることができる。 依存型を入れた型システムは、より複雑になる。プログラム中に出現する2つの依存型が等しいかどうかを判定するとき、プログラムの一部を実行する必要があるかもしれない。特に、依存型に任意の式を含めることが許される場合、型の同値性判定は任意に与えられた2個のプログラムが同じ結果をもたらすかどうかを判定する問題を含んでしまう。したがって、この場合ははとなってしまう。 (ja)
  • 在计算机科学和逻辑中,依赖类型(或依存类型,dependent type)是指依赖于值的类型,其理论同时包含了数学基础中的类型论和计算机编程中用以减少程序错误的类型系统两方面。在 Per Martin-Löf 的直觉类型论中,依赖类型可对应于谓词逻辑中的全称量词和存在量词;在依赖类型函数式编程语言如 ATS、Agda、、、F* 和 Idris 中,依赖类型系统通过极其丰富的类型表达能力使得程序规范得以借助类型的形式被检查,从而有效减少程序错误。 依赖类型的两个常见实例是依赖函数类型(又称依赖乘积类型、Π-类型)和依赖值对类型(又称依赖总和类型、Σ-类型)。一个依赖类型函数的返回值类型可以依赖于某个参数的具体值,而非仅仅参数的类型,例如,一个输入参数为整型值n的函数可能返回一个长度为n的数组;一个依赖类型值对中的第二个值可以依赖于第一个值,例如,依赖类型可表示这样的类型:它由一对整数组成,其中的第二个数总是大于第一个数。 依赖类型增加了类型系统的复杂度。由于确定两个依赖于值的类型的等价性需要涉及具体的计算,若允许在依赖类型中使用任意值的话,其类型检查将会成为不可判定问题;换言之,无法确保程序的类型检查一定会停机。 由于Curry-Howard同构揭示了程序语言的类型论与证明论的直觉逻辑之间的紧密关联性,以依赖类型系统为基础的编程语言大多同时也作为构造证明与可验证程序的辅助工具而存在,如 Coq 和 Agda(但并非所有证明辅助工具都以类型论为基础);近年来,一些以通用和系统编程为目的的编程语言被设计出来,如 Idris。 一些以证明辅助为主要目的的编程语言采用强函数式编程(total functional programming),这消除了停机问题,同时也意味着通过它们自身的核心语言无法实现任意无限递归,不是图灵完全的,如 Coq 和 Agda;另外一些依赖类型编程语言则是图灵完全的,如 Idris、由 ML 衍生而来的 ATS 和 由 F# 衍生而来的 F*。 (zh)
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 1949487 (xsd:integer)
dbo:wikiPageLength
  • 22514 (xsd:integer)
dbo:wikiPageRevisionID
  • 979778334 (xsd:integer)
dbo:wikiPageWikiLink
dbp:id
  • dependent+product (en)
  • dependent+product+type (en)
  • dependent+sum (en)
  • dependent+sum+type (en)
  • dependent+type (en)
  • dependent+type+theory (en)
dbp:title
  • dependent product (en)
  • dependent product type (en)
  • dependent sum (en)
  • dependent sum type (en)
  • dependent type (en)
  • dependent type theory (en)
dbp:wikiPageUsesTemplate
dct:subject
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 et Gallina (de l'assistant de preuve Coq) sont des exemples de langages à type dépendant. (fr)
  • Závislostní typ je v teorii typů typ závisející na konkrétní hodnotě. Obecně se rozlišuje mezi závislostními typy součinovými a součtovými. Je-li nějaký typ z univerza typů, pak je součinový závislostní typ,přičemž je typ závisející na hodnotě .Naopak je součtový závislostní typ. Na lze nahlížet jako na funkci přiřazující hodnotám (typu ) typy (z ). Je-li konstantní, odpovídají součinové typyfunkčním typům () a součtové typy kartézskému součinu(). (cs)
  • Στην επιστήμη των υπολογιστών και την , ένας εξαρτώμενος τύπος είναι ένας τύπος που εξαρτάται από μία τιμή. Οι εξαρτώμενοι τύποι διαδραματίζουν κεντρικό ρόλο στην και στον σχεδιασμό σαν την , την Agda και την . Ένα παράδειγμα είναι ο τύπος των ν-άδων από πραγματικούς αριθμούς. Αυτός είναι ένας εξαρτώμενος τύπος επειδή ο τύπος εξαρτάται από την τιμή ν. (el)
  • 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. (en)
  • 依存型 (いぞんがた、英: dependent type) とは、計算機科学と論理学において、値に依存する型のことである。数学の型理論の表現形式と計算機科学における型システムの特徴を併せ持つ。においては、全称量化子や存在量化子のような論理学における量化子をエンコードするために依存型が用いられている。、Agda、、などのいくつかの関数型プログラミング言語では、依存型を使った非常に表現力の強い型によって、バグを防止している。 依存型の中でも、依存関数と依存ペアは特によく使われている。依存関数の戻り値の型は、引数の型だけではなく引数の値に応じて変化する。例えば、整数"n"を引数に取る依存関数は長さ"n"の配列を返すことができる。 (これは、型そのものを引数として取ることができるというポリモーフィズムとは別の概念である。) 依存ペアでは、2番目の型が1番目の値に応じて変化する。依存ペアを使うと、2番目の値が1番目の値よりも大きいような整数の対をエンコードすることができる。 (ja)
  • 在计算机科学和逻辑中,依赖类型(或依存类型,dependent type)是指依赖于值的类型,其理论同时包含了数学基础中的类型论和计算机编程中用以减少程序错误的类型系统两方面。在 Per Martin-Löf 的直觉类型论中,依赖类型可对应于谓词逻辑中的全称量词和存在量词;在依赖类型函数式编程语言如 ATS、Agda、、、F* 和 Idris 中,依赖类型系统通过极其丰富的类型表达能力使得程序规范得以借助类型的形式被检查,从而有效减少程序错误。 依赖类型的两个常见实例是依赖函数类型(又称依赖乘积类型、Π-类型)和依赖值对类型(又称依赖总和类型、Σ-类型)。一个依赖类型函数的返回值类型可以依赖于某个参数的具体值,而非仅仅参数的类型,例如,一个输入参数为整型值n的函数可能返回一个长度为n的数组;一个依赖类型值对中的第二个值可以依赖于第一个值,例如,依赖类型可表示这样的类型:它由一对整数组成,其中的第二个数总是大于第一个数。 依赖类型增加了类型系统的复杂度。由于确定两个依赖于值的类型的等价性需要涉及具体的计算,若允许在依赖类型中使用任意值的话,其类型检查将会成为不可判定问题;换言之,无法确保程序的类型检查一定会停机。 (zh)
rdfs:label
  • Závislostní typ (cs)
  • Εξαρτώμενος τύπος (el)
  • Dependent type (en)
  • Type dépendant (fr)
  • 依存型 (ja)
  • 依赖类型 (zh)
rdfs:seeAlso
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
is dbo:wikiPageDisambiguates of
is dbo:wikiPageRedirects of
is dbo:wikiPageWikiLink of
is dbp:typing of
is rdfs:seeAlso of
is foaf:primaryTopic of