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

В области математической логики и информатики , известной как теория типов , вид — это тип конструктора типа или, реже, тип оператора типа более высокого порядка . Система видов, по сути, представляет собой просто типизированное лямбда-исчисление «на уровень выше», наделенное примитивным типом, обозначаемым $*$ и называется «типом», который представляет собой тип любого типа данных , который не требует каких-либо параметров типа .

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

Поскольку операторы типов высшего порядка редко встречаются в языках программирования , в большей части практики программирования виды используются для различения типов данных и типов конструкторов, которые используются для реализации параметрического полиморфизма . Виды появляются явно или неявно в языках, системы типов которых учитывают параметрический полиморфизм программно доступным способом, например C++ . Хаскель и Скала .

Примеры

• $*$, произносится как «тип», является разновидностью всех типов данных , которые рассматриваются как конструкторы нулевых типов и в этом контексте также называются правильными типами. Обычно сюда входят типы функций в функциональных языках программирования .
• $*\rightarrow *$ является разновидностью конструктора унарного типа , например конструктора спискового типа .
• $*\rightarrow *\rightarrow *$ это своего рода конструктор двоичного типа (через каррирование ), например, конструктор парного типа , а также конструктор типа функции (не путать с результатом его применения, который сам по себе является типом функции, то есть типа $*$)
• $(*\rightarrow *)\rightarrow *$ — это своего рода оператор типа более высокого порядка, преобразующий конструкторы унарных типов в правильные типы.

Виды в Haskell

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

Видовая система Haskell 98 включает ровно два вида:

• $*$, произносится как «тип» — это тип всех типов данных .
• $k_{1}\rightarrow k_{2}$ это своего рода конструктор унарного типа , который принимает тип вида $k_{1}$ и производит тип вида $k_{2}$.

Обитаемый тип (так в Haskell называются правильные типы) — это тип, который имеет значения. Например, игнорируя классы типов , которые усложняют картину, 4 это значение типа Int, пока [1, 2, 3] это значение типа [Int](список Ints). Поэтому, Int и [Int] иметь добрый $*$, но то же самое относится и к любому типу функции, например Int -> Bool или даже Int -> Int -> Bool.

Конструктор типа принимает один или несколько аргументов типа и создает тип данных, когда предоставлено достаточное количество аргументов, т. е. он поддерживает частичное применение благодаря каррированию. Вот как Haskell создает параметрические типы. Например, тип [](список) — это конструктор типа: для указания типа элементов списка требуется один аргумент. Следовательно, [Int] (список Ints), [Float] (список поплавков) и даже [[Int]] (список списков целых чисел) являются допустимыми приложениями []конструктор типов. Поэтому, [] это тип рода $*\rightarrow *$. Потому что Int имеет вид $*$, применяя [] к этому приводит [Int], типа $*$. 2- кортежный конструктор (,) имеет вид $*\rightarrow *\rightarrow *$, трехкортежный конструктор (,,) имеет вид $*\rightarrow *\rightarrow *\rightarrow *$ и так далее.

Добрый вывод

Стандартный Haskell не допускает полиморфных типов . В этом отличие от параметрического полиморфизма типов, который поддерживается в Haskell. Например, в следующем примере:

 данных  Дерево   z    =   Лист   |    Развилка   (  Дерево   z  )   (  Дерево   z  ) 

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

введите   FunnyTree   =   Tree   []       -- неверно 

потому что вид [], $*\rightarrow *$ не соответствует ожидаемому виду для z, что всегда $*$.

Однако разрешены операторы типов более высокого порядка. Например:

 данных  Приложение   unt   z   =   Z   (  unt   z  ) 

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

GHC имеет расширение PolyKinds, который вместе с KindSignatures, допускает полиморфные виды. Например:

 данных  Дерево   (  z   ::   k  )   =   Лист   |    Развилка   (  Дерево   z  )   (  Дерево   z  ) 
 тип   FunnyTree   =   Дерево   []       -- ОК 

Начиная с GHC 8.0.1, типы и виды объединены.

См. также

• Система Ф-омега
• Система чистого типа

Ссылки

• Пирс, Бенджамин (2002). Типы и языки программирования . МТИ Пресс. ISBN  0-262-16209-1 . , глава 29, «Операторы типов и сортировка»