关于 Haskell GADT [重复]答案

【问题标题】：About Haskell GADTs [duplicate]关于 Haskell GADT [重复]
【发布时间】：2013-05-06 17:39:41
【问题描述】：

谁能解释或给出解释 * -> * 下面部分代码的链接？

data BinaryTree t :: * -> * where
   Leaf :: BinaryTree Empty a
   Branch :: a -> BinaryTree isempty a -> BinaryTree isempty' a -> BinaryTree NonEmpty a

非常感谢。

【问题讨论】：

就像值有类型一样，types have kinds.
@dave4420：是的，我认为这个问题只是那个问题的重复。
从外部开始的好地方 SO：haskellWiki/Kind.
@TikhonJelvis 另一个问题是另一个问题，需要更多背景知识，例如“直到添加了一个 Kind 签名，它概括了 Cons 构造函数的受约束类型。” -- 在这个问题上，关于这些词的知识还不可用。

标签： haskell

【解决方案1】：

Kind signatures。它们可用于显式定义类型构造函数的数量。 * 表示“任何类型”，其余的kind 与普通函数类型类似。在这种情况下，我们甚至有一个部分应用程序：

BinaryTree t :: * -> *

表示“BinaryTree t 是从类型到类型的函数”，这是有道理的，因为您可以将其应用于另一种类型：

f :: (BinaryTree t) a -> (BinaryTree t) b
         * -> *     *        * -> *     *

BinaryTree t 部分应用于a 类型，为您提供BinaryTree t a :: * 类型。 (BinaryTree t) 单独还没有完全应用，因此有一种* -> *，你仍然需要应用它来获得一个简单的类型。（这与f 1 在f :: Int -> Int -> Int 仍然具有Int -> Int 类型时的工作方式相同）

请注意，您可以混合使用普通的“arity 声明”，提及类型的隐式参数和种类签名，就像这里所做的那样。我们也可以这样写BinaryTree：

data BinaryTree t a  -- normal variant

或者像这样：

data BinaryTree :: * -> * -> *  -- fully "kinded"

在这两种情况下，编译器都知道BinaryTree 将采用两个类型参数。

它是干什么用的？首先，就像链接中描述的那样，有时您需要或想要显式声明您的类型应该采用多少类型参数。当您使用 不同种类 而不是 *（又名 DataKinds）时，可能会出现另一个更有趣的情况。看看这个：

data Empty = Empty | NonEmpty
data BinaryTree (t :: Empty) (a :: *) :: * where 
   -- ...

哦，ghci 可以让您查看种类，以防您不确定。它的工作方式与:t 相同：

Prelude> :k Either
Either :: * -> * -> *

【讨论】：

非常感谢您的帮助

【解决方案2】：

* -> * 是一种类型签名的示例。种类可以被认为是“类型的类型”。也就是说，就像值有类型一样，类型也有种类。

种类

如果我们忽略一些语言扩展，种类仅由两个构造函数构建：

* 表示正确的类型，即那些被值所占据的类型，例如Int、Char、Maybe Int、[Char]。
k1 -> k2 形式的种类（其中k1 和k2 本身就是种类）指定类型构造函数， 即需要用一个或多个类型参数完成的类型表达式形成适当的类型。例如：类型构造函数Maybe 需要一个类型为* 的参数才能生成正确的类型，因此它有类型* -> *；同样适用于列表的类型构造函数[]，因此也有种类* -> *；类型构造函数Either 采用两个类型为* 的参数来形成正确的类型（例如Either Int Char 或Either (Maybe Int) [Char]），因此它具有类型* -> * -> *。

高阶类型的种类

请注意，类型构造函数-> 关联到右侧。即* -> * -> * 与* -> (* -> *) 相同。对于所谓的高阶类型（即作为类型构造函数而不是正确类型作为其参数的类型）的示例，首先考虑玫瑰树的类型Rose：

data Rose a = Branch a [Rose a]

这是* -> * 的一阶类型。但是，如果我们通过抽象它对列表的类型构造函数的使用进行概括，我们会得到

data GRose f a = Branch a (f a)

它有一种(* -> *) -> * -> *，因此是二阶类型。

二阶类型的另一个例子是类型级定点运算符Fix：

newtype Fix f = In {out :: f (Fix f)}

实际上几乎不会出现高于两个的订单类型。我见过的为数不多的例子之一是Fix“提升为善良* -> *：

data HFix h a = HIn {hOut :: h (HFix h) a}

确实，HFix 和 ((* -> *) -> * -> *) -> * -> * 一样。

GHCi

GHC 的交互环境 (ghci) 提供命令 :kind（通常缩写为 :k）用于查询类型表达式的种类。例如：

> :k Either
Either :: * -> * -> *

> :k Either Int
Either Int :: * -> *

> :k Either Int Char
Either Int Char :: *

种类错误

只是一个程序可以包含类型错误，有可能引入类型错误。例如：

> :k Either Int Maybe
<interactive>:1:12:
    Expecting one more argument to `Maybe'
    In a type in a GHCi command: Either Int Maybe

这里我们为Either 提供了一个类型为* -> * 而不是* 的类型表达式作为第二个参数。

如果你将非函数类型的类型表达式（即*）应用于另一个类型表达式，这也是一个类型错误：

> :k Int Char
<interactive>:1:1:                                                               
    `Int' is applied to too many type arguments
    In a type in a GHCi command: Int Char

【讨论】：

【解决方案3】：

该符号用于表示kinds，类似于函数可以具有Int -> String 或a -> a 等类型

基本上* 表示任何具体类型，如Int。然后像BinaryTree 这样的类型构造函数采用具体类型来生成像BinaryTree Int 或BinaryTree Double 这样的具体类型。这由BinaryTree 的类型表示，即* -> *。

你可以在 ghci 中查看：

ghci> :k Int
Int :: *

ghci> :k Maybe
Maybe :: * -> *

ghci> :k Maybe Int
Maybe Int :: *

【讨论】：