agda - 为什么 typecase 是一件坏事？

Question

阿格达和伊德里斯_有效地禁止对 type 值进行模式匹配Type。似乎 Agda 总是在第一种情况下匹配，而 Idris 只是抛出一个错误。

那么，为什么 typecase 是一件坏事呢？它会破坏一致性吗？我无法找到有关该主题的太多信息。

Answer 1

人们认为类型上的模式匹配很糟糕，这真的很奇怪。每当我们进行全域构造时，我们都会对编码类型的数据进行模式匹配。如果你采用我和 Thorsten Altenkirch 开创的方法（我和我的同志们开始设计），这些类型确实形成了一个封闭的宇宙，因此您甚至不需要解决（坦率地说值得解决）使用开放数据类型进行计算的问题来将类型视为数据。如果我们可以直接对类型进行模式匹配，我们就不需要解码函数来将类型代码映射到它们的含义，这在最坏的情况下减少了混乱，在最好的情况下减少了通过关于解码行为的等式定律证明和强制的需要功能。我完全打算以这种方式建立一个没有中间人的封闭类型理论。当然，您需要将 0 级类型包含在 1 级数据类型中。当你建立一个归纳递归的宇宙层次结构时，这自然会发生。

但是参数化呢，我听到你问了？

首先，当我尝试编写类型通用代码时，我不想要参数化。不要把参数强加给我。

其次，为什么类型应该是我们唯一参数化的东西？为什么我们有时不应该在其他东西中参数化，例如，完全普通的类型索引，它们存在于数据类型中，但我们不希望在运行时拥有它们？仅在规范中起作用的数量仅由于其类型而被迫存在，这真是令人讨厌。

域的类型与对它的量化是否应该是参数化的没有任何关系。

让我们（例如，由 Bernardy 和朋友们提出）一门学科，其中参数/可擦除和非参数/可匹配量化是不同的并且都是可用的。然后类型可以是数据，我们仍然可以说出我们的意思。

Answer 2

许多人认为类型匹配很糟糕，因为它破坏了类型的参数化。

在具有类型参数化的语言中，当您看到一个变量时

f : forall a . a -> a

您立即知道很多关于f. 直观地说：既然f是函数，可以写成：

f x = body

body 需要是 type 的a，但a它是未知的，所以 type 的唯一可用值a是x。如果语言允许不终止，f也可以循环。但是它可以x根据 的值在循环或返回之间做出选择x吗？不，因为a未知，f不知道要调用哪些函数才能x做出决定。所以实际上只有两个选择：f x = x和f x = f x. 这是一个关于 的行为的强大定理f，我们仅通过查看 的类型就可以得到f。类似的推理适用于具有普遍量化类型变量的所有类型。

现在如果f可以匹配 type a，更多的实现f是可能的。所以我们会失去强大的定理。

Answer 3

在 Agda 中，您不能进行模式匹配，Set因为它不是归纳类型。