| dbo:abstract
|
- Στην περιοχή της μαθηματικής λογικής και της επιστήμης των υπολογιστών γνωστής ως θεωρία τύπων, ένας κατασκευαστής τύπων είναι ένα χαρακτηριστικό μιας τυπικής γλώσσας με τύπους, το οποίο δημιουργεί νέους τύπους από παλιούς. Οι τυπικοί κατασκευαστές τύπων που συναντώνται είναι οι , οι , οι power types και οι . Οι θεωρούνται κατασκευαστές τύπων τάξης μηδέν. Νέοι τύποι μπορούν να οριστούν συνθέτοντας αναδρομικά κατασκευαστές τύπων Για παράδειγμα, ο λ-λογισμός με απλούς τύπους μπορεί να θεωρηθεί ως μία γλώσσα με ένα μοναδικό κατασκευαστή τύπων— τον κατασκευαστή συναρτήσεων. Οι τύποι γινομένου μπορούν γενικά να θεωρηθούν "ενσωματωμένοι" στον λ-λογισμό με τύπους μέσω του . Αφηρημένα, ένας κατασκευαστής τύπου είναι ένα τελεστής τύπων τάξης n που δέχεται ως όρισμα μηδέν ή περισσότερους τύπους, και επιστρέφει έναν άλλον τύπο. Χρησιμοποιώντας το currying, οι τελεστές τύπων τάξης n μπορούν να (ξανα)γραφούν ως μια ακολουθία εφαρμογών μοναδιαίων τελεστών τύπων. Ως εκ τούτου, μπορούμε να δούμε τους τελεστές τύπων ως λ-λογισμός με απλούς τύπους, ο οποίος έχει μόνο έναν βασικό τύπο που συνήθως συμβολίζεται με *,και προφέρεται "τύπος", ο οποίος είναι ο τύπος όλων των τύπων στην γλώσσα, οι όποίοι ονομάζονται σωστοί τύποι για να τους διακρίνουμε από τους τύπους των τύπων των τελεστών τύπων στον δικό τους λογισμό, που ονομάζονται kinds. Η καθιέρωση ενός λ-λογισμού με απλούς τύπους πάνω από τους τελεστές τύπων οδηγεί σε κάτι περισσότερο από απλά ένα φορμαλισμό των κατασκευαστών τύπων. Η χρήση τελεστών τύπων υψηλής τάξης γίνεται δυνατή. Οι τελεστές τύπων αντιστοιχούν στον δεύτερο άξονα του , οδηγώντας στον λαμδα λογισμό με απλούς τύπους με τελεστές τύπων, λω; καθώς αυτό δεν είναι τόσο γνωστό, συνδυάζοντας τελεστές τύπων με πολυμορφικό λ-λογισμό (Σύστημα F) οδηγεί στο . (el)
- In the area of mathematical logic and computer science known as type theory, a type constructor is a feature of a typed formal language that builds new types from old ones. Basic types are considered to be built using nullary type constructors. Some type constructors take another type as an argument, e.g., the constructors for product types, function types, power types and list types. New types can be defined by recursively composing type constructors. For example, simply typed lambda calculus can be seen as a language with a single non-basic type constructor—the function type constructor. Product types can generally be considered "built-in" in typed lambda calculi via currying. Abstractly, a type constructor is an n-ary type operator taking as argument zero or more types, and returning another type. Making use of currying, n-ary type operators can be (re)written as a sequence of applications of unary type operators. Therefore, we can view the type operators as a simply typed lambda calculus, which has only one basic type, usually denoted , and pronounced "type", which is the type of all types in the underlying language, which are now called proper types in order to distinguish them from the types of the type operators in their own calculus, which are called kinds. Type operators may bind type variables. For example, giving the structure of the simply-typed λ-calculus at the type level requires binding, or higher-order, type operators. These binding type operators correspond to the 2nd axis of the λ-cube, and type theories such as the simply-typed λ-calculus with type operators, λω. Combining type operators with the polymorphic λ-calculus (System F) yields System Fω. (en)
- В теории типов, конструктор типов представляет собой конструкцию полиморфно типизируемого формального языка, которая строит новые типы из старых. Примерами типичных конструкторов типов служат типы-произведения, функциональные типы и списки. Примитивные типы представляются конструкторами типов нулевой арности. Новые типы могут строиться посредством рекурсивной композиции конструкторов типов. Просто типизированное лямбда-исчисление можно рассматривать как язык с единственным конструктором типов — конструктором функционального типа. Каррирование позволяет рассматривать типы-произведения в типизированном лямбда-исчислении как встроенные. По сути, конструктор типов представляет собой n-арный ти́повый оператор (англ. type operator, оператор над типами), принимающий на входе ноль или более типов, и возвращающий другой тип. При использовании каррирования n-арный ти́повый оператор может быть представлен последовательным применением унарных ти́повых операторов. Следовательно, ти́повые операторы можно рассматривать как просто типизированное лямбда-исчисление, имеющее единственный тип, обычно обозначаемый «*» (читается «тип»), являющийся типом всех типов в нижележащем языке, которые в этом случае можно называть характерными типами, чтобы отличать их от типов ти́повых операторов в их собственном исчислении — родо́в типов. Однако, использование ти́повых операторов в качестве обоснования просто типизированного лямбда-исчисления — это больше, чем просто формализация — это делает возможными ти́повые операторы высших порядков (см. Род (теория типов)#Примеры, полиморфизм в высших родах). Ти́повые операторы соотносятся со второй осью в лямбда-кубе, приводя к просто типизированному лямбда-исчислению с ти́повыми операторами — λω. Комбинация ти́повых операторов с полиморфным лямбда-исчислением (системой F) порождает . Конструкторы типов интенсивно используются в полнотиповом программировании. (ru)
- 类型构造器也称类型构造子，是把若干已知类型组合成一新类型的手段。可以看作是类型的构造函数。打个比方，如果说普通的函数操作变量并产生新值，那么类型构造器就是操作类型返回新类型。 例如，数组 T[] 是若干相同类型 T 元素的有序集合，我们说从 T 类型构造出“T 的数组”这一类型的类型构造器是（后缀）[]、即“加上数组”。 (zh)
- У галузі математичної логіки і інформатики відомій як теорія типів, конструктор типу — це властивість характерна типізованим формальним мовам, за допомогою якої нові типи створюються з уже наявних. Вважається, що конструюються за допомогою конструкторів нульової арності. Деякі конструктори типів приймають інші типи як аргументи, наприклад, типи-добутки, функціональні типи, списки. Нові типи можна визначити через рекурсивну композицію конструкторів типів. Наприклад, можна розглядати як мову із єдиним конструктором типів—конструктором функціонального типу. Каррування дозволяє розглядати типи-добутки як вбудовані у типізованому лямбда численні. Абстрактно, конструктор типів є n-арним оператор над типами, що приймає нуль або більше типів і повертає інший тип. Через використання каррування, n-арний оператор над типами можна записати як послідовність застосувань унарного оператора над типами. Отже, ми можемо розглядати оператор над типами як просто типізоване лямбда числення, яке має лише один примітивний тип, зазвичай позначуваний як «*» (читається «тип»), що є типом усіх типів у нижчий мові, які називають властивими типами, щоб відрізняти їх від типів операторів над типами у їх власному численні — . Використання простого лямбда числення над операторами над типами, призводить до більш ніж просто формалізації конструкторів типів. Це уможливлює оператори типами вищого порядку. Оператори над типами відповідають другій осі лямбда-куба, приводячи до просто типізованого лямбда числення з операторами над типами, λω; поєднання операторів над типами із поліморфним лямбда численням породжує систему Fω. (uk)
|
| rdfs:comment
|
- 类型构造器也称类型构造子，是把若干已知类型组合成一新类型的手段。可以看作是类型的构造函数。打个比方，如果说普通的函数操作变量并产生新值，那么类型构造器就是操作类型返回新类型。 例如，数组 T[] 是若干相同类型 T 元素的有序集合，我们说从 T 类型构造出“T 的数组”这一类型的类型构造器是（后缀）[]、即“加上数组”。 (zh)
- Στην περιοχή της μαθηματικής λογικής και της επιστήμης των υπολογιστών γνωστής ως θεωρία τύπων, ένας κατασκευαστής τύπων είναι ένα χαρακτηριστικό μιας τυπικής γλώσσας με τύπους, το οποίο δημιουργεί νέους τύπους από παλιούς. Οι τυπικοί κατασκευαστές τύπων που συναντώνται είναι οι , οι , οι power types και οι . Οι θεωρούνται κατασκευαστές τύπων τάξης μηδέν. Νέοι τύποι μπορούν να οριστούν συνθέτοντας αναδρομικά κατασκευαστές τύπων (el)
- In the area of mathematical logic and computer science known as type theory, a type constructor is a feature of a typed formal language that builds new types from old ones. Basic types are considered to be built using nullary type constructors. Some type constructors take another type as an argument, e.g., the constructors for product types, function types, power types and list types. New types can be defined by recursively composing type constructors. (en)
- У галузі математичної логіки і інформатики відомій як теорія типів, конструктор типу — це властивість характерна типізованим формальним мовам, за допомогою якої нові типи створюються з уже наявних. Вважається, що конструюються за допомогою конструкторів нульової арності. Деякі конструктори типів приймають інші типи як аргументи, наприклад, типи-добутки, функціональні типи, списки. Нові типи можна визначити через рекурсивну композицію конструкторів типів. (uk)
- В теории типов, конструктор типов представляет собой конструкцию полиморфно типизируемого формального языка, которая строит новые типы из старых. Примерами типичных конструкторов типов служат типы-произведения, функциональные типы и списки. Примитивные типы представляются конструкторами типов нулевой арности. Новые типы могут строиться посредством рекурсивной композиции конструкторов типов. Конструкторы типов интенсивно используются в полнотиповом программировании. (ru)
|