Википедия

Конструктор типов: различия между версиями

Интерактивная навигация по истории
[отпатрулированная версия][отпатрулированная версия]
← Предыдущая правкаСледующая правка →
Содержимое удалено Содержимое добавлено
ВизуальныйВики-текст
м →‎Пример: стилевые правки
доделка
Строка 1:
'''Конструктор типа''' вВ [[язык программирования|языках программирования]] и [[теория типов|теории типов]] —, '''конструктор типа''' представляет собой конструкцияконструкцию [[система типов|типизированного]] [[формальный язык|формального языка]], которая строит новые типы из старых. Примерами типичных конструкторов типов служат {{iw|тип-произведение|типы-произведения|en|product type}}, {{iw|Функциональный тип|функциональные типы|en|Function type}} и [[Список (информатика)|списки]]. [[Примитивный тип|Примитивные типы]] представляются конструкторами типов нулевой [[арность|арности]].
 
== Пример ==
 
Конструкторы типов являются важным элементов языков, [[Система типов Хиндли — Милнера|типизированных по Хиндли  — Милнеру]], где они представляют собой определяемые функции с пустым телом.
 
Например, простейшую структуру [[XML]]-документа можно определить следующим образом:
Строка 9:
datatype simple_xml = Empty
| Word of string
| Tagged of { tag: string, contents:* simple_xml list }
</source>
Это определение вводит в программу четыре идентификатора: [[алгебраический тип данных]] <code>simple_xml</code> и три его конструктора: [[арность|нуль-арный]] <code>Empty</code>, и два унарных —унарный <code>Word</code> и бинарный <code>Tagged</code>. Последний конструктор принимает одиндва параметр,параметра (в данном случае в являющийсявиде [[Записькортеж (тип данныхинформатика)|записьюкортежа]]), которую составляют два поля, второевторой из которых имеет тип <code>simple_xml list</code> (то естьт.е. [[Список (информатика)|список]] объектов определяемого здесь типа). Таким образом, <code>simple_xml</code>). Таким образом, определяемый типпредставляет являетсясобой {{iw|Рекурсивныйрекурсивный тип данных|рекурсивным|en|Recursive data type}}.
 
Конструкторы типов обладают всеми правами функций (например, конструктор <code>Word</code> имеет {{iw|функциональный тип||en|Function type}} {{nowrap|«<code>string -> simple_xml</code>}}»), и в частности, могут использоваться в [[абстракция функций|абстракции функций]]:.
<source lang=ocaml>
fun listOfWords s =
Строка 23:
Empty => ""
| Word s => s ^ " "
| Tagged {(tag, contents}) => scat [ "<",tag,">", scat (map toString contents), "</",tag,">" ]
end
</source>
В теле функции <code>listOfWords</code> можно видеть как конструктор типа <code>Word</code> передаётся в качестве параметра функции [[map|<code>map</code>]], и та применяет его к каждому элементу списка строк, который она получает вторым параметром. ЭтотСписок списокстрок, в свою очередь, получен разбиением на слова (токенизацией) строки, полученной нафункцией входе<code>listOfWords</code>. ТакимПрименение конструктора типа <code>Word</code> к каждой строке порождает новый объект типа <code>simple_xml</code> — таким образом, результатом функции <code>listOfWords</code> будет [[Список (информатика)|список]] объектов типа <code>simple_xml</code>. Это подтверждается её {{iw|Функциональный тип|функциональным типом|en|Function type}}, который [[вывод типов|выводит]] компилятор: {{nowrap|«<code>string -> simple_xml list</code>}}». Соответственно, результат функции может непосредственно использоваться в качестве параметра для другого конструктора типа  — <code>Tagged</code>  — что породит новый объект типа <code>simple_xml</code>:
<source lang=ocaml>
fun mkXmlFile s = Tagged { tag =( "main", contents = listOfWords s })
</source>
Таким образом, [[XML]]-документ строится посредством рекурсивной композиции конструкторов типа. Например, документ
<source lang=xml>
<main>Jackdaws love my big sphinx of quartz</main>
</source>
будет представлен в программе такой [[Структура данных|структурой данных]]:
<source lang=ocaml>
Tagged ( "main", [Word "Jackdaws", Word "love", Word "my", Word "big", Word "sphinx", Word "of", Word "quartz"] )
</source>
 
