Род (теория типов)

Род в теории типов (англ. kind) — тип конструктора типов, или более формально, тип ти́пового оператора высшего порядка. Система родо́в естественным образом представляется как родительское (вышестоящее) просто типизированное лямбда-исчисление, снабжённое примитивным типом, обозначаемым «*» (читается «тип»), формирующим род мономорфных типов данных.

Более наглядно, род представляет собой тип типов, или метатип — аналогично тому как множество значений формирует тип, — множество типов формирует род. При этом вхождение типов в более общие типы (в качестве подтипов) отличается от принадлежности типов роду — деление разнообразных типов на рода происходит на более абстрактном уровне. Например, типы «натуральное», «целое» и «вещественное» являются подтипами более общего типа «число»; все четыре типа представляют непосредственные значения, и поэтому принадлежат к роду «*». Другие рода формируются из разнообразных операций над типами — подобно тому как в арифметике различают числа и операции над числами.

Синтаксически естественно было бы считать все полиморфные типы конструкторами типов; и, соответственно, все мономорфные — нульарными конструкторами типов. Однако, все нульарные конструкторы, то есть все мономорфные типы, в действительности принадлежат к единому роду, а именно к «*».

Из-за того, что ти́повые операторы высших порядков нетипичны для большинства языков программирования, в практике программирования рода́ используются для того, чтобы отличать типы данных от типов конструкторов, используемых для реализации параметрического полиморфизма. Рода́ явным или неявным образом появляются в языках с полными системами типов, таких как Haskell и Scala.

Примеры

• <math>*</math> (читается «тип») — род всех мономорфных типов, рассматриваемых как нульарные конструкторы типов, называемых также верными типами (англ. proper types). К этому роду также принадлежат функциональные типы в функциональных языках.
• <math>* \rightarrow *</math> — род всех унарных конструкторов типов. Например, конструктор типа список — list.
• <math>* \rightarrow * \rightarrow *</math> — род бинарных каррированных конструкторов типов. Например, конструктор типа-пары, или конструктор функционального типа (не следует путать с результатом применения этого конструктора, то есть с самим функциональным типом, который принадлежит к роду «*»).
• <math>(* \rightarrow *) \rightarrow *</math> — род ти́повых операторов высшего порядка, то есть операторов, которые получают унарные конструкторы типов на входе и порождают верные типы на выходе.

Выведение родо́в в Haskell

Haskell предоставляет полиморфные типы, но не разрешает полиморфные рода́. Например, в этом определении полиморфного алгебраического типа

data Tree z  = Leaf | Fork (Tree z) (Tree z)

z может принадлежать к любому роду, включая «<math>*</math>», «<math>* \rightarrow *</math>» и др. По умолчанию Хаскел всегда выводит род «<math>*</math>», если не явно не указан иной (см.ниже). Поэтому система проверки согласования типов отвергнет следующую попытку использовать тип Tree:

type FunnyTree = Tree []     -- ошибка

потому что тип [] принадлежит к роду «<math>* \rightarrow *</math>», а это не соответствует ожидаемому роду для z, который всегда «<math>*</math>».

Однако, ти́повые операторы высших порядков разрешены. Например,

data App unt z = Z (unt z)

принадлежит к роду «<math>(* \rightarrow *) \rightarrow * \rightarrow *</math>», то есть unt должен быть унарным конструктором, но здесь он в качестве аргумента получает тип и возвращает другой тип.

См. также

• Система Fω
• Чистая система типов

Литература

• Лука Карделли [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.
• Лука Карделли, Peter Wegner [lucacardelli.name/Papers/OnUnderstanding.A4.pdf On Understanding Types, Data Abstraction, and Polymorphism]. — ACM Computing Surveys, 1985. — С. 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].
• Pierce, Benjamin C. [www.cis.upenn.edu/~bcpierce/tapl/ Types and Programming Languages]. — MIT Press, 2002. — ISBN 0-262-16209-1.
  • Перевод на русский язык: Пирс Б. Типы в языках программирования. — Добросвет, 2012. — 680 с. — ISBN 978-5-7913-0082-9.

Отрывок, характеризующий Род (теория типов)

