haskell - 关于 Haskell GADT

Question

这个问题在这里已经有了答案:





Kind Signatures

(1 个回答)


8年前关闭。




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

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

非常感谢。

Answer 1

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 :: * -> * -> *