Русская Википедия:Род (теория типов)
Род в теории типов (Шаблон:Lang-en[1]) — тип конструктора типов, или более формально, тип ти́пового оператора высшего порядка. Система родо́в естественным образом представляется как родительское (вышестоящее) просто типизированное лямбда-исчисление, снабжённое примитивным типом, обозначаемым «*» (читается «тип»), формирующим род мономорфных типов данных.
Более наглядно, род представляет собой тип типов, или метатип — аналогично тому как множество значений формирует тип, — множество типов формирует родШаблон:Sfn. При этом вхождение типов в более общие типы (в качестве подтипов) отличается от принадлежности типов роду — деление разнообразных типов на рода происходит на более абстрактном уровне. Например, типы «натуральное», «целое» и «вещественное» являются подтипами более общего типа «число»; все четыре типа представляют непосредственные значения, и поэтому принадлежат к роду «*». Другие рода формируются из разнообразных операций над типами — подобно тому как в арифметике различают числа и операции над числами.
Синтаксически естественно было бы считать все полиморфные типы конструкторами типов; и, соответственно, все мономорфные — нульарными конструкторами типов. Однако, все нульарные конструкторы, то есть все мономорфные типы, в действительности принадлежат к единому роду, а именно к «*».
Из-за того, что ти́повые операторы высших порядков нетипичны для большинства языков программирования, в практике программирования рода́ используются для того, чтобы отличать типы данных от типов конструкторов, используемых для реализации параметрического полиморфизма. Рода́ явным или неявным образом появляются в языках с полными системами типов, таких как Haskell и Scala[2].
Примеры
- <math>*</math> (читается «тип») — род всех мономорфных типов, рассматриваемых как нульарные конструкторы типов, называемых также собственно типами (Шаблон:Lang-en). К этому роду также принадлежат функциональные типы в функциональных языках.
- <math>* \rightarrow *</math> — род всех унарных конструкторов типов. Например, конструктор типа список —
list. - <math>* \rightarrow * \rightarrow *</math> — род бинарных каррированных конструкторов типов. Например, конструктор типа-пары, или конструктор функционального типа (не следует путать с результатом применения этого конструктора, то есть с самим функциональным типом, который принадлежит к роду «
*»). - <math>(* \rightarrow *) \rightarrow *</math> — род ти́повых операторов высшего порядка, то есть операторов, которые получают унарные конструкторы типов на входе и порождают собственно типы на выходеШаблон:Sfn.
Выведение родов в Haskell
Haskell предоставляет полиморфные типы, но не разрешает полиморфные рода́[3]. Например, в этом определении полиморфного алгебраического типа
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 должен быть унарным конструктором, но здесь он в качестве аргумента получает тип и возвращает другой тип.
См. также
Примечания
Литература
- Шаблон:Статья
- Шаблон:Статья
- Шаблон:Книга
- Перевод на русский язык: Шаблон:Книга
- ↑ В русскоязычной литературе нет устоявшегося перевода термина «kind». Встречаются такие варианты перевода как «вид», «сорт», «типаж»
- ↑ Шаблон:Cite web
- ↑ Документация по языку Haskell использует одну и ту же стрелку и для функциональных типов, и для родов
