Теория типов: типы типов

Я прочитал много интересного о типах, типах более высокого типа и т.д. По умолчанию Haskell поддерживает два типа типов:

Простой тип: *
Конструктор типов: * → *

Последние расширения языка GHC ConstraintKinds добавляет новый вид:

Ограничение параметра типа: Constraint

Также после чтения этого списка рассылки становится ясно, что другой тип типа может существовать, но не поддерживается GHC (но такая поддержка реализован в .NET):

Unboxed type: #

Я узнал о полиморфных видах, и я думаю, что понимаю эту идею. Также Haskell поддерживает явно выраженную количественную оценку.

Итак, мои вопросы:

Существуют ли другие типы видов?
Существуют ли другие функции языка с выраженным выражением?
Что означает subkinding? Где он реализован/полезен?
Существует ли система типов поверх kinds, например kinds - это система типов сверху types? (просто интересно)

Ответ 1

Да, существуют другие виды. Страница Промежуточные типы описывает другие типы, используемые в GHC (включая как незапакованные типы, так и некоторые более сложные виды). Язык Ωmega использует более высокосортные типы для максимального логического расширения, что позволяет определять определяемые пользователем типы (и сортировки и выше). Эта страница предлагает вид системного расширения для GHC, который позволит определять пользовательские типы в Haskell, а также хороший пример того, почему они были бы полезны.

Как короткий отрывок, предположим, что вам нужен тип списка, который имел аннотацию на уровне уровня длины списка, например:

data Zero
data Succ n

data List :: * -> * -> * where
  Nil   :: List a Zero
  Cons  :: a -> List a n -> List a (Succ n)

Предполагается, что аргумент последнего типа должен быть только Zero или Succ n, где n снова является только Zero или Succ n. Короче говоря, вам нужно ввести новый вид, называемый Nat, который содержит только два типа Zero и Succ n. Тогда тип данных List мог бы выразить, что последний аргумент не является *, но a Nat, например

data List :: * -> Nat -> * where
  Nil   :: List a Zero
  Cons  :: a -> List a n -> List a (Succ n)

Это позволит проверять тип гораздо более дискриминационным в том, что он принимает, а также сделать более понятным программирование на уровне.

Ответ 2

Подобно тому, как типы классифицируются по видам, виды классифицируются по видам.

Язык программирования Ωmega имеет свою систему с определенными пользователями на любом уровне. (Так говорит его вики. Я думаю, что это относится к типам и уровням выше, но я не уверен.)

Ответ 3

Было предложено поднять типы на уровень вида и значения на уровень типа. Но я не знаю, если это уже реализовано (или если оно когда-либо достигнет "прайм-тайм" )

Рассмотрим следующий код:

data Z
data S a 

data Vec (a :: *) (b :: *) where
  VNil  :: Vec Z a 
  VCons :: a -> Vec l a -> Vec (S l) a

Это вектор, который имеет размерность, закодированную в типе. Мы используем Z и S для генерации натурального числа. Такой хороший, но мы не можем "набирать чек", если мы используем правильные типы при создании Vec (мы могли бы случайно изменить длину типа содержимого), и нам также необходимо создать тип S и Z, что неудобно, если мы уже определяли натуральные числа следующим образом:

data Nat = Z | S Nat

С предложением вы можете написать примерно следующее:

data Nat = Z | S Nat

data Vec (a :: Nat) (b :: *) where                                              
  VNil  :: Vec Z a
  VCons :: a -> Vec l a -> Vec (S l) a

Это поднимет Nat на уровне уровня, а S и Z - на уровень типа, если это необходимо. Так что Nat - другой вид и живет на том же уровне, что и *.

Вот презентация Брент Йорги

Типичное функциональное программирование на уровне уровня в GHC