掌握存在类型：haskell-exercises GADTs练习题深度解析，看懂ShowList与MysteryBox

gitblog_00074

320人浏览 · 2026-08-16 07:39:40

gitblog_00074 · 2026-08-16 07:39:40 发布

掌握存在类型：haskell-exercises GADTs练习题深度解析，看懂ShowList与MysteryBox

【免费下载链接】haskell-exercises A little course to learn about some of the more obscure GHC extensions. 项目地址: https://gitcode.com/gh_mirrors/has/haskell-exercises

haskell-exercises 是一个通过实战练习来掌握 GHC 语言扩展的开源教程项目，而 GADTs（广义代数数据类型） 正是它的第一课。本篇文章将带你从零开始，深度解析 GADTs 练习题背后的核心概念——存在类型（Existential Types），并用 ShowList 与 MysteryBox 这两个经典例子，帮你把"类型系统还能这样玩"的疑惑一次讲透。无论你是刚接触 Haskell 进阶特性，还是对类型安全充满好奇，这篇 GADTs 练习题解析都能帮你建立直观理解。🚀

haskell-exercises 是什么：先从普通列表的局限说起

haskell-exercises 一共包含 10 个练习模块，从 GADTs、FlexibleInstances 到 DataKinds、TypeFamilies、ConstraintKinds，层层递进地展示 GHC 各种语言扩展的威力。所有练习题都存放在各自的 src 目录下，比如第一课就在 01-GADTs/src/GADTs.hs 中给出了完整讲解，而 01-GADTs/src/Exercises.hs 则是留给你的空白题目。

要理解 GADTs，先看一个"痛点"：Haskell 中普通的列表是**同质（homogeneous）**的，也就是说所有元素必须是同一个类型：

data List a = Nil | Cons a (List a)

比如 Cons 2 (Cons 3 Nil) 可以正常求值，但你想把 "Tom"、25、True 塞进同一个列表？编译器直接拒绝。可问题是——如果我们只想对列表里的每个元素调用 show，为什么非要它们类型一致呢？我们真正需要的，只是"每个元素都有 Show 实例"这个保证而已。

ShowList 深度解析：存在类型由此诞生

GADTs 的威力在于：它允许你手写每个构造子的类型签名，从而打破普通 ADT 的两条铁律：

类型变量可以不出现在结果类型中；
构造子参数可以用类型类约束。

于是，01-GADTs/src/GADTs.hs 中给出了这样一个惊为天人的定义：

data ShowList where
  ShowNil  :: ShowList
  ShowCons :: Show a => a -> ShowList -> ShowList

注意 ShowCons 里的类型变量 a：它只存在于构造函数的内部作用域，外部无从得知它到底是什么类型，只知道它满足 Show 约束。这种类型变量，就叫做存在类型变量。正是它的存在，让 ShowCons "Tom" (ShowCons 25 (ShowCons True ShowNil)) 这种"混装"列表得以编译通过。

更有趣的是，为 ShowList 写 Show 实例时，代码和普通列表几乎一模一样，唯一区别是：模式匹配时我们完全不知道 head 的具体类型，只拿得到它带有 Show 实例这一条信息。

存在类型的"能力边界"：为什么只能 show？

这是 GADTs 练习题里最容易踩坑的地方。试着写一个 showListHead :: Show a => ShowList -> Maybe a，你会发现编译器报错：调用方可以自由选择 a 是 Int 还是 Bool，但存在类型根本不归调用方决定。

这个"谁来挑选类型"的问题，正是区分存在类型与高阶多态（RankNTypes，haskell-exercises 第五课）的关键。对存在类型来说，你能做的只有调用"对任意类型都成立"的函数，实际操作下来基本就是 show。所以题目的标准解法是把返回值固定成 Maybe String，先 show 再返回：

showListHead' :: ShowList -> Maybe String
showListHead'  ShowNil          = Nothing
showListHead' (ShowCons head _) = Just (show head)

MysteryBox 解析：类型参数随构造子而变

如果说 ShowList 展示的是"隐藏类型变量"，那么 MysteryBox 展示的则是 GADTs 的另一面——同一个类型参数，在不同构造子中被"钉死"成不同的具体类型：

data MysteryBox a where
  EmptyBox  ::                                MysteryBox ()
  IntBox    :: Int    -> MysteryBox ()     -> MysteryBox Int
  StringBox :: String -> MysteryBox Int    -> MysteryBox String
  BoolBox   :: Bool   -> MysteryBox String -> MysteryBox Bool

看到没？MysteryBox Int 只能由 IntBox 构造，MysteryBox String 只能由 StringBox 构造，环环相扣，像俄罗斯套娃一样一层包一层。🧩

模式匹配时，类型检查器替你"收窄分支"

MysteryBox 最妙的地方在于：写模式匹配时，GHC 会根据结果的类型自动排除不可能的构造子。比如：

getInt :: MysteryBox Int -> Int
getInt (IntBox int _) = int

你压根不需要写 EmptyBox、StringBox、BoolBox 的分支，因为类型已经告诉你：MysteryBox Int 只可能由 IntBox 产生。题目里 getInt' :: MysteryBox String -> Int 更是"陷阱题"——从 StringBox 里拿出 Int 是不可能的，答案只能是通过多层模式匹配一路"拆盒"到最底层的 IntBox。这正是 GADTs 练习题想教会你的：让类型替你排除错误分支。

更多 GADTs 练习题：从 HList 到类型安全的表达式

除了 ShowList 与 MysteryBox，01-GADTs/src/Exercises.hs 里还有一组由浅入深的题目，非常值得逐一挑战：

练习题	考察重点
CountableList	存在类型 + 自定义类型类约束
AnyList	无约束存在类型的能力上限
EqPair	存在类型与 Eq 实例的局限
HList	用类型参数记录每个元素的类型
HTree	类型层面的异构二叉树
Expr	用 GADT 构造"类型安全"的表达式语言

其中最惊艳的是 Expr：它用类型参数保证表达式良构（well-typed）——Add 只接受 Expr Int，Equals 只产生 Expr Bool，于是 eval :: Expr a -> a 根本不需要处理类型错误，因为"类型错误"在编译期就被消灭了。这就是 GADTs 从"奇技淫巧"走向"工程价值"的地方。

如何上手这套 GADTs 练习题？

想要亲自体验存在类型的魔力？只需要两步：

克隆仓库：git clone https://gitcode.com/gh_mirrors/has/haskell-exercises
进入练习目录并打开 REPL：进入 01-GADTs 目录后执行 cabal repl 或 stack repl；配合 ghcid -c "cabal repl" 还能获得实时的类型检查反馈。

建议先通读 GADTs.hs 的讲解部分，再动手填写 Exercises.hs 里的空白实现。遇到"为什么这里编译不过"的报错时，不妨回想本文的两个关键词：存在类型决定了你知道什么、不知道什么；类型参数则决定了 GHC 能替你排除哪些分支。

总结

通过 haskell-exercises 第一课的练习，我们完成了对 GADTs 的初步认识：ShowList 让你看到存在类型如何突破同质列表的限制，MysteryBox 让你体会类型参数驱动模式匹配的优雅。这两块基石，会一路支撑你后续理解 DataKinds 的类型级编程、TypeFamilies 的族函数，以及 ConstraintKinds 的约束即类型。现在，动手打开练习文件，让类型检查器成为你的学习伙伴吧！✨

【免费下载链接】haskell-exercises A little course to learn about some of the more obscure GHC extensions. 项目地址: https://gitcode.com/gh_mirrors/has/haskell-exercises