在Idris中对类型进行模式匹配

Question

也许这很基础，但我不明白为什么下面的函数对于fnc Nat和fnc Integer都回答1，即使后者甚至未包括在模式中。

fnc : Type -> Integer
fnc Bool = 1
fnc Nat = 2

- Attila Karoly

Answer 1

你不能对类型进行模式匹配，也不应该这样做。当我编译你的代码时，会收到下一个错误：

warning - Unreachable case: fnc Nat

这个问题之前已经讨论过：

1. 旧的讨论。
2. 一些类似的问题。
3. GitHub上的一些类似问题。

更新：

最终找到了一个更相关的问题和答案：

为什么typecase是不好的？

- Shersh

---

@Shersh，感谢您提供的最后一个链接！您能投票支持重新开放这个非常好的问题吗？我认为关闭它是一件遗憾的事情。 - Anton Trunov

@AntonTrunov 我也这么认为。投票支持重新开放。 - Shersh

Answer 2

实际上，您现在可以在Idris 2中执行此操作：

fnc : Type -> Integer
fnc Bool = 1
fnc Nat = 2
fnc _ = 3

- Matt R