数据类型提升受限的动机

Question

“请问有人能解释或猜测讨论GHC用户指南7.9.2中数据类型提升限制背后的动机吗？”

“以下限制适用于类型提升： - 我们只提升那些种类为<* ->...-> * ->*>的数据类型。特别地，我们不提升高阶种类的数据类型，例如data Fix f = In (f (Fix f))，或者其种类包含提升类型的数据类型，例如Vec :: * -> Nat -> *。 - 特别是，我对最后一部分关于诸如 Vec:: *->Nat->* 的提升类型很感兴趣。 提升这样的一些类型似乎很自然。我很快就遇到了这个问题，当我尝试将我的库转换为使用具体的晋升种类来进行各种幻象类型而不是在所有情况下使用kind <*>时，这将提供更好的文档等。”

往往像这样的编译器限制原因只需要稍加思考就能明白，但我并没有看到这个。所以我想知道它属于“目前还不需要，所以我们没有构建它”或者“那是不可能/不可决定的/破坏推断”的类别。

- Doug McClean

Answer 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)

另一个解决方法就是允许非同构方程，正如我在15年前的依赖类型理论中所做的那样。不可避免地会有一些东西之间的等式，在语法上并不明显相等。

目前更青睐后者的计划。据我所知，你提到的政策被采用作为临时措施，直到具有非同构相等性的核心语言设计（由Weirich和同事提出）成熟为实现。我们生活在一个有趣的时代。

- pigworker

---

如果有更好的答案，请点赞。异构相等只影响广义代数数据类型（GADTs）吗？ - daniel gratzer

干杯！GADTs是引入相等约束的主要场所，但有时它们也会出现在实例声明中。有一个技巧，你可以做类似于instance (x ~ p, C t) => C (x -> t)这样的事情，以比instance C t => C (p -> t)更强烈地承诺。我敢打赌，异构相等性也会在那种情况下出现。 - pigworker

Answer 2

这可能源于 GHC 没有特别丰富的“排序”概念，因为排序是种类的类型，所以。

  values : type : kind : sort : ...

请注意，尽管我们有一个与数据类别相关的相当复杂的类型系统，但所有类型仍然都可以简化为非常简单的排序。提升像Nat这样的种类将需要存在多种排序类型/构造函数，并且提升Fix将需要更高级的排序种类，这也不在原始排序系统中涵盖。

这并不是技术上的障碍，像Coq或Agda（依赖类型语言）这样的语言有整个无限的这些栈，但是GHC最近才增加了一种系统。它尚未实现任何复杂的排序系统，也许在未来我们会得到一个。

- Daniel Gratzer