内容很大部分来自 https://haskell.love/richard-eisenberg/ 这一视频，奇怪的知识增加了。

引入

1
2
const :: a -> b -> a
const x y = x

const 函数接收几个参数呢？是 a 类型的 x 与 b 类型的 y —— 两个吗？

为了便捷，GHC 默认会省略掉 rank 1 的 quantifier。我们可以打开语言扩展
ExplicitForAll 并在 GHCi中开启参数 -fprint-explicit-foralls，以便在代码中可以显式书写量词，以及使得在 GHCi 使用 :t 时会同时打印出量词。当然，有了 UnicodeSyntax 语言扩展，∀ 也能被 parse。所以我们可以改写一下新的 const：

1
2
const :: ∀ a b . a -> b -> a
const x y = x

这样就清晰多了 —— const 接收四个参数：类型变量 a 和 b，以及 x 和 y。有的同志（用过 exteff 相关库）可能知道一个叫 TypeApplications 的扩展，开启它之后类型变量也能显式指定，例如 const @Int @String 233 "QAQ"。这样以来我们可以更加确信 const 有四个参数。

再来看一个相似的例子：

1
2
shout :: ∀ a . Show a => a -> String
shout x = map toUpper (show x) ++ "!"

shout 接收三个参数：类型变量 a、类型类实例 Show a 以及 x。类型类实例有点像隐式转换，编译器会在上下文中去找这个东西，使得函数体中能够正确调用类型类约定的函数。值得注意的是和类型变量不同，类型类实例只能靠编译器推断，不能手动传进去。

三类形参

下面介绍三种形参具有的特性：dependent、relevant、visible。

  • dependent —— 这个参数是依赖的，即这个参数值的选择会影响后续参数的类型。
  • relevant —— 这个参数是相关的，即这个参数值能在运行期函数体中使用。
  • visible —— 这个参数是可见的，即这个参数能显式传入。

这样我们可以画出一张表：

类型变量 类型类实例 常规项
dependent 是 否 否
relevant 否 是 是
visible 否 否 是

通过上面 const 与 shout 的例子，我们得知了：

  • 常规项，例如 Int -> ... 是 relevant（参数就要在函数体用嘛）、visible*（当然要显式传，不然怎么知道是几）并且 *non-dependent 的（你 Haskell 并没有原生依赖类型）。

  • 类型类实例，例如 Show a => ... 是 relevant（函数体调用到了类型类实例中的代码）、invisible （只能靠编译器找）并且 non-dependent 的。

  • 类型变量，例如 ∀ (a :: Type). ... 是 irrelevant、invisible 并且 non-dependent 的。

事实上，这三类特性还有其他的组合方式，我们暂且画出一张更全的表：

relevant visible dependent 表示方法
是 是 是 ?????
是 是 否 通常项 Int -> ...
是 否 是 ?????
是 否 否 类型类实例 Show a => ...
否 是 是 ?????
否 是 否 要你有何用！
否 否 是 类型参数 ∀ (a :: Type). ...
否 否 否 要你有何用！

不要急，咱一点点来，先从 relevant 看起。

relevant

看看以下 id 函数：

1
2
3
4
-- 这段代码不能成功编译
id :: ∀ a . a -> a
id True = False
id x    = x

我们尝试定义出一个奇怪的 id 函数，对于 Bool 类型的 True 会返回 False；而对于其他类型则原封不动地返回。好像没啥问题的说，但这段代码并不能被 GHC 编译。id 应适用于所有类型 a，但我们在第一个模式中把 a 特化成了 Bool，这是不合法的。由此可以得出 Haskell 中的类型变量是 irrelevant 的（至少在编译期）。但是！咱还有所谓的反射（Data.Typeable / Type.Reflection）：

1
2
3
4
5
6
7
weirdID :: ∀ a . Typeable a => a -> a
weirdID
  | Just HRefl <- typeRep @a `eqTypeRep` typeRep @Bool
  = \case True -> False
          x    -> x
  | otherwise
  = \x -> x

Pattern guard 语法之前没见过呢。 不难看出，这里在运行期比较了 a 和 Bool 是否相等，根据比较结果来决定函数行为。Typeable constraint 给了类型 Propositional equality 的能力。weirdID 中的 a 已经算是 dependent & relevant 了，虽然有些丑陋。至于说这个组合有什么用，别问，问就是模拟依赖类型。当然，还可以像 weirdID2 这样显式传入 TypeRep 来代替 Typeable 约束，它们没啥本质上的区别：

