Конструктор типов

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

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

Просто типизированное лямбда-исчисление можно рассматривать как язык с единственным конструктором типов — конструктором функционального типа. Каррирование позволяет рассматривать типы-произведения в типизированном лямбда-исчислении как встроенные.

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

Однако, использование ти́повых операторов в качестве обоснования просто типизированного лямбда-исчисления — это больше, чем просто формализация — это делает возможными ти́повые операторы высших порядков (см. примеры родов типов). Ти́повые операторы соотносятся со второй осью в лямбда-кубе, приводя к просто типизированному лямбда-исчислению с ти́повыми операторами — λω. Комбинация ти́повых операторов с полиморфным лябда-исчислением (системой F) порождает систему Fω[en].

Конструкторы типов интенсивно используются в полнотиповом программировании.





В языках программирования

В языках программирования семейства ML конструктор типов представляется функцией над типами — т.е. функцией, которая получает на входе одни типы и возвращает другие типы. Оптимизирующие компиляторы исполняют эти функции статически, т.е. на этапе компиляции[en] (см., например, MLton).

В классических диалектах ML (Standard ML, OCaml) для n-арных конструкторов типов используется нотация кортежей. В Haskell возможны каррированные конструкторы типов. Классические диалекты ML при конструировании новых типов используют постфиксный синтаксис (например, «int list»), а Haskell — префиксный («List Int»).

Standard ML

В современных реализациях Standard ML примитивные типы, такие как char, int, word, real, определены в модулях стандартной библиотеки (SML Basis) как нуль-арные конструкторы типов (подробнее см. управление разрядностью чисел в ML). Такие классические агрегатные типы как массивы и списки реализованы аналогично, но уже представляют собой унарные конструкторы типов vector (массивы неизменяемых элементов), array (массивы изменяемых элементов) и list.

В Standard ML для определения конструкторов типов есть две разные конструкции — type и datatype. Первая определяет псевдоним имеющегося конструктора типов или их композиции, вторая вводит новый алгебраический тип данных со своими конструкторами. Вновь определяемые конструкторы типов могут принимать любое количество аргументов. В качестве аргумента конструктора типов используется переменная типа. Типы, параметризованные одним и более аргументами, называются полиморфными; типы без аргументов — мономорфными.

datatype t0 = T of int * real             (* 0 аргументов *)
type 'a t1 = 'a * int                     (* 1 аргумент   *)
datatype ('a, 'b) t2 = A | B of 'a * 'b   (* 2 аргумента  *)
type ('a, 'b, 'c) t3 = 'a * ('b -> 'c)    (* 3 аргумента  *)

Здесь определено четыре конструктора типов: t0, t1, t2 и t3. Для создания объектов типов 'a t1 и 'a t2 необходимо вызывать их конструкторы T, A и B.

Пример композиции конструкторов типов, показывающий построение новых типов:

type t4 = t0 t1

Здесь в качестве фактического значения ти́повой переменной 'a конструктора типов t1 используется тип t0. Полученный тип представляет собой кортеж из двух элементов, из которых второй является целым числом, а первый был построен применением конструктора T к кортежу из целого и вещественного.

Более сложный пример:

type 'a t5 = ('a, 'a, 'a) t3 t1

Объектами типа t5 будут кортежи из двух элементов, первый из которых является частным случаем типа t3, у которого все три аргумента должны быть идентичными, а второй — целым числом.

Haskell

В Haskell для определения конструкторов типов есть уже три конструкции — type, data и newtype.

Конструкции type и data используются аналогично type и datatype в Standard ML, однако, имеются следующие отличия:

  • синтаксис префиксный (параметр указывается после конструктора);
  • синтаксис требует (а не рекомендует, как в большинстве языков) различать регистр в идентификаторах: компоненты слоя типов в языке (конструкторы типов, конструкторы значений, классы типов) должны начинаться только с заглавной буквы, а компоненты слоя значений — только со строчных;
  • переменные типа не должны отмечаться апострофами, но записываются также строчными буквами;
  • и конструкторы типов, и конструкторы значений могут быть каррированными.

Пример:

data Point a = Pt a a

На самом деле, во всех языках семейства ML конструкторы типов и конструкторы значений находятся в разных пространствах имён, поэтому в подобных случаях можно использовать один и тот же идентификатор:

data Point a = Point a a

В подобных случаях происходят некоторые потери производительности, так как конструктор значений применяется динамически. Замена абстрактного типа на псевдоним типа (определяемый через type) повышает эффективность, но снижает типобезопасность (так как становится невозможно контролировать уникальные свойства надстроенного типа, сужающие его применение относительно лежащего в его основе). Для решения этой дилемы в Haskell была добавлена конструкция newtype:

