Тип-произведение

Поделись знанием:
Перейти к: навигация, поиск

Тип-произведение (также Π-тип, произведение типов; англ. product type) — конструкция в языках программирования и интуиционистской теории типов[en], тип данных, построенный как декартово произведение исходных типов; другими словами — кортеж типов, или «кортеж как тип»[⇨]. Использованные типы и порядок их следования определяют сигнатуру[en] типа-произведения; порядок следования объектов в создаваемом кортеже сохраняется на протяжении его времени жизни согласно заданной сигнатуре.

Например, если типы A и B представляют собой множества значений a и b соответственно, то составленное из них декартово произведение записывается как A×B, и полученный тип-произведение представляет собой всё множество возможных пар (a,b).





Теоретическое и прикладное значение

В языках, использующих вызов по значению, тип-произведение может интерпретироваться как произведение в категории типов. В соответствии Карри-Ховарда типы-произведения соответствуют конъюнкции в логике (операции AND).

Частный случай произведения двух типов часто называют «парой» или более точно «упорядоченной парой». Произведение произвольного конечного количества типов называется «n-арным типом-произведением» или «кортежем из n типов». В русскоязычной литературе также присутствует вариант наименования «упорядоченная энка» (обобщение от «двойка», «тройка» и т. д.), лингвистически построенный по аналогии с английским термином «tuple» (см. кортеж  (англ.)).

Вырожденная форма типа-произведения — произведение нуля типов — представляет собой единичный тип[en] (англ. unit type, «тип юнит»), то есть тип, представленный единственным значением. Системы типов некоторых языков (например, Python) могут предусматривать один или несколько уникальных единичных типов, не совместимых с типом кортежа из нуля элементов.

Типы-произведения встроены в большинство функциональных языков программирования. Например, произведение type1× … × typen записывается как type1 * * typen в ML или как (type1,,typen) в Haskell. В обоих языках кортежи записываются как (v1,,vn) и их компоненты извлекаются посредством сопоставления с образцом. В дополнение к этому большинство функциональных языков предоставляет алгебраические типы данных, расширяющие понятия как типа-произведения, так и типа-суммы. Алгебраические типы, заданные единственным конструктором, изоморфны типам-произведениям.

Кортеж типов как чистое воплощение типа-произведения служит формальным обоснованием для более часто встречающегося в языках составного типа «запись»[⇨], хотя в некоторых языках реализованы оба контейнера. Разница обычно заключается в том, что кортежи задают и сохраняют порядок следования своих компонентов в памяти ЭВМ (это важно при обращении к их компонентам посредством адресной арифметики), но не предоставляют возможности доступа к ним посредством квалифицированных идентификаторов, а записи, наоборот, определяют идентификаторы, но не определяют порядок следования. Однако, есть исключения:

  • в языке Standard ML кортежи значений с целью оптимизации размещения в памяти реализуются посредством записей, у которых в качестве идентификаторов компонентов используются их порядковые номера в кортеже; адресная арифметика недоступна; типы перестают существовать после компиляции; и требуемый порядок следования принуждается только при межъязыковом взаимодействии[en].
  • в языке Си тип данных «структура» (struct)[⇨] соединяет в себе свойства записей и кортежей, то есть позволяет назначать компонентам идентификаторы и одновременно гарантирует сохранение порядка их следования. Кроме того, в отличие от записей и кортежей, структуры в Си могут содержать указатели на собственные объекты, что позволяет непосредственно строить рекурсивные типы данных[en].

Реализация в языках программирования

Кортежи

Записи

Во многих языках запись представляет собой агрегатный тип данных, инкапсулирующий без сокрытия набор значений[en] различных типов.

В одних языках (например, в Си или Паскале) порядок размещения значений в памяти задаётся при определении типа и сохраняется на протяжении времени жизни объектов, что даёт возможность косвенного доступа (например, через указатели); в других языках (например, в ML) порядок размещения не определён, так что доступ к значениям возможен только по квалифицированному идентификатору. В некоторых языках, хотя порядок следования и сохраняется, но выравнивание контролируется компилятором, так что использование адресной арифметики может оказаться платформенно-зависимым. Некоторые языки позволяют присваивание между экземплярами разных записей, игнорируя различия в идентификаторах компонентов записей, и основываясь только на порядке следования. Другие языки, напротив, учитывают только совпадение имён, разрешая различия в порядке их определения.

Впервые записи были представлены в языке Кобол, где они имели довольно сложную нотацию. При проверке согласования типов, Кобол учитывает только совпадение имён полей записей и не учитывает совпадение порядка их следования.

Кортежи служат формальным обоснованием записей в теории типов. В то же время, в языках кортежи временами могут реализовываться посредством записей, использующих в качестве идентификаторов индексные номера полей в получаемом кортеже.

