Мотивация для ограничения продвижения типа данных

Может ли кто-нибудь объяснить или предположить мотивы ограничения на продвижение типов данных, обсуждаемого в разделе 7.9.2. руководства пользователя GHC?

На продвижение действуют следующие ограничения:

  • Мы продвигаем только те типы данных, виды которых имеют вид * -> ... -> * -> *. В частности, мы не продвигаем типы данных более высокого типа, такие как data Fix f = In (f (Fix f)), или типы данных, виды которых включают расширенные типы, такие как Vec :: * -> Nat -> *.

В частности, меня интересует последняя часть о продвигаемых типах, таких как Vec :: * -> Nat -> *. Продвижение некоторых типов вроде этого кажется естественным. Я столкнулся с этим довольно быстро, когда пытался преобразовать одну из моих библиотек для использования определенных продвинутых типов для различных типов фантомов вместо использования типа * для всего, чтобы предоставить лучшую документацию и тому подобное.

Часто причины подобных ограничений компилятора бросаются в глаза, если немного подумать, но я не вижу этой причины. Поэтому мне интересно, входит ли это в категорию «еще не нужно, поэтому мы его не строили» или «это невозможно/неразрешимо/разрушает вывод».


haskell ghc data-kinds
person Doug McClean    schedule 18.01.2014    source источник

Ответы (2)


arrow_upward
20
arrow_downward

Интересная вещь происходит, если вы продвигаете типы, индексированные продвигаемыми типами. Представьте, мы строим

data Nat = Ze | Su Nat

а потом

data Vec :: Nat -> * -> * where
  VNil   :: Vec Ze x
  VCons  :: x -> Vec n x -> Vec (Su n) x

За кулисами внутренние типы конструкторов представляют инстанцированные возвращаемые индексы ограничениями, как если бы мы написали

data Vec (n :: Nat) (a :: *)
  =            n ~ Ze    => VNil
  | forall k.  n ~ Su k  => VCons a (Vec k a)

Теперь, если бы нам разрешили что-то вроде

data Elem :: forall n a. a -> Vec n a -> * where
  Top :: Elem x (VCons x xs)
  Pop :: Elem x xs -> Elem x (VCons y xs)

перевод во внутреннюю форму должен быть чем-то вроде

data Elem (x :: a) (zs :: Vec n a)
  = forall (k :: Nat), (xs :: Vec k a).            (n ~ Su k, zs ~ VCons x xs) =>
      Top
  | forall (k :: Nat), (xs :: Vec k s), (y :: a).  (n ~ Su k, zs ~ VCons y xs) =>
      Pop (Elem x xs)

но посмотрите на второе ограничение в каждом случае! У нас есть

zs :: Vec n a

но

VCons x xs, VCons y xs :: Vec (Su k) a

Но в System FC, как тогда было определено, ограничения равенства должны иметь типы одного и того же вида с обеих сторон, так что этот пример не так уж проблематичен.

Одно исправление заключается в использовании свидетельства первого ограничения для исправления второго, но тогда нам понадобятся зависимые ограничения.

(q1 :: n ~ Su k, zs |> q1 ~ VCons x xs)

Другое решение — просто разрешить гетерогенные уравнения, как я сделал пятнадцать лет назад в теории зависимых типов. Неизбежно возникнут уравнения между вещами, виды которых равны в синтаксически неочевидном смысле.

В настоящее время предпочтение отдается последнему плану. Насколько я понимаю, политика, которую вы упомянули, была принята в качестве удерживающей позиции до тех пор, пока разработка основного языка с гетерогенным равенством (как это было предложено Вейрихом и его коллегами) не созрела для реализации. Мы живем в интересные времена.

person pigworker    schedule 18.01.2014
comment
+1 за гораздо лучший ответ, чем мой. Влияет ли гетерогенное равенство только на GADT? - person Daniel Gratzer; 18.01.2014
comment
Ваше здоровье! GADT — это основное место, где вводятся ограничения равенства, но иногда они также появляются в объявлениях экземпляров. Есть такой трюк, когда вы делаете что-то вроде instance (x ~ p, C t) => C (x -> t), чтобы добиться более агрессивных обязательств, чем instance C t => C (p -> t). Бьюсь об заклад, гетерогенное равенство проявится и в подобных вещах. - person pigworker; 18.01.2014

arrow_upward
4
arrow_downward

Вероятно, это связано с тем, что в GHC нет особенно богатого понятия «сорты», сорта — это тип видов, поэтому

  values : type : kind : sort : ...

Обратите внимание, что хотя у нас есть довольно сложная система видов с типами данных, все виды по-прежнему превращаются в очень простые сортировки. Для продвижения таких видов, как Nat, потребуется более одного типа/конструктора сортировки, а для продвижения Fix потребуются виды с более высокой сортировкой, которые также не охватываются примитивной системой сортировки.

Это не технический барьер, такие языки, как Coq или Agda (языки с зависимой типизацией), имеют целый бесконечный стек из них, но GHC только недавно создал добрую систему. Просто еще не реализована какая-либо сложная система сортировки, возможно, в будущем мы ее получим.

person Daniel Gratzer    schedule 18.01.2014