newtype Point a = Point a a

Определённый таким образом тип используется идентично тем, что были определены через data, но конструктор его значений (который может быть только один, в отличие от data) исполняется на этапе компиляции.


См.также

Напишите отзыв о статье "Конструктор типов"

Ссылки

  • Pierce, Benjamin C. [www.cis.upenn.edu/~bcpierce/tapl/ Types and Programming Languages]. — MIT Press, 2002. — ISBN 0-262-16209-1.
  • Лука Карделли[en], Peter Wegner [lucacardelli.name/Papers/OnUnderstanding.A4.pdf On Understanding Types, Data Abstraction, and Polymorphism] // ACM Computing Surveys. — New York, NY, USA: ACM, 1985. — Т. 17, вып. 4. — С. 471–523. — ISSN [www.sigla.ru/table.jsp?f=8&t=3&v0=0360-0300&f=1003&t=1&v1=&f=4&t=2&v2=&f=21&t=3&v3=&f=1016&t=3&v4=&f=1016&t=3&v5=&bf=4&b=&d=0&ys=&ye=&lng=&ft=&mt=&dt=&vol=&pt=&iss=&ps=&pe=&tr=&tro=&cc=UNION&i=1&v=tagged&s=0&ss=0&st=0&i18n=ru&rlf=&psz=20&bs=20&ce=hJfuypee8JzzufeGmImYYIpZKRJeeOeeWGJIZRrRRrdmtdeee88NJJJJpeeefTJ3peKJJ3UWWPtzzzzzzzzzzzzzzzzzbzzvzzpy5zzjzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzztzzzzzzzbzzzzzzzzzzzzzzzzzzzzzzzzzzzvzzzzzzyeyTjkDnyHzTuueKZePz9decyzzLzzzL*.c8.NzrGJJvufeeeeeJheeyzjeeeeJh*peeeeKJJJJJJJJJJmjHvOJJJJJJJJJfeeeieeeeSJJJJJSJJJ3TeIJJJJ3..E.UEAcyhxD.eeeeeuzzzLJJJJ5.e8JJJheeeeeeeeeeeeyeeK3JJJJJJJJ*s7defeeeeeeeeeeeeeeeeeeeeeeeeeSJJJJJJJJZIJJzzz1..6LJJJJJJtJJZ4....EK*&debug=false 0360-0300]. — DOI:10.1145/6041.6042.
  • Лука Карделли[en] [www.lucacardelli.name/Papers/TypefulProg.pdf Typeful programming] ( (англ.)) // IFIP State-of-the-Art Reports. — New York: Springer-Verlag, 1991. — Вып. Formal Description of Programming Concepts. — С. 431–507.
  • P.T. Johnstone[en] Sketches of an Elephant. — С. 940.

Отрывок, характеризующий Конструктор типов