Структуры в Си

В языке Си, структура (struct) — композитный тип данных, инкапсулирующий без сокрытия набор значений[en] различных типов. Порядок размещения значений в памяти задаётся при определении типа и сохраняется на протяжении времени жизни объектов, что даёт возможность косвенного доступа (например, через указатели)

Напишите отзыв о статье "Тип-произведение"

Примечания

Ссылки

  • [homotopytypetheory.org/2013/06/20/the-hott-book/ Homotopy Type Theory: Univalent Foundations of Mathematics, section 1.5] (англ.). — The Univalent Foundations Program, Institute for Advanced Study.
  • Роберт Харпер[en]. Введение в Стандартный ML. — Carnegie Mellon University, 1986. — 97 с. — ISBN PA 15213-3891.
  • Эммануэль Шалуа, Паскаль Манури, Бруно Пагано. [bookre.org/reader?file=1251401 Разработка программ с помощью Objective Caml]. — 2007.

Отрывок, характеризующий Тип-произведение

Х
8 го сентября в сарай к пленным вошел очень важный офицер, судя по почтительности, с которой с ним обращались караульные. Офицер этот, вероятно, штабный, с списком в руках, сделал перекличку всем русским, назвав Пьера: celui qui n'avoue pas son nom [тот, который не говорит своего имени]. И, равнодушно и лениво оглядев всех пленных, он приказал караульному офицеру прилично одеть и прибрать их, прежде чем вести к маршалу. Через час прибыла рота солдат, и Пьера с другими тринадцатью повели на Девичье поле. День был ясный, солнечный после дождя, и воздух был необыкновенно чист. Дым не стлался низом, как в тот день, когда Пьера вывели из гауптвахты Зубовского вала; дым поднимался столбами в чистом воздухе. Огня пожаров нигде не было видно, но со всех сторон поднимались столбы дыма, и вся Москва, все, что только мог видеть Пьер, было одно пожарище. Со всех сторон виднелись пустыри с печами и трубами и изредка обгорелые стены каменных домов. Пьер приглядывался к пожарищам и не узнавал знакомых кварталов города. Кое где виднелись уцелевшие церкви. Кремль, неразрушенный, белел издалека с своими башнями и Иваном Великим. Вблизи весело блестел купол Ново Девичьего монастыря, и особенно звонко слышался оттуда благовест. Благовест этот напомнил Пьеру, что было воскресенье и праздник рождества богородицы. Но казалось, некому было праздновать этот праздник: везде было разоренье пожарища, и из русского народа встречались только изредка оборванные, испуганные люди, которые прятались при виде французов.
Очевидно, русское гнездо было разорено и уничтожено; но за уничтожением этого русского порядка жизни Пьер бессознательно чувствовал, что над этим разоренным гнездом установился свой, совсем другой, но твердый французский порядок. Он чувствовал это по виду тех, бодро и весело, правильными рядами шедших солдат, которые конвоировали его с другими преступниками; он чувствовал это по виду какого то важного французского чиновника в парной коляске, управляемой солдатом, проехавшего ему навстречу. Он это чувствовал по веселым звукам полковой музыки, доносившимся с левой стороны поля, и в особенности он чувствовал и понимал это по тому списку, который, перекликая пленных, прочел нынче утром приезжавший французский офицер. Пьер был взят одними солдатами, отведен в одно, в другое место с десятками других людей; казалось, они могли бы забыть про него, смешать его с другими. Но нет: ответы его, данные на допросе, вернулись к нему в форме наименования его: celui qui n'avoue pas son nom. И под этим названием, которое страшно было Пьеру, его теперь вели куда то, с несомненной уверенностью, написанною на их лицах, что все остальные пленные и он были те самые, которых нужно, и что их ведут туда, куда нужно. Пьер чувствовал себя ничтожной щепкой, попавшей в колеса неизвестной ему, но правильно действующей машины.
Пьера с другими преступниками привели на правую сторону Девичьего поля, недалеко от монастыря, к большому белому дому с огромным садом. Это был дом князя Щербатова, в котором Пьер часто прежде бывал у хозяина и в котором теперь, как он узнал из разговора солдат, стоял маршал, герцог Экмюльский.
Их подвели к крыльцу и по одному стали вводить в дом. Пьера ввели шестым. Через стеклянную галерею, сени, переднюю, знакомые Пьеру, его ввели в длинный низкий кабинет, у дверей которого стоял адъютант.
Даву сидел на конце комнаты над столом, с очками на носу. Пьер близко подошел к нему. Даву, не поднимая глаз, видимо справлялся с какой то бумагой, лежавшей перед ним. Не поднимая же глаз, он тихо спросил:
– Qui etes vous? [Кто вы такой?]
Пьер молчал оттого, что не в силах был выговорить слова. Даву для Пьера не был просто французский генерал; для Пьера Даву был известный своей жестокостью человек. Глядя на холодное лицо Даву, который, как строгий учитель, соглашался до времени иметь терпение и ждать ответа, Пьер чувствовал, что всякая секунда промедления могла стоить ему жизни; но он не знал, что сказать. Сказать то же, что он говорил на первом допросе, он не решался; открыть свое звание и положение было и опасно и стыдно. Пьер молчал. Но прежде чем Пьер успел на что нибудь решиться, Даву приподнял голову, приподнял очки на лоб, прищурил глаза и пристально посмотрел на Пьера.
– Я знаю этого человека, – мерным, холодным голосом, очевидно рассчитанным для того, чтобы испугать Пьера, сказал он. Холод, пробежавший прежде по спине Пьера, охватил его голову, как тисками.
– Mon general, vous ne pouvez pas me connaitre, je ne vous ai jamais vu… [Вы не могли меня знать, генерал, я никогда не видал вас.]
– C'est un espion russe, [Это русский шпион,] – перебил его Даву, обращаясь к другому генералу, бывшему в комнате и которого не заметил Пьер. И Даву отвернулся. С неожиданным раскатом в голосе Пьер вдруг быстро заговорил.
– Non, Monseigneur, – сказал он, неожиданно вспомнив, что Даву был герцог. – Non, Monseigneur, vous n'avez pas pu me connaitre. Je suis un officier militionnaire et je n'ai pas quitte Moscou. [Нет, ваше высочество… Нет, ваше высочество, вы не могли меня знать. Я офицер милиции, и я не выезжал из Москвы.]
– Votre nom? [Ваше имя?] – повторил Даву.
– Besouhof. [Безухов.]
– Qu'est ce qui me prouvera que vous ne mentez pas? [Кто мне докажет, что вы не лжете?]
– Monseigneur! [Ваше высочество!] – вскрикнул Пьер не обиженным, но умоляющим голосом.
Даву поднял глаза и пристально посмотрел на Пьера. Несколько секунд они смотрели друг на друга, и этот взгляд спас Пьера. В этом взгляде, помимо всех условий войны и суда, между этими двумя людьми установились человеческие отношения. Оба они в эту одну минуту смутно перечувствовали бесчисленное количество вещей и поняли, что они оба дети человечества, что они братья.
В первом взгляде для Даву, приподнявшего только голову от своего списка, где людские дела и жизнь назывались нумерами, Пьер был только обстоятельство; и, не взяв на совесть дурного поступка, Даву застрелил бы его; но теперь уже он видел в нем человека. Он задумался на мгновение.
– Comment me prouverez vous la verite de ce que vous me dites? [Чем вы докажете мне справедливость ваших слов?] – сказал Даву холодно.
Пьер вспомнил Рамбаля и назвал его полк, и фамилию, и улицу, на которой был дом.
– Vous n'etes pas ce que vous dites, [Вы не то, что вы говорите.] – опять сказал Даву.
Пьер дрожащим, прерывающимся голосом стал приводить доказательства справедливости своего показания.
Но в это время вошел адъютант и что то доложил Даву.
Даву вдруг просиял при известии, сообщенном адъютантом, и стал застегиваться. Он, видимо, совсем забыл о Пьере.
Когда адъютант напомнил ему о пленном, он, нахмурившись, кивнул в сторону Пьера и сказал, чтобы его вели. Но куда должны были его вести – Пьер не знал: назад в балаган или на приготовленное место казни, которое, проходя по Девичьему полю, ему показывали товарищи.
Он обернул голову и видел, что адъютант переспрашивал что то.
– Oui, sans doute! [Да, разумеется!] – сказал Даву, но что «да», Пьер не знал.
Пьер не помнил, как, долго ли он шел и куда. Он, в состоянии совершенного бессмыслия и отупления, ничего не видя вокруг себя, передвигал ногами вместе с другими до тех пор, пока все остановились, и он остановился. Одна мысль за все это время была в голове Пьера. Это была мысль о том: кто, кто же, наконец, приговорил его к казни. Это были не те люди, которые допрашивали его в комиссии: из них ни один не хотел и, очевидно, не мог этого сделать. Это был не Даву, который так человечески посмотрел на него. Еще бы одна минута, и Даву понял бы, что они делают дурно, но этой минуте помешал адъютант, который вошел. И адъютант этот, очевидно, не хотел ничего худого, но он мог бы не войти. Кто же это, наконец, казнил, убивал, лишал жизни его – Пьера со всеми его воспоминаниями, стремлениями, надеждами, мыслями? Кто делал это? И Пьер чувствовал, что это был никто.