Haskell类型级别平等

Question

Haskell有一个用于定义类型系列的resticted语法:

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

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

没有防护,没有case表达式,没有if-then-else语法,没有let和where,而且没有部分函数应用程序.这不是问题,因为缺少的case表达式可以被专门的类型级别函数替换,该模式匹配不同的情况,缺少的if-then-else语法可以被Data.Type的If 函数替换. 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)的计算结果为"真" .如果我们在值级别函数上执行相同的操作,GHC会回答Conflicting definitions for 'x'错误.在值级函数中,我们必须添加一个Eq a =>上下文来编译函数.

在Prolog的旧时代,类型级别模式匹配似乎与统一类似.我没有成功搜索有关类型级函数语法的一些文档.

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

Answer 1

Haskell的类型级语言是纯粹的一阶语言,其中"application"只是另一个构造函数,而不是计算的东西.有类似的绑定结构,forall但类型级别的东西的相等概念基本上只是alpha等价:结构直到绑定变量的重命名.实际上,我们整个构造函数级的机器,monad等依赖于能够m v明确地分开应用程序.

类型级函数并不像一等公民那样生活在类型级语言中:只有他们的完整应用程序才能这样做.我们最终得到了~类型级表达式的等式(对于平等概念)理论,其中约束被表达和解决,但这些表达式所表示的价值的基本概念总是一阶的,因此总是可以用等式表示.

因此,通过结构相等性测试来解释重复的模式变量总是有意义的,这正是模式匹配在其原始的1969年化身中的设计,作为根植于基本的一阶价值概念LISP的另一种语言的扩展.