Князь Андрей приехал в главную квартиру армии в конце июня. Войска первой армии, той, при которой находился государь, были расположены в укрепленном лагере у Дриссы; войска второй армии отступали, стремясь соединиться с первой армией, от которой – как говорили – они были отрезаны большими силами французов. Все были недовольны общим ходом военных дел в русской армии; но об опасности нашествия в русские губернии никто и не думал, никто и не предполагал, чтобы война могла быть перенесена далее западных польских губерний.
Князь Андрей нашел Барклая де Толли, к которому он был назначен, на берегу Дриссы. Так как не было ни одного большого села или местечка в окрестностях лагеря, то все огромное количество генералов и придворных, бывших при армии, располагалось в окружности десяти верст по лучшим домам деревень, по сю и по ту сторону реки. Барклай де Толли стоял в четырех верстах от государя. Он сухо и холодно принял Болконского и сказал своим немецким выговором, что он доложит о нем государю для определения ему назначения, а покамест просит его состоять при его штабе. Анатоля Курагина, которого князь Андрей надеялся найти в армии, не было здесь: он был в Петербурге, и это известие было приятно Болконскому. Интерес центра производящейся огромной войны занял князя Андрея, и он рад был на некоторое время освободиться от раздражения, которое производила в нем мысль о Курагине. В продолжение первых четырех дней, во время которых он не был никуда требуем, князь Андрей объездил весь укрепленный лагерь и с помощью своих знаний и разговоров с сведущими людьми старался составить себе о нем определенное понятие. Но вопрос о том, выгоден или невыгоден этот лагерь, остался нерешенным для князя Андрея. Он уже успел вывести из своего военного опыта то убеждение, что в военном деле ничего не значат самые глубокомысленно обдуманные планы (как он видел это в Аустерлицком походе), что все зависит от того, как отвечают на неожиданные и не могущие быть предвиденными действия неприятеля, что все зависит от того, как и кем ведется все дело. Для того чтобы уяснить себе этот последний вопрос, князь Андрей, пользуясь своим положением и знакомствами, старался вникнуть в характер управления армией, лиц и партий, участвовавших в оном, и вывел для себя следующее понятие о положении дел.
Когда еще государь был в Вильне, армия была разделена натрое: 1 я армия находилась под начальством Барклая де Толли, 2 я под начальством Багратиона, 3 я под начальством Тормасова. Государь находился при первой армии, но не в качестве главнокомандующего. В приказе не было сказано, что государь будет командовать, сказано только, что государь будет при армии. Кроме того, при государе лично не было штаба главнокомандующего, а был штаб императорской главной квартиры. При нем был начальник императорского штаба генерал квартирмейстер князь Волконский, генералы, флигель адъютанты, дипломатические чиновники и большое количество иностранцев, но не было штаба армии. Кроме того, без должности при государе находились: Аракчеев – бывший военный министр, граф Бенигсен – по чину старший из генералов, великий князь цесаревич Константин Павлович, граф Румянцев – канцлер, Штейн – бывший прусский министр, Армфельд – шведский генерал, Пфуль – главный составитель плана кампании, генерал адъютант Паулучи – сардинский выходец, Вольцоген и многие другие. Хотя эти лица и находились без военных должностей при армии, но по своему положению имели влияние, и часто корпусный начальник и даже главнокомандующий не знал, в качестве чего спрашивает или советует то или другое Бенигсен, или великий князь, или Аракчеев, или князь Волконский, и не знал, от его ли лица или от государя истекает такое то приказание в форме совета и нужно или не нужно исполнять его. Но это была внешняя обстановка, существенный же смысл присутствия государя и всех этих лиц, с придворной точки (а в присутствии государя все делаются придворными), всем был ясен. Он был следующий: государь не принимал на себя звания главнокомандующего, но распоряжался всеми армиями; люди, окружавшие его, были его помощники. Аракчеев был верный исполнитель блюститель порядка и телохранитель государя; Бенигсен был помещик Виленской губернии, который как будто делал les honneurs [был занят делом приема государя] края, а в сущности был хороший генерал, полезный для совета и для того, чтобы иметь его всегда наготове на смену Барклая. Великий князь был тут потому, что это было ему угодно. Бывший министр Штейн был тут потому, что он был полезен для совета, и потому, что император Александр высоко ценил его личные качества. Армфельд был злой ненавистник Наполеона и генерал, уверенный в себе, что имело всегда влияние на Александра. Паулучи был тут потому, что он был смел и решителен в речах, Генерал адъютанты были тут потому, что они везде были, где государь, и, наконец, – главное – Пфуль был тут потому, что он, составив план войны против Наполеона и заставив Александра поверить в целесообразность этого плана, руководил всем делом войны. При Пфуле был Вольцоген, передававший мысли Пфуля в более доступной форме, чем сам Пфуль, резкий, самоуверенный до презрения ко всему, кабинетный теоретик.
Кроме этих поименованных лиц, русских и иностранных (в особенности иностранцев, которые с смелостью, свойственной людям в деятельности среди чужой среды, каждый день предлагали новые неожиданные мысли), было еще много лиц второстепенных, находившихся при армии потому, что тут были их принципалы.