在推导种类时，“Learn You a Haskell”中的假设是什么？

Question

这个问题不是主观的。参考书中使用了一个非常具体的动词，我想了解该措辞的含义，因为我担心我误解了一些东西。

从Learn You a Haskell 中，以下段落是包含“我们假设*”的第三段也是最后一段。

data Barry t k p = Barry { yabba :: p, dabba :: t k }  

现在我们想让它成为Functor. Functor想要那种类型，* -> *但Barry看起来没有那种类型。什么样的Barry？好吧，我们看到它需要三个类型参数，所以它将是something -> something -> something -> *. 可以肯定地说，这p是一个具体的类型，因此有一种*. 对于k，我们假设*并且因此推而广之，t有一种* -> *。现在让something我们用我们用作占位符的s替换这些种类，我们看到它有一种(* -> *) -> * -> * -> *.

我们为什么要假设任何事情？在阅读“我们假设 X（即我们假设 X 为真）”时，我很自然地认为我们还应该考虑 X 为假的情况。在示例的特定情况下，不能t是 kind(* -> *) -> *和kof kind(* -> *)吗？如果是这样的话，无论t和k实际上是，t k仍然是一个具体类型，不是吗？

我看到然后针对编译器检查了整个推理过程，但我认为编译器不会假设. 如果是这样，我想知道是什么，如果不是，那么恐怕我又错过了该段落的含义。

Answer 1

事实上，编译器确实假设！但是您可以要求它不要使用 PolyKinds 扩展。您可以在此处更详细地了解它。打开该扩展程序后，Barry将是forall k. (k -> *) -> k -> * -> *.