为什么我们不能在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多态相反).从实现的角度来看,这意味着编译器可以从程序中擦除所有类型,因为函数永远不会在计算上依赖于类型的参数Set.能够擦除类型在依赖类型语言中尤其重要,因为类型通常可以成为巨大的表达.

从更理论的角度来看,参数多态是很好的,因为它允许我们通过查看它的类型来推断函数的某些属性,由Phil Wadler雄辩地描述为"自由定理".我可以尝试给你这篇论文的要点,但你应该去看看它.

当然,有时需要ad-hoc多态来实现一个函数,这就是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,同时它将引发任何其他类型的类型错误.