Haskell：[(Type,Type)]种类的居民是什么？如何强类型表示类型级配对列表？

这个问题戳中了Haskell类型系统里一个容易混淆的点——类型和种类的层级关系，咱们一步步来理清楚并解决它。

为什么原来的写法会失败？ #

首先得明确几个关键概念：

• Bool是一个类型，它的种类是Type（也就是旧版Haskell里的*）。
• 普通元组构造器(,)的种类是Type -> Type -> Type，所以(Bool, Bool)是一个类型，它的种类同样是Type。
• 你写的[(Type, Type)]是一个种类，它表示“由种类为(Type, Type)的元素组成的列表”——但(Type, Type)本身是两个种类的配对，我们根本没办法写出一个类型让它的种类是(Type, Type)，这就是为什么:k ('[(Bool,Bool)] :: [(Type,Type)])会报错。

简单说：你想要的是“类型级的配对列表”，但普通元组是“值级/类型级的元组类型”，两者不在同一个层级上。

解决方案：用DataKinds自定义类型级配对 #

要实现类型级的强类型配对列表，我们需要借助GHC的扩展把“配对”这个概念提升到类型级。具体步骤如下：

1. 启用必要的GHC扩展 #

首先需要开启几个核心扩展：

{-# LANGUAGE DataKinds, TypeOperators, KindSignatures #-}

• DataKinds：允许把数据类型提升为种类，把数据构造器提升为类型构造器。
• TypeOperators：支持自定义中缀类型算子，让代码更直观。
• KindSignatures：允许显式标注种类，增强可读性。

2. 定义类型级配对结构 #

我们可以自定义一个用于表示类型配对的数据类型，然后通过DataKinds把它提升到种类层面：

-- 自定义中缀类型配对算子，优先级设为5
infixr 5 :&:
data (:&:) a b = a :&: b

通过DataKinds提升后：

• (:&:)成为一个种类，专门用来表示类型配对的种类。
• ':&:'（注意前面的单引号）成为一个类型构造器，它的种类是Type -> Type -> (:&:)，可以用来构造具体的类型配对。

3. 构造类型级配对列表 #

现在我们就可以定义由类型配对组成的列表了：

-- 一个包含两个类型配对的类型级列表
type MyTypePairs = '[ Bool :&: Bool, Int :&: String ]

4. 在GHCi中验证 #

现在去GHCi里检查种类：

-- 检查列表的种类
:k MyTypePairs
-- 输出：MyTypePairs :: [(:&:)]

-- 检查单个配对的种类
:k Bool :&: Bool
-- 输出：Bool :&: Bool :: (:&:)

完全符合我们的需求——每个列表元素都是(:&:)种类的类型配对，整个列表的种类是[(:&:)]。

另一种写法：用命名的配对构造器 #

如果你更喜欢前缀式的写法，也可以用命名的构造器：

data TypePair a b = TypePair a b

type MyPairs = '[ 'TypePair Bool Bool, 'TypePair Int String ]

-- GHCi验证
:k MyPairs
-- 输出：MyPairs :: [TypePair]

效果和中缀式的:&:完全一样，只是写法不同。

总结 #

核心思路就是：用DataKinds把“类型配对”这个概念从值级/类型级提升到种类级，这样我们就能构造出由类型配对组成的强类型列表，完全避免了普通元组带来的种类不匹配问题。

内容的提问来源于stack exchange，提问作者lando