在“Haskell 中的高阶类型级编程”一文中， anf :: Type -> Type被定义为“生成式”，如下所示：

定义（生成性）。f 是生成的 ? fa~gb ? f~g

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

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

反过来说：

F :: Type -> Type是生成的，如果没有G :: Type -> Type，除了F这样存在A, B :: Type于其中F A ~ G B

该论文继续对不饱和类型族的生成性（它们不是生成性的）进行了陈述。据我了解，为了能够形成不饱和类型族是否是生成的命题，变量的f, g :: Type -> Type范围应该涵盖类型族和类型构造函数。请注意，这意味着~inf ~ 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

正如我之前所说，我们实际上无法Maybe ~ G在 GHC 中形成命题（因为G未饱和），但是如果F ~ G将其理解F为G“定义上等于”，则很明显Maybe /~ G. 因此Maybe，在论文中定义的意义上，它似乎实际上并不是生成性的。在我看来，任何data/newtype都容易受到类似的推理序列的影响。

那么我哪里出错了？

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

我是否误解了生成性陈述中变量的量化方式？

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

回答