限制数据类型促销的动机

Question

任何人都可以解释或猜测GHC用户指南第7.9.2节中讨论的数据类型提升限制背后的动机吗？

以下限制适用于促销:

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

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

通常情况下编译器限制的原因会引起一些思考,但我没有看到这一点.所以我想知道它是否属于"不需要,所以我们没有建立它"或"那是不可能的/不可判断的/破坏推理".

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

但是在那时定义的系统FC中,等式约束必须在两侧都有相同类型的类型,所以这个例子并不是一个小问题.

一个修复是使用第一个约束的证据来修复第二个约束,但是我们需要依赖约束

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

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

这是后一个目前受到青睐的计划.据我了解,您提到的政策被采纳为持有立场,直到具有异质平等的核心语言(由Weirich及其同事提出)的设计已经成熟到实施.我们生活在有趣的时代.