伊德里斯的不可能模式(Impossible patterns in Idris)

伊德里斯的不可能模式(Impossible patterns in Idris)

我正在学习伊德里斯，我陷入了一个非常简单的引理，它表明数据类型不可能有某些特定的索引。 我试图使用不可能的模式，但Idris拒绝它们，并出现以下错误消息：

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

完整的代码段可在以下要点中找到：

https://gist.github.com/rodrigogribeiro/f27f1f035e5a98f506ee

任何帮助表示赞赏。

I'm learning Idris and I got stuck on a very simple lemma that shows that some specific index is impossible for a data type. I've tried to use impossible patterns but Idris refuses them with the following error message:

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

The complete code piece is available in the following gist:

https://gist.github.com/rodrigogribeiro/f27f1f035e5a98f506ee

Any help is appreciated.

最满意答案

我和freenode Idris社区的人交谈，他们向我解释说荒谬的模式需要一个明确的不可能的案例，以便发现这是不可能的。 举个例子：

hasEmptyZero : HasEmpty Zero -> Void hasEmptyZero HasEps impossible

这里放置构造函数HasEps可以帮助Idris检测它不能用于构造HasEmpty Zero类型的值。 完整的（工作）代码在以下要点：

https://gist.github.com/rodrigogribeiro/5b39048df1d9ddc083ec

I've talk with people at freenode Idris community and they explained to me that absurd pattern needs a explicit impossible case in order to detect that is really impossible. As an example:

hasEmptyZero : HasEmpty Zero -> Void hasEmptyZero HasEps impossible

Here putting the constructor HasEps helps Idris to detect that it cannot be used to construct a value of type HasEmpty Zero. The complete (working) code is at the following gist:

https://gist.github.com/rodrigogribeiro/5b39048df1d9ddc083ec