Интуиционистская теория типов
- 1 year ago
- 0
- 0
Род
в
теории типов
(
англ.
kind
) — тип
конструктора типов
, или более формально, тип
ти́пового оператора высшего порядка
. Система родо́в естественным образом представляется как родительское (вышестоящее)
просто типизированное лямбда-исчисление
, снабжённое примитивным типом, обозначаемым «
*
» (читается «
тип
»), формирующим род
мономорфных
типов данных
.
Более наглядно, род представляет собой
тип типов
, или
метатип
— аналогично тому как множество значений формирует
тип
, — множество типов формирует род
. При этом вхождение типов в более общие типы (в качестве подтипов) отличается от принадлежности типов роду — деление разнообразных типов на рода происходит на более абстрактном уровне. Например, типы «
натуральное
», «
целое
» и «
вещественное
» являются подтипами более общего типа «
число
»; все четыре типа представляют непосредственные значения, и поэтому принадлежат к роду «
*
». Другие рода формируются из разнообразных
операций над типами
— подобно тому как в арифметике различают
числа
и
операции над числами
.
Синтаксически естественно было бы считать все полиморфные типы
конструкторами типов
; и, соответственно, все мономорфные —
нульарными
конструкторами типов. Однако, все нульарные конструкторы, то есть все мономорфные типы, в действительности принадлежат к единому роду, а именно к «
*
».
Из-за того, что ти́повые операторы высших порядков нетипичны для большинства языков программирования , в практике программирования рода́ используются для того, чтобы отличать типы данных от типов конструкторов , используемых для реализации параметрического полиморфизма . Рода́ явным или неявным образом появляются в языках с полными системами типов , таких как Haskell и Scala .
list
.
*
»).
Haskell предоставляет полиморфные типы, но не разрешает полиморфные рода́ . Например, в этом определении полиморфного алгебраического типа
data Tree z = Leaf | Fork (Tree z) (Tree z)
z
может принадлежать к любому роду, включая «
», «
» и др. По умолчанию Хаскел всегда выводит род «
», если не явно не указан иной (см.ниже). Поэтому
система проверки согласования типов
отвергнет следующую попытку использовать тип
Tree
:
type FunnyTree = Tree [] -- ошибка
потому что тип
[]
принадлежит к роду «
», а это не соответствует ожидаемому роду для
z
, который всегда «
».
Однако, ти́повые операторы высших порядков разрешены. Например,
data App unt z = Z (unt z)
принадлежит к роду «
», то есть
unt
должен быть унарным
конструктором
, но здесь он в качестве аргумента получает тип и возвращает другой тип.