haskell - 有什么可生成的吗？

Question

在论文"Higher-order Type-level Programming in Haskell" ，一个 f::Type -> Type 被定义为“生成”的，方式如下:

Definition (Generativity). f is generative ⇔ f a ~ g b ⇒ f ~ g

我将按照我的理解明确写出预期的量化:

type IsGenerative :: (Type -> Type) -> Constraint
class (forall g a b. f a ~ g b => f ~ g) => IsGenerative f

反过来说:

F :: Type -> Type is generative if there is no G :: Type -> Type besides F such that there exist A, B :: Type for which F A ~ G B

该论文继续对不饱和类型家族的生成性(它们不是生成性的)进行了陈述。据我了解，为了能够形成不饱和类型族是否可生成的命题，变量 f, g::Type -> Type 也应该涵盖类型族作为类型构造函数。请注意，这意味着 f ~ g 中的 ~ 必须表示比 GHC 的 (~)::(Type -> Type) 更抽象的定义相等意义 -> (Type -> Type) -> Constraint，不能应用于不饱和类型族。

现在问题来了:似乎没有任何东西是生成的。您会期望像 Maybe::Type -> Type 这样的数据类型构造函数是生成的，但我可以轻松构造一个不同的类型族 G::Type -> Type和 A, B::Type 其中 F A ~ G B (尽管 F/~ G)。

type G :: Type -> Type
type family G a
  where
  G _ = Maybe Int

data Dict c
  where
  Dict :: c => Dict c

lhs :: Dict (Maybe Int ~ G String)
lhs = Dict

正如我之前所说，我们实际上不能在 GHC 中形成命题 Maybe ~ G(因为 G 没有饱和)，但是如果 F ~ G 的意思是“F 定义上等于 G”，很明显 Maybe/~ G。所以看起来 Maybe 实际上并不是论文中定义的意义上的生成。在我看来，任何 data/newtype 都容易受到类似推理序列的影响。

那么我哪里错了？

我的假设是否允许 F, G 跨越类型家族以及类型构造函数？如果不是，生成性似乎是一个相当微不足道的属性:“我们无法形成类型族是否具有生成性的命题，因此类型族不是生成性的”。

我是否误解了在生成性陈述中变量是如何量化的？

实际上是否有任何类型级表达式 f::Type -> Type 满足生成的形式属性？

Answer 1

呃，你想多了。 ~ 确实是来自 GHC 的。如果您愿意，请将声明“不饱和类型族不是生成”替换为“如果我们扩展 ~ 以允许不饱和类型族¹，那么它们将不能保证生成< sup>2”。后一个事实是(部分)我们不费心扩展 ~ 以允许不饱和类型族的原因——与其他类型表达式相比，它对它们的用处要小得多。

如果他们对论文中的这种划分不准确，那只是写得有点草率，就像我们都曾经做过的那样。

¹ 你可以通过简单地在 ~ G/Maybe 的情况 但不是另一个。

² 事实上，我相信它更强大:它们将被保证不会生成。