Тип (теория типов)

редактировать

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

Тип иногда ошибочно описывается как "тип типа (данных) ", но на самом деле это скорее спецификатор arity. Синтаксически естественно рассматривать полиморфные типы как конструкторы типов, поэтому неполиморфные типы должны быть конструкторами типов nullary. Но все конструкторы с нулевым значением, а значит, и все мономорфные типы, имеют один и тот же самый простой вид; а именно $∗ {\ displaystyle *}$ $*$ .

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

Contents

1 Примеры
2 Типа в Haskell
- 2.1 Вывод типа
3 См. Также
4 Ссылки

Примеры

$∗ {\ displaystyle *}$ $*$ , произносится " type "- это вид всех типов данных, рассматриваемых как конструкторы типов nullary и также называемых в этом контексте собственными типами. Обычно сюда входят типы функций в языках функционального программирования.
$∗ → ∗ {\ displaystyle * \ rightarrow *}$ $* \ rightarrow *$ - это разновидность конструктора унарного типа, например конструктора типа списка.
$∗ → ∗ → ∗ {\ displaystyle * \ rightarrow * \ rightarrow *}$ $* \ rightarrow * \ rightarrow *$ является разновидностью двоичного типа конструктор (через каррирование ), например конструктора парного типа , а также конструктора типа функции (не путать с результатом его применения, который сам является типом функции, таким образом, вида $∗ {\ displaystyle *}$ $*$ )
$(∗ → ∗) → ∗ {\ displaystyle (* \ rightarrow *) \ rightarrow *}$ $(* \ rightarrow *) \ rightarrow *$ - это разновидность оператора типа высшего порядка из конструкторов унарного типа. к правильным типам.

Виды в Haskell

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

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

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

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

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

`Вид вывода`

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

дерево данных z = Leaf | Вилка (Дерево z) (Дерево z)

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

FunnyTree = Tree - invalid

, потому что это вид , $∗ → ∗ {\ displaystyle * \ rightarrow *}$ $* \ rightarrow *$ не соответствует ожидаемому типу для z, которым всегда является $∗ {\ displaystyle *}$ $*$ .


Однако разрешены операторы типа более высокого порядка. Например:
приложение данных Unt z = Z (unt z)
имеет вид  $(∗ → ∗) → ∗ → ∗ {\ displaystyle (* \ rightarrow *) \ rightarrow * \ rightarrow *}$  $(* \ rightarrow *) \ rightarrow * \ rightarrow *$ , т.е. unt, как ожидается, будет унарным конструктором данных, который применяется к своему аргументу, который должен быть типом, и возвращает другой тип.
GHC имеет расширение PolyKinds, которое вместе с KindSignaturesдопускает полиморфные виды. Например:
дерево данных (z :: k) = Leaf | Fork (Tree z) (Tree z) type FunnyTree = Tree - OK
Начиная с GHC 8.0.1, типы и виды объединены.
См. Также
System F-omega 
Pure система типов 
Ссылки