为什么在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也被定义为一个接口。

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

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

- luochen1990

---

相关问题 - Anton Trunov

Answer 1

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

从更理论的角度来看，参数多态很好，因为它使我们能够通过查看函数的类型来推断出某些属性，菲尔·沃德勒（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，对于其他任何类型都会引发类型错误。

- Jesper