haskell - 关于 Haskell GADT

This question already has an answer here:

Kind Signatures

(1 个回答)


8年前关闭。




任何人都可以解释或给出解释 * -> * 下面代码的一部分的链接吗？

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

非常感谢。

最佳答案

Kind signatures 。它们可用于显式定义类型构造函数的元数。 * 的意思是“任何类型”，其余的有点像普通函数类型。在这种情况下，我们甚至有一个部分应用程序:

BinaryTree t :: * -> *

意思是“BinaryTree t 是一个从类型到类型的函数”，这是有道理的，因为您可以将它应用于另一种类型:

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

BinaryTree t 部分应用于类型 a ，为您提供类型 BinaryTree t a :: * 。 (BinaryTree t) 本身还没有完全应用，因此有一个 * -> * ，你仍然需要应用它来获得一个简单的类型。 (这与 f 1 时 Int -> Int 仍然具有 f :: 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 :: * -> * -> *