Haskell 类型级别相等

Question

Haskell 有一个受限制的语法来定义类型族:

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

在等号 (=) 左侧的 (2) 和 (3) 行，我们只有简单的模式匹配。
在等号的右侧，我们只有类型级函数应用程序和语法糖
有类型运算符(第 (3) 行中的 (+))。

没有 guard ，没有 case 表达式，没有 if-then-else 语法，没有 let 和 where's
并且没有偏函数应用。
这不是问题，因为缺少的 case 表达式可以用专门的类型级别函数替换，
该模式在不同的情况下匹配，缺少的 if-then-else 语法可以替换为 If
Data.Type.Bool 的功能
包裹。

看看我们看到的一些例子，类型级别的模式匹配语法至少有一个
附加功能，在正常的 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)

在第 (2) 行中，我们使用了两倍的变量 x。第 (2) 行的计算结果为 'True，如果第一个参数的列表的头部
等于第二个参数。
如果我们在值(value)级别函数上做同样的事情，GHC 会回答 Conflicting definitions for 'x'错误。
在值级函数中，我们必须添加 Eq a =>编译函数的上下文。

类型级别的模式匹配似乎与 Prolog 旧时代的统一类似。
我在谷歌上搜索了一些关于类型级函数语法的文档，但没有成功。

为什么 GHC 在 Contains 类型族的定义中不需要 a ~ b 类型等式约束？

类型相等总是可用的吗？

类型族语法是否有其他附加功能，在值级别上不可用？

这是在哪里记录的？

Answer 1

Haskell 的类型级语言是一种纯粹的一阶语言，其中“应用程序”只是另一个构造函数，而不是计算的东西。有绑定(bind)结构，如 forall ，但是类型级别的东西的平等概念基本上只是 alpha 等价:结构上直到重命名绑定(bind)变量。事实上，我们的整个构造器类机制、monad 等都依赖于能够接受应用程序 m v毫不含糊地分开。

类型级函数并不像一等公民那样真正存在于类型级语言中:只有它们的完整应用程序才如此。我们最终得到了类型级别表达式的等式(对于 ~ 的相等概念)理论，其中约束被表达和解决，但这些表达式表示的基本值(value)概念始终是一阶的，因此始终是可配的与平等。

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