1
2
3
4
5
6
7
weirdID2 :: ∀ a . TypeRep a -> a -> a
weirdID2 req
  | Just HRefl <- rep `eqTypeRep` typeRep @Bool
  = \case True -> False
          x    -> x
  | otherwise
  = \x -> x

visible

weirdID / weirdID2 中的 a 已经做到了 dependent & relevant*，那么 *visible 呢？很遗憾，universal quantification ∀ a 依然是不可见的，而我们真正想要的是 VDQ（visible dependent quantification），就像 weirdID3 这样：

1
2
3
4
5
6
7
8
-- 这段代码不能成功编译
weirdID3 :: ∀ a -> Typeable a => a -> a
weirdID3 a
  | Just HRefl <- typeRep a `eqTypeRep` typeRep @Bool
  = \case True -> False
          x    -> x
  | otherwise
  = \x -> x

这里的 ∀ a. 变成了 ∀ a ->，意味着 ∀ a 从一个 Scheme（在 universal quantifier 约束下的 polymorphic type variable）变成了一个 dependent term。

只不过 —— 编译这段代码，你会得到 Illegal visible, dependent quantification in the type of a term: forall a -> Typeable a => a -> a (GHC does not yet support this)（这波啊，这波是 GHC 布星

既然 Term 层不行，咱来 Kind 层实现：

1
2
3
4
type WeirdId3 :: ∀ a -> a -> a -- 需要打开 StandaloneKindSignatures
type family WeirdId3 a x where
  WeirdId3 Bool True = False
  WeirdId3 _    x    = x

唔姆，类型家族很好理解，就是定义一个操作类型的函数。在 GHCi 中运行 :k WeirdId3 Bool True 可以得到 'False。注意这个 ' —— 咱运算得出的结果是一个类型，'False 的 kind 是 Bool。类似，运行 WeirdId3 Symbol "hello" 可以得到 "hello"，当然这个 "hello" 不是 String 的实例，而是 kind 为 Symbol 的一个类型。所有在 Kind Level 进行 quantification 的类型变量都是 relevant 的，这是 GHC 钦定的。换句话说，咱写不出来类型家族 WeirdId3 :: ∀ a. a -> a，而且调用 WeirdId _ x 时 _ 必须写上 x 的类型。

好像完事了，来把表填上：

relevant visible dependent 表示方法
是 是 是 Typeable VDQ： ∀ a -> Typeable a => ...（GHC 现在不支持）
类型层 VDQ：∀ a -> ...
是 是 否 通常项： Int -> ...
类型层：ℕ -> ...
是 否 是 有 Typeable 约束的类型参数 ∀ a . Typeable a =>（恶星）
类型层：∀ a . ...
是 否 否 类型类实例 Show a => ...
否 是 是 VDQ：∀ a -> ...（GHC 现在不支持 因为已经钦定了）
否 是 否 要你有何用！
否 否 是 类型参数 ∀ (a :: Type). ...
否 否 否 要你有何用！

看到这儿相信大家应该能理解 ∀ a. ... 和 ∀ a -> ... 的区别吧……

题外话

看这个 Vec（Indexed datatype）：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
data ℕ = Z | S ℕ

data Vec n a where
  Nil :: Vec Z a
  (∶) :: a -> Vec n a -> Vec (S n) a

vReplicate :: ∀ (n :: ℕ) a . Typeable n => a -> Vec n a
vReplicate x
  | Just HRefl <- typeRep @n `eqTypeRep`typeRep @Z
  = Nil
  | App succ m <- typeRep @n
  , Just HRef; <- succ `eqTypeRep` typeRep @S
  = x ∶ withTypeable n (vReplicate x)
  | otherwise
  = error "impossible"

对于 vReplicate 而言，长度 n（类型变量）既是 relevant 的又是 dependent 的，因为这个函数要根据 n 来确定生成多长的 Vec，同时 Vec 的类型也依赖它的长度。事实上现在咱们还没法使用 ℕ 进行运算。首先，它是个 Type，咱们需要 type family 来定义操作 ℕ。其次，有了 type family 后它也只能出现在类型签名里或者像 vReplicate 这样通过 Typeable 强行让 n 变得 relevant，不能直接在模式匹配中使用。强制 Typeable 是很恶星的，把事情都搞到了 runtime，还弱化了类型系统的表达能力。关于更好地在 Haskell 中使用这种索引数据类型，可以康康 singleton，顺便做一下 Codewars 上那道题（

Further Reading