理解Haskell类的种类

Kev*_*ith 5 haskell

看一下Learn You a Haskell的一个kind例子:

data Frank a b = Frank {frankField :: b a} deriving (Show)

LYAH讨论:

我们看到弗兰克有一种* - >(* - >*) - >*第一个*代表a而(* - >*)代表b.

当我想到一个例子时,这对我来说很有意义:Frank String Maybe = Frank {frankField :: Maybe String}.

但我对如何思考kind右手方面感到困惑

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

由于返回类型frankField :: b a,怎么能kindFrank为:

* -> (* -> *) -> * -- what does the right-most * represent?

为什么右手边kind等于*

Dav*_*vid 10

嗯,Frank右边是构造函数,值没有种类,它们有类型.类型指的Frank是左侧,它是一个类型构造函数.将值构造函数重命名为MkFrank:

data Frank a b = MkFrank {frankField :: b a} deriving (Show)
Run Code Online (Sandbox Code Playgroud)

值构造函数的类型是

MkFrank :: b a -> Frank a b
Run Code Online (Sandbox Code Playgroud)

和类型构造函数的类型是

Frank :: * -> (* -> *) -> *
Run Code Online (Sandbox Code Playgroud)

这表示Frank采用一个(具体)类型(*)和一个类型构造函数,它接受一个类型((* -> *))并给你一个类型(最后一个*).这类似于具有类型的函数A -> (B -> C) -> D:它采用"具体"值和函数(获取给定另一个值的值的方法)并且它为您提供"具体"值,不同之处在于我们正在处理类型而不是价值观.

作为旁注,类型对类型类的工作方式略有不同(尽管类中没有涉及类).有一种特殊的叫做Constraint代表可以=>在签名的左侧出现的东西.


Ben*_*Ben 5

首先是一些重要的概念点:

  1. 类型的存在是为了“限定”一组可以以相同方式处理的(在某种意义上)。类型存在于值级别的“上一级”,在类型级别。

  2. 种类的存在是为了“限定”一组可以以相同方式处理的类型1(在某种意义上)。种类存在于类型级别的“上一级”,在种类级别。

在 form 的任何定义中data ... = ...,您都在做两件事:

  1. 将新的可能实体添加到值级别。定义的右侧给出了可能的新值的“形状”(构造函数本身就是值,作为函数)。这使用类型级别的东西来谈论新值的“形状”(因为这是类型的用途),但声明的东西是值。

  2. 将新实体添加到类型级别。定义的左侧给出了可能的新类型的“形状”(类型构造函数本身是类型级别的东西)。

所以希望你能看到种类的概念不能应用于整个等式的右侧,因为它在谈论价值级别的事情。它使用一些类型级别的东西来谈论值,这些东西有种类。左侧整体确实“有种”,因为它引入了一种新的类型,但那种总是*如此,所以不是很有趣。左侧声明的类型构造函数可以有一种更有趣的类型。

让我们更详细地看一个简单的例子:

data Maybe a = Nothing | Just a
Run Code Online (Sandbox Code Playgroud)

在这里,我们已经声明了形式Nothing和形式的Just a新事物是值,形式的新事物Maybe a是类型(等式“链接”了a两边,所以它Just a是类型Maybe a,其中的a是相同的变量)。

Just本身就是一个构造函数,可以看作是一个存在于值级别的函数,因此有一个类型;它的类型是a -> Maybe a. Thea有一个 kind,因为它是一个类型级别的东西,但是无论Nothing, Just,整个Just a,还是整个右手边Nothing | Just a都不能有意义地说有一个 kind。

在左侧,整体Maybe a具有 kind *(因为您使用声明来声明新数据类型data,其中具有值的类型,数据声明的整个左侧始终具有 kind *)。Maybe本身也被引入为类型构造函数;因为它需要一个参数,所以它必须有一个类似___ -> *,我们需要填写空白。

要知道应填空的种类,a即定义中的类型变量的种类,我们需要知道a在RHS上是如何使用的。我们可以看到它只在模式中使用Just a。我们知道这Just a价值层面上的新事物的形式,所以a一定是Just可以应用的某些价值集的类型。有值的类型是*,所以a必须是这种类型(这就是我们如何避免像 那样不合理的东西Just Maybe)。所以这让我们得出结论,Maybe有种* -> *

回到你的例子,这一切都非常相似,除了引入的新类型构造函数与引入的新值构造函数具有相同的名称(都是Frank)。这不会导致问题,因为它们存在于不同的命名空间2 中的不同级别。但永远记住,仍然有两种不同的东西;Frank右边的the 是一个值构造函数,因此谈论它的类型没有意义。在Frank从左侧是一个类型构造,里面确实有一个样。

但是,这里的新类型构造函数Frank有两个参数,因此它必须是类似于___ -> ___ -> *. 同样,我们需要查看右侧以了解如何a以及b习惯于了解它们的种类。

这两个变量的唯一用途是在值构造函数的单个字段的类型中Frank;这种类型是b ab atotal 是将要存储在此字段中的值的类型,因此它必须是 kind *。这意味着它b是一种类似___ -> *.

现在我们理论上被卡住了。a仅用作 的参数b,并且我们仍然有一个空格作为 的参数类型填充b,因此无论我们分配给哪种类型都a可以使用3,但这会改变类型b以及类型构造函数Frank种类多态性的概念适合这里,但默认情况下 Haskell 只是将这些种类默认为*. 所以a有kind *b有kind * -> *,因此类型构造函数Frank有kind * -> (* -> *) -> *

Frank String Maybe(或者实际上Frank a b当我们是多态时)Frank应用于两个(类型级别)参数,所以它有 kind *; 这对于它是一种值是必要的。Frank (Just "foo")在类型的值Frank String MaybeFrank是在所述类型的值b a -> Frank a b,并且frankField是在所述类型的值Frank a b -> b a; 这些都没有种类(并且它们的所有类型都有 kind *)。

TLDR:类型FrankIS b a -> Frank a b,该样的Frank* -> (* -> *) -> *,但是这两个事实,因为他们都在谈论只有两个是真的不同命名实体Frank; 不可能理智地谈论同一事物的种类和类型,因为种类和类型在完全不同的层面上限定事物。


1我的第一个谎言;种类限定“类型级别的事物”,但并非 Haskell 中可以存在的所有类型级别的事物都是严格意义上的类型(无论如何取决于您的定义)。具有类型 like 的事物* -> *是“类型级实体”,但它们不是可以与值建立类型关系的事物。

2总是可以纯粹从给定名称出现的位置知道它应该在类型名称空间还是值名称空间中查找,因此编译器永远不会混淆类型名称和值名称。但是,在您熟悉 Haskell 之前,这对读者来说并不总是正确的!

3我可以通过使用KindSignatures扩展名显式声明它们来证明这适用于其他类型:

{-# LANGUAGE KindSignatures #-}

data Frank (a :: * -> *) (b :: (* -> *) -> *)  = Frank {frankField :: b a} deriving Show

data Strange (a :: * -> *) = Strange (a Int)
Run Code Online (Sandbox Code Playgroud)

然后在 GHCI 中:

? :t Frank
Frank :: b a -> Frank a b

? :t Frank (Strange (Just 1))
Frank (Strange (Just 1)) :: Frank Maybe Strange

? :k Frank
Frank :: (* -> *) -> ((* -> *) -> *) -> *
Run Code Online (Sandbox Code Playgroud)