13

谁能解释或猜测GHC 用户指南第 7.9.2 节中讨论的数据类型提升限制背后的动机？

以下限制适用于促销：

  • 我们只推广类型为 的数据类型* -> ... -> * -> *。特别是，我们不推广更高种类的数据类型，例如data Fix f = In (f (Fix f))，或种类涉及提升类型的数据类型，例如Vec :: * -> Nat -> *.

特别是，我对有关提升类型的最后一点感兴趣，例如Vec :: * -> Nat -> *. 推广一些这样的类型似乎很自然。在尝试将我的一个库转换为对各种幻像类型使用特定的提升类型而不是对所有内容使用类型时，我很快就遇到了它*，以提供更好的文档等。

通常，像这样的编译器限制的原因会在你稍微思考一下的情况下跳出来，但我没有看到这个。所以我想知道它是否属于“还不需要，所以我们没有构建它”或“那是不可能/不可判定/破坏推理”的类别。

4

2 回答 2

21

如果您提升由提升类型索引的类型，则会发生一件有趣的事情。想象我们建造

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)

另一个解决方法是允许异构方程，就像我十五年前在依赖类型理论中所做的那样。事物之间不可避免地存在等式，它们的种类在句法上并不明显。

后者是目前受青睐的计划。据我了解，您提到的政策被采纳为持有立场，直到具有异构平等的核心语言的设计（如 Weirich 及其同事提出的）已经成熟实施。我们生活在有趣的时代。

于 2014-01-18T17:31:11.580 回答
4

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

  values : type : kind : sort : ...

请注意，虽然我们有一个非常复杂的类型系统，其中包含数据类型，但所有类型仍会升级为非常简单的类型。提升种类Nat需要不止一种排序类型/构造函数，提升Fix需要更高排序的种类，这也没有包含在原始排序系统中。

这不是技术障碍，像 Coq 或 Agda（依赖类型语言）这样的语言有一个完整的无限堆栈，但 GHC 直到最近才发展出一种类型的系统。它只是还没有实现任何复杂的排序系统，也许将来我们会得到一个。

于 2014-01-18T16:29:24.457 回答