在Idris中列出和类型元素的惯用法

Question

我有一个表示算术运算符的和类型:

data Operator = Add | Substract | Multiply | Divide

我正在尝试为它编写解析器.为此,我需要一份详尽的所有运营商名单.

在Haskell中,我将使用deriving (Enum, Bounded)以下StackOverflow问题中的建议:获取Haskell中所有可能的数据类型值的列表

不幸的是,问题#19所建议的伊德里斯似乎没有这样的机制.大卫·克里斯蒂安森正在就这个问题进行一些正在进行的工作,所以希望将来情况会有所改善: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

它做的工作,但它是很多样板.我错过了什么？有没有更好的方法呢？

Answer 1

可以选择使用该语言的特性（例如详细反射）来获取所有构造函数的列表。

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

%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

一些评论：

1. 似乎要解决类似结构的任何归纳数据类型的这个问题，需要完成Idris 论文中的 Elaborator Reflection: Extending Idris。
2. 也许pruviloj库有一些东西可以使解决更一般情况下的这个问题变得更容易。