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

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

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

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

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

Примеры

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

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

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

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

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

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

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

data App unt z = Z (unt z)

принадлежит к роду « », то есть unt должен быть унарным конструктором , но здесь он в качестве аргумента получает тип и возвращает другой тип.

См. также

Примечания

  1. В русскоязычной литературе нет устоявшегося перевода термина « kind ». Встречаются такие варианты перевода как « вид », « сорт », « типаж »
  2. , Глава 29. Операторы над типами и виды.
  3. . Дата обращения: 30 сентября 2017. 10 июня 2012 года.
  4. , Глава 32. Расширенный пример: чисто функциональные объекты.
  5. Документация по языку Haskell использует одну и ту же стрелку и для функциональных типов, и для родов

Литература

  • . ( (англ.) ) // IFIP State-of-the-Art Reports. — New York: Springer-Verlag, 1991. — Вып. Formal Description of Programming Concepts . — С. 431–507 .
  • , Peter Wegner. . — , 1985. — С. 471-523 . — ISSN .
  • Pierce, Benjamin C. . — MIT Press , 2002. — ISBN 0-262-16209-1 .
    • Перевод на русский язык: Пирс Б. Типы в языках программирования. — , 2012. — 680 с. — ISBN 978-5-7913-0082-9 .
Источник —

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