Coyoneda 没有更高等级的类型，但实际上它是什么类型？

Question

Yoneda 只要设置了更高级别的扩展名，就具有有效的类型：

newtype Yoneda f a = Yoneda (forall b. (a -> b) -> f b)这产生了类型(forall b. (a -> b) -> f b) -> Yoneda f a。

b由消费者挑选Yoneda，因此不会出现在newtype声明的 LHS 上。

Coyoneda但是，对我来说没有意义：

data Coyoneda f a = forall b. Coyoneda (b -> a) (f b)这产生(b -> a) -> f b -> Coyoneda f a.

b被明确量化，但量词似乎不在正确位置呈现类型变量等级 2。尽管如此b，并未在data声明的 LHS 中列出。那是什么？几乎是存在的？这只是一个没有受过教育的猜测，因为我不太了解存在量词，并假设 Haskell 不支持它们。

Answer 1

data Coyoneda f a = forall b. Coyoneda (b -> a) (f b)

也可以用 GADT 语法编写：

data Coyoneda f a where
  Coyoneda :: forall b. (b -> a) -> f b -> Coyoneda f a

显式量化是可选的。

Coyoneda ::               (b -> a) -> f b -> Coyoneda f a
Coyoneda :: forall f a b. (b -> a) -> f b -> Coyoneda f a

所以你猜对了：b这里是存在量化的，因为它没有出现在Coyoneda数据构造函数的结果类型中。

@IvenMarquart，当你在构造函数上进行模式匹配时，你会得到一个新的类型，你可以使用 `ScopedTypeVariables` 来捕获。`f (Coyoneda g (b :: b)) = ...`。同样重要的是，你不能在 `Coyoneda` 上懒惰地进行模式匹配，所以 `let Coyoneda fx = blah in bloop` 是一个错误。 (2认同)
@IvenMarquardt：如果你更喜欢普遍而不是存在主义，你可以通过`unCoyoneda :: Coyoneda fa -> (forall b. (b -> a) -> fb -> r) -> 将两者联系起来r`。类型变量 `b` 不能出现在消费者的“结果”类型 `r` 中，因为它会超出其作用域。或者，您可以将一个存在视为一对类型，这里是 `b`，其值取决于该类型，这里相当于 `(b -> a, fb)`。 (2认同)