如何让 Idris 警告不完整的案例/匹配？答案

【问题标题】：How to make Idris warn of incomplete cases/matches?如何让 Idris 警告不完整的案例/匹配？
【发布时间】：2019-11-28 17:34:52
【问题描述】：

例如，当为以下类型实现Show 实例时：

data Shape = Circle Double
           | Box Vector2D
           | Polygon (List Vector2D)
           | Chain (List Vector2D)

...省略Chain 的情况，Idris 将成功键入检查此文件。

实现其他功能也存在类似问题。

在文件开头添加%default total 似乎没有帮助，但我的印象是应该这样做。

【问题讨论】：

标签： idris

【解决方案1】：

有了这个：

%default total

data DataType = A | B | C

Show DataType where
  show A = "A"

我明白了

$ idris Testme.idr
Type checking ./Testme.idr
Testme.idr:5:1-13:
  |
5 | Show DataType where
  | ~~~~~~~~~~~~~
Main.DataType implementation of Prelude.Show.Show is possibly not total due to: Prelude.Show.Main.DataType implementation of Prelude.Show.Show, method show

请注意，您不会在 Atom 中看到此类警告 - 它们似乎不是编译器/编辑器协议的一部分。

【讨论】：

啊是的，这就是问题所在：我原以为 Atom 会报告该消息

【解决方案2】：

您可以通过以下方式致电idris：

--total 要求函数默认为总计

我仍然不确定这是否是唯一的方法，为什么%default total 似乎什么都不做，以及是否有可能只在函数不完整时收到警告。

【讨论】：