了解数据类型、类型类的签名，并使数据类型成为类型类的实例

Question

一直在阅读为伟大的利益而学习 Haskell！并且在理解实例和种类方面有很大的麻烦。

Q1：所以Tofu t 中的类型t 充当了一个带有类型签名(* -> (* -> *)) -> * 的函数？而tofu 的整体签名是* -> *，不是吗？因为(* -> *) -> * 导致*，(* -> (* -> *)) -> * 也是如此

Q2：当我们要创建类型类Tofu t的Frank a b实例时，数据类型Frank a b也必须与t具有相同的类型。这意味着a 是*，b 是* -> *，b a 是(* -> *) -> *，结果是*。对吗？

Q3：tofu x 中的x 代表j a，因为两者都有* 的类型。 Frank 及其同类 (* -> (* -> *)) -> * 应用于 x。但我不确定将j a 呈现为x 将如何区分tofu x 中的x 即j a 和Frank x 中的x 即a j。

我对在数据类型或类中包含函数的想法有点陌生（例如：Frank a b 中的 b 或 Tofu t 中的 t），这有点令人困惑

我将链接留在这里，因为引用会使帖子看起来不必要地长。 link

class Tofu t where
  tofu :: j a -> t a j

data Frank a b = Frank {frankField :: b a} 

instance Tofu Frank where
  tofu x = Frank x 

Answer 1

第一季度：

因此，Tofu t 中的类型 t 充当具有种类签名 (* -> (* -> *)) -> * 的函数？

t 的种类是 * -> (* -> *) -> *，或者更明确地说是 * -> ((* -> *) -> *)，而不是 (* -> (* -> *)) -> *。

而且豆腐的整体种类签名是* -> *，不是吗？

tofu 没有 kind 签名，只有类型构造函数有；它的类型是*。它的参数和结果的类型也是如此。任何功能都一样。

Q2：你从一个错误的假设开始：instance Tofu Frank 使Frank 类型构造函数成为Tofu 的实例，而不是Frank a b。所以Frank 必须与t 具有相同的种类，而不是Frank a b（具有* 的种类）。

b a 将是 (* -> *) -> *

不，b a 是一种b 的应用程序* -> * 到a 的一种*，所以应用程序有一种*。就好像b 是x -> y 类型的函数，而a 是x 类型的值，b a 将具有y 类型，而不是(x -> y) -> x：只需替换x 和@ 987654350@*。

第三季度：

豆腐x中的x代表j a

“有类型”，而不是“代表”。

因为两者都有 *

x 没有类型，因为它不是类型。

Frank with its kind (* -> (* -> *)) -> * 应用于 x

不，在

tofu x = Frank x

它是应用于x 的Frank data constructor，而不是类型构造函数。这是一个带有签名b a1 -> Frank a1 b 的函数（重命名a，这样你就不会将它与tofu 混淆）。所以b ~ j 和a1 ~ a。

Answer 2

Alexey 已经尝试回答您的问题。我会用任何相关的细节来解释你的例子。

class Tofu t where
  tofu :: j a -> t a j
          ^^^    ^^^^^
          ^^^^^^^^^^^^

突出显示的位必须具有类型*。 （类型级别）箭头两侧的任何内容都必须具有类型*^[1]，并且箭头术语本身（即整个j a -> t a j 术语）也具有类型* .事实上，任何可以被一个值所占据的“类型”^[2] 都有种类*。如果它有任何其他类型，则不能有任何值（它只是用于在其他地方构造适当的类型）。

因此，在tofu 的签名中，以下内容成立

j a :: *
t a j :: *

因为它们被用作“居住”类型，因为它们是 (->) 的参数。

这些是唯一限制类的东西。特别是，a 可以是任何类型。与PolyKinds^[3]

a :: k   -- for any kind k
j :: k -> *
t :: k     ->   (k -> *) -> *
     ^          ^^^^^^^^    ^
 kind of a      kind of j   required since is used as inhabited type by ->

所以我们找到了所需的t。

我们可以对Frank 使用类似的推理。

data Frank a b = Frank {frankField :: b a}
     ^^^^^^^^^                        ^^^

同样，突出显示的位必须具有类型*，因为它们可以具有值。否则没有约束。概括地说，我们有

a :: k
b :: k -> *
Frank a b :: *

因此

Frank :: k -> (k -> *) -> *

我们可以看到Frank 的种类与Tofu 所需的种类相匹配。但它也适用于更具体的类型，例如：

data KatyPerry a b = KatyPerry a (b Int)

尝试推断她的种类，并检查它是否比Tofu要求的种类更具体。

---

[1] 如果我们假设TypeInType，即使是善良级别的箭头也是如此。没有TypeInType，“种类的种类”被称为sorts，没有人担心它们；在那个级别通常没有什么有趣的事情发生。

[2] 我将“类型”放在引号中，因为从技术上讲，只有类型为 * 的东西才称为类型，其他所有东西都称为 类型构造函数。我试图准确地说明这一点，但我找不到一种不尴尬的方式来同时引用两者，并且段落变得非常混乱。所以“输入”它是。

[3] 没有PolyKinds，任何像k 这样的无约束类型都会被专门化为*。这也意味着Tofu 的种类可能取决于您首先碰巧将它实例化的类型，或者您是在同一模块中还是在不同模块中的类型上实例化它。这不好。 PolyKinds 不错。