Idris中的不可能模式

Question

4

我正在学习Idris，遇到了一个非常简单的引理，它显示某个特定索引对于数据类型是不可能的。我试图使用不可能的模式，但是Idris拒绝了它们，并显示以下错误信息：

RegExp.idr line 32 col 13:
hasEmptyZero prf is a valid case

完整的代码片段可在以下gist中找到：

任何帮助都会受到赞赏。

- Rodrigo Ribeiro

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Rodrigo Ribeiro · Accepted Answer

我与freenode Idris社区的人交谈过，他们向我解释说，荒谬模式需要一个明确的不可能情况来检测其是否真正不可能。以下是一个例子：

hasEmptyZero : HasEmpty Zero -> Void
hasEmptyZero HasEps impossible

在这里放置构造函数 HasEps 有助于Idris检测到它不能用来构造类型为 HasEmpty Zero 的值。完整（可工作）的代码在以下的gist链接中：