haskell - 限制数据种类推广的动机

Question

谁能解释或猜测 7.9.2 of the GHC user guide 部分中讨论的数据类型提升限制背后的动机？ ?

The following restrictions apply to promotion:

• We only promote datatypes whose kinds are of the form * -> ... -> * -> *. In particular, we do not promote higher-kinded datatypes such as data Fix f = In (f (Fix f)), or datatypes whose kinds involve promoted types such as Vec :: * -> Nat -> *.

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

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

Answer 1

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

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 及其同事提出的)已经成熟实现。我们生活在有趣的时代。