Haskell 类型级别相等性

Question

Haskell的语法对于定义类型族有限制:

(1)   type family Length (xs :: [*]) where
(2)     Length '[] = 0
(3)     Length (x ': xs) = 1 + Length xs

在等号（=）左侧的第（2）和第（3）行，我们只有简单的模式匹配。在等号右侧，我们只有类型级函数应用，而作为一种语法糖， 有类型运算符（（+）在第（3）行）。

没有保护程序，没有情况表达式，没有if-then-else语法，没有let和where，并且没有部分函数应用。 这不是问题，因为缺少的情况表达式可以由专门的类型级函数替换，该函数在不同情况下进行模式匹配， 缺失的if-then-else语法可以由Data.Type.Bool包的If函数替换。

从一些示例中我们可以看到，类型级别的模式匹配语法至少具有一个普通Haskell值级函数中不可用的附加功能：

(1)   type family Contains (lst :: [a]) (elem :: a) where
(2)     Contains (x ': xs) (x) = 'True
(3)     Contains '[]       (x) = 'False
(4)     Contains (x ': xs) (y) = Contains xs (y)

在第二行中，我们使用变量x的两倍。 第二行的求值结果为'True'，如果第一个参数的列表的头与第二个参数相等。 如果我们在一个值级别的函数上做同样的事情，GHC会返回一个Conflicting definitions for 'x' 错误。 在值级别的函数中，我们必须添加一个Eq a => 上下文才能编译该函数。

类型级别的模式匹配似乎与早期的Prolog中的unification类似工作。 我尝试谷歌一些关于类型级别函数语法的文档，但没有成功。

• 为什么GHC在Contains类型族的定义中不需要类似a ~ b的类型相等约束？
• 类型相等是否总是可用的？
• 类型族语法是否具有其他在值级别不可用的附加功能？
• 这在哪里记录？

- Jogger

---

确实经常有人说Haskell的类型级语言基本上是一种逻辑语言。 - leftaroundabout

@leftaroundabout 在这个问题上有点有趣 :) - Benjamin Hodgson

@BenjaminHodgson，这只使用（关系）系统的功能特性，以配合“Haskell”（如他们所定义的）是一种函数式语言的说法。 - dfeuer

Answer 1

Haskell的类型级语言是一种纯一阶语言，在其中，“应用”只是另一个构造器，而不是计算的东西。有绑定构造，如forall，但类型级别的等价性的概念从根本上来说只是α-等价：结构上重命名绑定变量。事实上，我们整个构造器类机制、单子等都依赖于能够无歧义地分解应用m v。

类型级别的函数并不真正作为一等公民存在于类型级别语言中：只有它们的完全应用才是。我们最终得到的是类型级别表达式的等式（对于~等价性的概念），在其中表达和解决限制条件，但这些表达式所表示的基础值始终是一阶的，因此始终可以用等式来描述。

因此，通过结构等价测试来解释重复的模式变量总是有意义的，这正是模式匹配最初的1969年版本的设计方式，作为根植于基本一阶值概念LISP的另一种语言的扩展。

- pigworker