Добрый (теория типов)

Эта статья может быть слишком технической, чтобы ее могло понять большинство читателей . Пожалуйста, помогите улучшить его, чтобы он был понятен неспециалистам , не удаляя технические детали. ( Июнь 2020 г. ) ( Узнайте, как и когда удалить этот шаблон сообщения )

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

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

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

Примеры [ править ]

• ${\ displaystyle *}$, произносится как «тип» - это вид всех типов данных, рассматриваемых как конструкторы нулевого типа и также называемых в этом контексте собственными типами. Обычно сюда входят типы функций в языках функционального программирования .
• ${\ displaystyle * \ rightarrow *}$является разновидностью конструктора унарного типа , например конструктора типа списка .
• ${\ displaystyle * \ rightarrow * \ rightarrow *}$- это своего рода конструктор двоичного типа (через каррирование ), например конструктор парного типа , а также конструктор типа функции (не путать с результатом его применения, который сам является типом функции, таким образом, своего рода )${\ displaystyle *}$
• ${\ Displaystyle (* \ rightarrow *) \ rightarrow *}$является разновидностью оператора типа высшего порядка от конструкторов унарных типов до соответствующих типов. ^[3]

Виды в Haskell [ править ]

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

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

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

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

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

Доброе заключение [ править ]

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

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

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

тип  FunnyTree  =  Tree  []  - недопустимый

потому что тип [], не соответствует ожидаемому типу , который всегда .${\ displaystyle * \ rightarrow *}$z${\ displaystyle *}$

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

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

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

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

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

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

См. Также [ править ]

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

Ссылки [ править ]