在“向您学习Haskell"一书中所做的假设是什么?什么时候推导那种? [英] What is the assumption made in "Learn You a Haskell" when deducing the kind?

问题描述

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

This question is not subjective. A very specific verb is used in the referenced book, and I'd like to understand what the implication of that phrasing is, because I'm afraid I'm misunderstanding something.

从了解Haskell ，下一段是第三行，也是最后一行，包含我们假设 * ".

From Learn You a Haskell, the following paragraph is the third and last one containing "we assume *".

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

现在我们要使其成为 Functor 的实例. Functor 想要类型为 *->的类型.* ，但是 Barry 看起来不像那样. Barry 是什么类型?好吧，我们看到它需要三个类型参数，因此它将是 something->东西->东西->* .可以肯定地说 p 是具体类型，因此具有 * 的一种.对于 k ，我们假定 * ，因此，扩展名， t 具有一种 *->* .现在，让我们用用作占位符的 something 替换这些类型，我们会看到它具有(*-> *)->*->*->* .

And now we want to make it an instance of Functor. Functor wants types of kind * -> * but Barry doesn't look like it has that kind. What is the kind of Barry? Well, we see it takes three type parameters, so it's going to be something -> something -> something -> *. It's safe to say that p is a concrete type and thus has a kind of *. For k, we assume * and so by extension, t has a kind of * -> *. Now let's just replace those kinds with the somethings that we used as placeholders and we see it has a kind of (* -> *) -> * -> * -> *.

我们为什么要承担一切呢?读完我们假设X(即我们假设X为真)"后，我自然认为我们也应该考虑X为假的情况.在示例的特定情况下， t 不能为(*-> *)->* 和 k 类型为(*-> *)?如果是这种情况，无论 t 和 k 实际上是什么， t k 仍将是具体类型，不是吗?

Why are we assuming anything at all? Upon reading "we assume X (i.e. we assume that X is true)" it is natural for me to think that we should also consider the case that X is false. In the specific case of the example, couldn't t be of kind (* -> *) -> * and k of kind (* -> *)? If this was the case, whatever t and k actually were, t k would still be a concrete type, no?

我看到整个推理过程都经过了编译器的检查，但我认为编译器没有假设.如果是这样，我想知道是什么，如果没有，那么我恐怕会错过本段的含义.

I see that the whole line of reasoning is then checked against the compiler, but I don't think the compiler assumes. If it does, I'd like to know what, if it doesn't then again I'm afraid I'm missing the meaning of the paragraph.

推荐答案

实际上，编译器确实假定！但是您可以通过PolyKinds扩展程序来要求它.您可以在此处此处进行详细了解..启用该扩展名后， Barry 的类型将为 forall k.(k-> *)->k->*->* .

In fact, the compiler does assume! But you can ask it not to with the PolyKinds extension. You can read about it in more detail here. With that extension turned on, the kind of Barry will be forall k. (k -> *) -> k -> * -> *.

这篇关于在“向您学习Haskell"一书中所做的假设是什么?什么时候推导那种?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！