coq - 为什么 Coq/Agda/Idris 中的 Set/Type 无法进行模式匹配？

Question

考虑一个接受 Set 并返回其字节长度的函数，名为 byteLength :

byteLength : Set -> Maybe Nat

如果我想直接实现这个函数，我需要对类型参数进行模式匹配:

byteLength Char = Just 1
byteLength Double = Just 8
byteLength _ = Nothing

但上面的代码无法编译，因为不允许在 Set/Type 上进行模式匹配。

所以我们必须定义一个接口(interface)作为解决方法

Interface ByteLength a where
    byteLength : Nat

implement ByteLength Char where
    byteLength = 1

并且以更一般的方式，也许我们可以使用 TypeRep 之类的东西来做类似的事情并在 TypeRep 上进行模式匹配。但是 TypeRep 也被定义为一个接口(interface)。

我认为使用 Interface 和使用 forall 是非常不同的，因为 Interface 意味着“对于某些类型”，而 forall 意味着“对于所有类型”。

我想知道为什么这些 DT 语言不支持 Set/Type 上的模式匹配，是否有一些我不知道的特殊原因？

Answer 1

在 Agda、Idris、Haskell 和许多其他语言中，对类型的量化是参数化的(与允许匹配类型的临时多态性相反)。从实现的角度来看，这意味着编译器可以从程序中删除所有类型，因为函数永远不会在计算上依赖于 Set 类型的参数。 .能够删除类型在依赖类型语言中尤其重要，因为类型通常会变成巨大的表达式。

从更理论的角度来看，参数多态性很好，因为它允许我们仅通过查看函数的类型来推断函数的某些属性， Eloquent 地描述为 "free theorems" by Phil Wadler .我可以试着给你这篇论文的要点，但你真的应该去阅读它。

当然，有时实现一个函数需要特定的多态性，这就是为什么 Haskell 和 Idris 有类型类(Agda 有一个类似的特性称为实例参数，而 Coq 有规范结构和类型类)。例如，在 Agda 中，您可以定义这样的记录:

record ByteLength (A : Set) : Set where
  field
    theByteLength : Nat
open ByteLength

byteLength : (A : Set) {{_ : ByteLength A}} -> Nat
byteLength A {{bl}} = bl .theByteLength

然后您可以通过定义实例来定义各种类型的 byteLength 函数:

instance
  byteLengthChar : ByteLength Char
  byteLengthChar .theByteLength = 1

  byteLengthDouble : ByteLength Double
  byteLengthDouble .theByteLength = 8

使用此代码， byteLength Char计算结果为 1和 byteLength Double计算结果为 8 , 而它会引发任何其他类型的类型错误。