Теория типов: виды типов - PullRequest
Новая
       54

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

26 голосов
/ 13 октября 2011

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

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

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

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

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

  • Распакованный тип: #

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

Так что мои вопросы таковы:

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

Ответы [ 3 ]

14 голосов
/ 13 октября 2011

Да, существуют другие виды. Страница Промежуточные типы описывает другие виды, используемые в 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 может выражать, что последний аргумент не является *, а Nat, как 

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

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

10 голосов
/ 13 октября 2011

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

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

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 - на уровень типа, если это необходимо. Таким образом, Нат - другой тип и живет на том же уровне, что и *.

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

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

10 голосов
/ 13 октября 2011

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

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

...