在 Idris 中列出 sum 类型的元素的惯用方式答案

【问题标题】：Idiomatic way of listing elements of a sum type in Idris在 Idris 中列出 sum 类型的元素的惯用方式
【发布时间】：2018-01-24 18:21:03
【问题描述】：

我有一个表示算术运算符的 sum 类型：

data Operator = Add | Substract | Multiply | Divide

我正在尝试为它编写一个解析器。为此，我需要一份所有运营商的详尽清单。

在 Haskell 中，我会使用 deriving (Enum, Bounded)，就像在以下 StackOverflow 问题中建议的那样：Getting a list of all possible data type values in Haskell

不幸的是，Idris 中似乎没有Issue #19 建议的这种机制。 David Christiansen 正在就这个问题进行一些工作，因此希望将来情况会有所改善：david-christiansen/derive-all-the-instances

来自 Scala，我习惯于手动列出元素，所以我很自然地想出了以下内容：

Operators : Vect 4 Operator
Operators = [Add, Substract, Multiply, Divide]

为了确保Operators 包含所有元素，我添加了以下证明：

total
opInOps : Elem op Operators
opInOps {op = Add} = Here
opInOps {op = Substract} = There Here
opInOps {op = Multiply} = There (There Here)
opInOps {op = Divide} = There (There (There Here))

因此，如果我将一个元素添加到 Operator 而不将其添加到 Operators，那么整体检查器会抱怨：

Parsers.opInOps is not total as there are missing cases

它可以完成工作，但它是很多样板。我错过了什么？有没有更好的方法？

【问题讨论】：

您可以手动为Operator实现Enum接口。
@AntonTrunov 谢谢，这就是我真正开始的地方，但我不太确定 fromNat 应该如何表现。
这取决于您的确切用例，但例如fromNat Z = Add fromNat (S Z) = Subtract fromNat (S (S Z)) = Multiply fromNat (S (S (S _))) = Divide 之类的东西可能对你有用。
非常感谢，使用 Enum 似乎更习惯用语，但我不得不放弃详尽无遗，这有点可惜
你仍然可以证明穷举，只要证明对于每个op，都有一个k : Nat，这样fromNat k = op

标签： dependent-type idris

【解决方案1】：

可以选择使用elaborator reflection这样的语言特性来获取所有构造函数的列表。

这是解决这个特殊问题的一种非常愚蠢的方法（我发布这个是因为目前的文档非常稀缺）：

%language ElabReflection

data Operator = Add | Subtract | Multiply | Divide

constrsOfOperator : Elab ()
constrsOfOperator = 
  do (MkDatatype _ _ _ constrs) <- lookupDatatypeExact `{Operator}
     loop $ map fst constrs

  where loop : List TTName -> Elab ()
        loop [] =
          do fill `([] : List Operator); solve
        loop (c :: cs) =
          do [x, xs] <- apply `(List.(::) : Operator -> List Operator -> List Operator) [False, False]
             solve
             focus x; fill (Var c); solve
             focus xs
             loop cs

allOperators : List Operator
allOperators = %runElab constrsOfOperator

几个cmets：

似乎要解决任何类似结构的归纳数据类型的问题，都需要通过Elaborator Reflection: Extending Idris in Idris 论文。
也许pruviloj 库有一些东西可以使解决这个问题更容易解决更一般的情况。

【讨论】：