PAYATHON 2026

GHC2024 中 ADT 与 GADT 的声明语法及 kind 标注有何区别？

数据小陈

在题目给出的例子中，这三种写法定义的数据类型结构相同：Door :: DoorState -> Type。构造器接收一个 String，对任意状态参数都返回 Door s。第三种写法也是完整的 GADT-style declaration；声明头是否写出参数名，与是否使用 GADT syntax 是两个独立的选择。

三种声明分别表达什么？

写法声明头的作用构造器的写法
data Door (s :: DoorState) = ...命名参数并标注其 kind使用传统声明语法
data Door :: DoorState -> Type where ...直接标注完整 kind显式给出构造器签名
data Door (s :: DoorState) where ...命名参数并标注其 kind显式给出构造器签名

GHC 的 GADT-style 声明可以使用带参数的声明头，也可以使用内联 kind signature。GHC 的声明语法说明列出了这两类声明头及其混合形式，第三种写法也在支持范围内。

Door 与 Door s 的 kind 要分开看

它们的 kind 分别是：

Door :: DoorState -> Type
s :: DoorState
Door s :: Type

Door 是尚未应用参数的 type constructor；应用参数后得到 Door s，其 kind 为 Type。

第一种声明中，:: DoorState 指定参数的 kind。这里，普通 data 声明的结果类型具有 kind Type，无需通过是否已经构造出值来推导。给类型变量添加 kind 标注的规则见 KindSignatures 文档。

两处 s 为什么不指同一个变量？

在题目这种 GADT-style 声明中，声明头的参数名不会绑定构造器签名里的同名变量。构造器签名会独立量化其中的类型变量，因此可以将签名中的变量改名为 t：

data Door (s :: DoorState) where
  UnsafeMkDoor :: { doorMaterial :: String } -> Door t

Door 的参数要求决定了 t 的 kind 是 DoorState。忽略记录字段的声明形式，构造器的类型可以写为：

UnsafeMkDoor :: forall (t :: DoorState). String -> Door t

改名不改变含义。t 出现在构造器的返回类型中，因此不是 existential type variable。这一作用域规则在 GHC 的 GADT syntax 文档中有说明。

使用 GADT syntax 就是在定义 GADT 吗？

普通 ADT 也可以使用 GADT syntax。题目里的构造器对任意 s :: DoorState 都能返回 Door s，没有把状态参数限制为某个具体状态。s 也没有出现在存储字段的类型里，因此这里仍是带 phantom type parameter 的普通 ADT。

返回类型细化可以用下面的定义说明：

data CheckedDoor :: DoorState -> Type where
  MkClosedDoor :: String -> CheckedDoor 'Closed

这个示例假设 DoorState 包含 Closed。该构造器只能返回 CheckedDoor 'Closed；匹配它时，类型检查器能够据此细化状态参数。GHC 将这种能力与单纯使用 GADT syntax 区分开来，详见 GADTs 文档。

怎样组织一个完整示例？

下面的完整示例补充了 DoorState 定义，并采用第三种写法：

{-# LANGUAGE GHC2024 #-}

module DoorExample where

import Data.Kind (Type)

data DoorState = Opened | Closed

data Door (s :: DoorState) where
  UnsafeMkDoor :: { doorMaterial :: String } -> Door s

closedDoor :: Door 'Closed
closedDoor = UnsafeMkDoor "wood"

openedDoor :: Door 'Opened
openedDoor = UnsafeMkDoor "wood"

同一个构造器可以创建这两种状态的门。如果要限制状态的创建方式，需要相应设计构造器和模块导出接口。

GHC2024 包含这里用到的 DataKinds、KindSignatures、GADTSyntax 和 GADTs。使用支持该语言版本的 GHC 时，只要没有额外关闭这些扩展，就无需逐个启用。具体可查阅 GHC2024 扩展列表。

应该去哪里查语法？

可以根据需要查阅以下资料：

  1. 传统声明语法：查 Haskell2010 Report 的 Algebraic Datatype Declarations。它提供基础语法，不覆盖 GHC 的全部扩展。
  2. GADT 构造器语法：查 GHC User’s Guide 的 Formal syntax for GADTs，其中有 BNF-style grammar，包括题目使用的 record constructor 形式。
  3. 某个 GHC 版本的具体解析规则：查对应版本源码中的 compiler/GHC/Parser.y。它包含实现使用的 grammar；声明是否最终合法，还涉及扩展开关与后续类型检查。

GHC2024 是一组语言扩展的集合。查阅时应选择与所用编译器版本对应的 User’s Guide，尤其不要把开发版文档中新增的语法直接当作该版本已经支持的功能。

备注：内容仅供参考。