Старики из самых значительных составляли центр кружков, к которым почтительно приближались даже незнакомые, чтобы послушать известных людей. Большие кружки составлялись около графа Ростопчина, Валуева и Нарышкина. Ростопчин рассказывал про то, как русские были смяты бежавшими австрийцами и должны были штыком прокладывать себе дорогу сквозь беглецов.
Валуев конфиденциально рассказывал, что Уваров был прислан из Петербурга, для того чтобы узнать мнение москвичей об Аустерлице.
В третьем кружке Нарышкин говорил о заседании австрийского военного совета, в котором Суворов закричал петухом в ответ на глупость австрийских генералов. Шиншин, стоявший тут же, хотел пошутить, сказав, что Кутузов, видно, и этому нетрудному искусству – кричать по петушиному – не мог выучиться у Суворова; но старички строго посмотрели на шутника, давая ему тем чувствовать, что здесь и в нынешний день так неприлично было говорить про Кутузова.
Граф Илья Андреич Ростов, озабоченно, торопливо похаживал в своих мягких сапогах из столовой в гостиную, поспешно и совершенно одинаково здороваясь с важными и неважными лицами, которых он всех знал, и изредка отыскивая глазами своего стройного молодца сына, радостно останавливал на нем свой взгляд и подмигивал ему. Молодой Ростов стоял у окна с Долоховым, с которым он недавно познакомился, и знакомством которого он дорожил. Старый граф подошел к ним и пожал руку Долохову.
– Ко мне милости прошу, вот ты с моим молодцом знаком… вместе там, вместе геройствовали… A! Василий Игнатьич… здорово старый, – обратился он к проходившему старичку, но не успел еще договорить приветствия, как всё зашевелилось, и прибежавший лакей, с испуганным лицом, доложил: пожаловали!
Раздались звонки; старшины бросились вперед; разбросанные в разных комнатах гости, как встряхнутая рожь на лопате, столпились в одну кучу и остановились в большой гостиной у дверей залы.
В дверях передней показался Багратион, без шляпы и шпаги, которые он, по клубному обычаю, оставил у швейцара. Он был не в смушковом картузе с нагайкой через плечо, как видел его Ростов в ночь накануне Аустерлицкого сражения, а в новом узком мундире с русскими и иностранными орденами и с георгиевской звездой на левой стороне груди. Он видимо сейчас, перед обедом, подстриг волосы и бакенбарды, что невыгодно изменяло его физиономию. На лице его было что то наивно праздничное, дававшее, в соединении с его твердыми, мужественными чертами, даже несколько комическое выражение его лицу. Беклешов и Федор Петрович Уваров, приехавшие с ним вместе, остановились в дверях, желая, чтобы он, как главный гость, прошел вперед их. Багратион смешался, не желая воспользоваться их учтивостью; произошла остановка в дверях, и наконец Багратион всё таки прошел вперед. Он шел, не зная куда девать руки, застенчиво и неловко, по паркету приемной: ему привычнее и легче было ходить под пулями по вспаханному полю, как он шел перед Курским полком в Шенграбене. Старшины встретили его у первой двери, сказав ему несколько слов о радости видеть столь дорогого гостя, и недождавшись его ответа, как бы завладев им, окружили его и повели в гостиную. В дверях гостиной не было возможности пройти от столпившихся членов и гостей, давивших друг друга и через плечи друг друга старавшихся, как редкого зверя, рассмотреть Багратиона. Граф Илья Андреич, энергичнее всех, смеясь и приговаривая: – пусти, mon cher, пусти, пусти, – протолкал толпу, провел гостей в гостиную и посадил на средний диван. Тузы, почетнейшие члены клуба, обступили вновь прибывших. Граф Илья Андреич, проталкиваясь опять через толпу, вышел из гостиной и с другим старшиной через минуту явился, неся большое серебряное блюдо, которое он поднес князю Багратиону. На блюде лежали сочиненные и напечатанные в честь героя стихи. Багратион, увидав блюдо, испуганно оглянулся, как бы отыскивая помощи. Но во всех глазах было требование того, чтобы он покорился. Чувствуя себя в их власти, Багратион решительно, обеими руками, взял блюдо и сердито, укоризненно посмотрел на графа, подносившего его. Кто то услужливо вынул из рук Багратиона блюдо (а то бы он, казалось, намерен был держать его так до вечера и так итти к столу) и обратил его внимание на стихи. «Ну и прочту», как будто сказал Багратион и устремив усталые глаза на бумагу, стал читать с сосредоточенным и серьезным видом. Сам сочинитель взял стихи и стал читать. Князь Багратион склонил голову и слушал.
«Славь Александра век
И охраняй нам Тита на престоле,
Будь купно страшный вождь и добрый человек,
Рифей в отечестве а Цесарь в бранном поле.
Да счастливый Наполеон,
Познав чрез опыты, каков Багратион,
Не смеет утруждать Алкидов русских боле…»
Но еще он не кончил стихов, как громогласный дворецкий провозгласил: «Кушанье готово!» Дверь отворилась, загремел из столовой польский: «Гром победы раздавайся, веселися храбрый росс», и граф Илья Андреич, сердито посмотрев на автора, продолжавшего читать стихи, раскланялся перед Багратионом. Все встали, чувствуя, что обед был важнее стихов, и опять Багратион впереди всех пошел к столу. На первом месте, между двух Александров – Беклешова и Нарышкина, что тоже имело значение по отношению к имени государя, посадили Багратиона: 300 человек разместились в столовой по чинам и важности, кто поважнее, поближе к чествуемому гостю: так же естественно, как вода разливается туда глубже, где местность ниже.
Перед самым обедом граф Илья Андреич представил князю своего сына. Багратион, узнав его, сказал несколько нескладных, неловких слов, как и все слова, которые он говорил в этот день. Граф Илья Андреич радостно и гордо оглядывал всех в то время, как Багратион говорил с его сыном.
Николай Ростов с Денисовым и новым знакомцем Долоховым сели вместе почти на середине стола. Напротив них сел Пьер рядом с князем Несвицким. Граф Илья Андреич сидел напротив Багратиона с другими старшинами и угащивал князя, олицетворяя в себе московское радушие.
Труды его не пропали даром. Обеды его, постный и скоромный, были великолепны, но совершенно спокоен он всё таки не мог быть до конца обеда. Он подмигивал буфетчику, шопотом приказывал лакеям, и не без волнения ожидал каждого, знакомого ему блюда. Всё было прекрасно. На втором блюде, вместе с исполинской стерлядью (увидав которую, Илья Андреич покраснел от радости и застенчивости), уже лакеи стали хлопать пробками и наливать шампанское. После рыбы, которая произвела некоторое впечатление, граф Илья Андреич переглянулся с другими старшинами. – «Много тостов будет, пора начинать!» – шепнул он и взяв бокал в руки – встал. Все замолкли и ожидали, что он скажет.
– Здоровье государя императора! – крикнул он, и в ту же минуту добрые глаза его увлажились слезами радости и восторга. В ту же минуту заиграли: «Гром победы раздавайся».Все встали с своих мест и закричали ура! и Багратион закричал ура! тем же голосом, каким он кричал на Шенграбенском поле. Восторженный голос молодого Ростова был слышен из за всех 300 голосов. Он чуть не плакал. – Здоровье государя императора, – кричал он, – ура! – Выпив залпом свой бокал, он бросил его на пол. Многие последовали его примеру. И долго продолжались громкие крики. Когда замолкли голоса, лакеи подобрали разбитую посуду, и все стали усаживаться, и улыбаясь своему крику переговариваться. Граф Илья Андреич поднялся опять, взглянул на записочку, лежавшую подле его тарелки и провозгласил тост за здоровье героя нашей последней кампании, князя Петра Ивановича Багратиона и опять голубые глаза графа увлажились слезами. Ура! опять закричали голоса 300 гостей, и вместо музыки послышались певчие, певшие кантату сочинения Павла Ивановича Кутузова.
«Тщетны россам все препоны,
Храбрость есть побед залог,
Есть у нас Багратионы,
Будут все враги у ног» и т.д.
Только что кончили певчие, как последовали новые и новые тосты, при которых всё больше и больше расчувствовался граф Илья Андреич, и еще больше билось посуды, и еще больше кричалось. Пили за здоровье Беклешова, Нарышкина, Уварова, Долгорукова, Апраксина, Валуева, за здоровье старшин, за здоровье распорядителя, за здоровье всех членов клуба, за здоровье всех гостей клуба и наконец отдельно за здоровье учредителя обеда графа Ильи Андреича. При этом тосте граф вынул платок и, закрыв им лицо, совершенно расплакался.


