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

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

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

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

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

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

Ответ 1

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

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)

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

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

Ответ 2

Это, вероятно, связано с тем, что GHC не имеет особого богатого понятия "сорта", сорта - это тип видов, поэтому

  values : type : kind : sort : ...

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

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