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

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

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

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

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

Примеры

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

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

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

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

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

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

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

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

data App unt z = Z (unt z)

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

См. также

• <span class="nowrap">Система Fω</span>^[en]
• Чистая система типов

Примечания

Литература

• Лука Карделли^[en]. Typeful programming ( (англ.)) // IFIP State-of-the-Art Reports. — New York: Springer-Verlag, 1991. — Вып. Formal Description of Programming Concepts. — С. 431–507.
• Лука Карделли^[en], Peter Wegner. On Understanding Types, Data Abstraction, and Polymorphism. — ACM Computing Surveys, 1985. — С. 471-523. — ISSN 0360-0300.
• Pierce, Benjamin C. Types and Programming Languages. — MIT Press, 2002. — ISBN 0-262-16209-1.
  • Перевод на русский язык: Пирс Б. Типы в языках программирования. — Добросвет, 2012. — 680 с. — ISBN 978-5-7913-0082-9.

Эта страница в последний раз была отредактирована 27 июня 2022 в 18:11.