Пьер сидел против Долохова и Николая Ростова. Он много и жадно ел и много пил, как и всегда. Но те, которые его знали коротко, видели, что в нем произошла в нынешний день какая то большая перемена. Он молчал всё время обеда и, щурясь и морщась, глядел кругом себя или остановив глаза, с видом совершенной рассеянности, потирал пальцем переносицу. Лицо его было уныло и мрачно. Он, казалось, не видел и не слышал ничего, происходящего вокруг него, и думал о чем то одном, тяжелом и неразрешенном.
Этот неразрешенный, мучивший его вопрос, были намеки княжны в Москве на близость Долохова к его жене и в нынешнее утро полученное им анонимное письмо, в котором было сказано с той подлой шутливостью, которая свойственна всем анонимным письмам, что он плохо видит сквозь свои очки, и что связь его жены с Долоховым есть тайна только для одного него. Пьер решительно не поверил ни намекам княжны, ни письму, но ему страшно было теперь смотреть на Долохова, сидевшего перед ним. Всякий раз, как нечаянно взгляд его встречался с прекрасными, наглыми глазами Долохова, Пьер чувствовал, как что то ужасное, безобразное поднималось в его душе, и он скорее отворачивался. Невольно вспоминая всё прошедшее своей жены и ее отношения с Долоховым, Пьер видел ясно, что то, что сказано было в письме, могло быть правда, могло по крайней мере казаться правдой, ежели бы это касалось не его жены. Пьер вспоминал невольно, как Долохов, которому было возвращено всё после кампании, вернулся в Петербург и приехал к нему. Пользуясь своими кутежными отношениями дружбы с Пьером, Долохов прямо приехал к нему в дом, и Пьер поместил его и дал ему взаймы денег. Пьер вспоминал, как Элен улыбаясь выражала свое неудовольствие за то, что Долохов живет в их доме, и как Долохов цинически хвалил ему красоту его жены, и как он с того времени до приезда в Москву ни на минуту не разлучался с ними.