Haskell高阶类型编程中是否存在符合generativity定义的类型级表达式？

核心解答 #

你对Generativity定义的适用前提和相等性语义存在两处核心偏差，下面逐个回应你的疑问：

1. 推导过程的问题 #

你的推导混淆了类型的定义相等（句法相等）和归约后的外延相等，同时错误地将类型族归约后的结果代入了Generativity的定义条件：

Generativity原始定义中的f a ~ g b是对未归约的类型应用项的句法相等判断，而非归约后最终结果的相等。你举的例子中Maybe Int是G String归约后的结果，并不等于未归约的G String本身的句法结构，自然不能套用f a ~ g b的前提。
另外你给出的IsGenerative类的定义不符合GHC的约束规则：原生~无法比较未饱和类型族，因此该约束本身无法对包含类型族的情况生效，基于此得到的推论自然存在偏差。

2. 变量取值范围的假设不合理 #

论文中讨论Generativity时，量化的变量f、g的范围默认是刚性类型构造器（即data/newtype定义的类型构造器，以及饱和的可注入类型族），并不包含未饱和的类型族：

• 未饱和类型族本身不属于合法的类型应用头符号，无法出现在f a这类应用结构的头位置，自然不存在满足f a ~ g b的前提，所以说未饱和类型族不具备Generativity属性，并不是无意义的循环判断，而是符合类型系统语法约束的结论。
  你将未饱和类型族纳入量化范围，属于超出了原始定义的讨论域。

3. 你确实误解了量化规则 #

原始定义的完整量化逻辑应该是：

对于任意刚性类型构造器g :: Type -> Type，任意类型a, b :: Type，如果未归约的类型应用项f a与g b定义相等，则f与g定义相等。
你不仅扩大了g的取值范围，还将~的语义替换成了归约后的外延相等，和原始定义的规则不符。

4. 存在大量满足Generativity属性的类型级表达式 #

所有Haskell中通过data/newtype定义的类型构造器都满足该属性，比如Maybe、[]、Either e（偏应用的二元构造器也满足）：

• 对Maybe来说，任何未归约的类型应用项Maybe a如果和另一个刚性构造器的应用项g b句法相等，那么g必然是Maybe，完全符合Generativity的定义。
  你之前的反例不成立，是因为你用了归约后的结果来替换未归约的应用项，不符合定义的前提要求。

内容的提问来源于stack exchange，提问作者user1726343