Lt304888.ru

Туристические услуги

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

07-06-2023

Перейти к: навигация, поиск

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

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

Примечание: В русскоязычной литературе нет устоявшегося перевода термина «kind». Встречаются такие варианты перевода как «вид», «сорт», «типаж».

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

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

Примеры

Рода́ в языке Haskell

(Примечание: Документация по языку Haskell использует одну и ту же стрелку и для функциональных типов, и для родов.)

Система родо́в языка Haskell[4] состоит из следующих правил:


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

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. Pierce, 2002, Chapter 29, Type Operators and Kinding
  2. Generic of a Higher Kind
  3. Pierce, 2002, Chapter 32
  4. Kinds - The Haskell 98 Report

Литература

  • Typeful programming ( (англ.)) // IFIP State-of-the-Art Reports. — New York: Springer-Verlag, 1991. — В. Formal Description of Programming Concepts. — С. 431–507.
  • Benjamin Pierce Types and Programming Languages ( (англ.)). — MIT Press, 2002. — ISBN 0-262-16209-1.

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

© 2020–2023 lt304888.ru, Россия, Волжский, ул. Больничная 49, +7 (8443) 85-29-01