为什么 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 ByteLength a where
    byteLength : Nat

implement ByteLength Char where
    byteLength = 1

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

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

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

Answer 1

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

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

当然，有时候实现一个函数需要特殊的多态性，这就是为什么 Haskell 和 Idris 有 类型类 （Agda 有一个类似的功能称为 instance arguments ，并且 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，但它会引发任何其他类型的类型错误。