== Теория ==
 
Например, [[Просто типизированное лямбда-исчисление]] можно рассматривать как язык с единственным конструктором типа  — конструктором функционального типа. Типы-произведения в [[типизированное лямбда-исчисление|типизированном лямбда-исчислении]] в целом могут рассматриваться как встроенные посредством [[каррирование|каррирования]].
<!--
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 ''[[Kind (type theory)|kinds]]''.
 
По сути, конструктор типа представляет собой [[арность|''<code>n</code>''-арный]] '''ти́повый оператор''' ({{lang-en|type operator}}, оператор над типами), принимающий на входе ноль или более типов, и возвращающий другой тип. При использовании [[каррирование|каррирования]] ''<code>n</code>''-арный ти́повый оператор может быть представлен последовательным применением унарных ти́повых операторов. Следовательно, ти́повые операторы можно рассматривать как [[просто типизированное лямбда-исчисление]], имеющее единственный тип, обычно обозначаемый * (читается «''тип''»), являющийся типом всех типов в нижележащем языке, которые в этом случае можно называть ''характерными типами'', чтобы отличать их от типов ти́повых операторов в их собственном исчислении — {{iw|Род (теория типов)|'''родов типов'''|en|Kind (type theory)}}.
Instituting a simply typed lambda calculus over the type operators results in more than just a formalization of type constructors though. Higher-order type operators become possible. (See [[Kind (type theory)#Examples|Kind (type theory)]] for some examples.) Type operators correspond to the 2nd axis in the [[lambda cube]], leading to the simply typed lambda-calculus with type operators, λ<sub>ω</sub>; while this is not so well known, combining type operators with polymorphic lambda calculus ([[system F]]) yields [[system F-omega]].
 
-->
Однако, использование ти́повых операторов в качестве обоснования просто типизированного лямбда-исчисления — это больше, чем просто формализация — это делает возможными ти́повые операторы высших порядков (см. {{iw|Род (теория типов)#Примеры|примеры родов типов'''|en|Kind (type theory)#Examples}}). Ти́повые операторы соотносятся со второй осью в [[Лямбда-куб|лямбда-кубе]], приводя к просто типизированному лямбда-исчислению с ти́повыми операторами — λ<sub>ω</sub>. Комбинация ти́повых операторов с полиморфным лябда-исчислением ({{nowrap|[[Система F|системой F]]}}) порождает {{iw|Система F-омега|{{nowrap|систему Fω}}|en|System F-omega}}.
{{В планах}}
 
== См. также ==
* [[Алгебраический тип данных]]
* {{iw|Рекурсивный тип данных||en|Recursive data type}}
* {{iw|Род (теория типов)||en|Kind (type theory)}}
 
<!--
 
== Примечания ==
{{примечания}}
-->
 
== Ссылки ==
* {{статья
* {{Cite book|last=Pierce|first=Benjamin|title=Types and Programming Languages|publisher=MIT Press|date=2002|id=ISBN 0-262-16209-1}}, chapter 29, «Type Operators and Kinding»
|автор = Benjamin Pierce
* [[P.T. Johnstone]], ''Sketches of an Elephant'', p. 940
|заглавие = Types and Programming Languages
|издательство = MIT Press
|год = 2002
|ISBN = 0-262-16209-1
|ссылка =
|ref =
}}, глава 29, "Type Operators and Kinding"
* {{статья
|автор = {{iw|P.T. Johnstone}}
|заглавие = Sketches of an Elephant
|издательство =
|страницы = 940
|год =
|ссылка =
|ref =
}}
 
{{Типы данных}}
 
<!--
[[Категория:Информатика]]
[[Категория:Формальные методы]]
Строка 63 ⟶ 83 :
[[Категория:Типы данных]]
[[Категория:Определение соответствия]]
-->
 
{{compu-prog-stub}}
Источник — https://ru.wikipedia.org/wiki/Конструктор_типов