如何在 Idris 中使用“deriving”？

Question

我试图在 Idris 中导出 Show、Eq、Ord 等，但以下试验均无效：

踪迹#1：

data Expr =
      Lit Int
    | Neg Expr
    | Add Expr Expr
    deriving (Show)

得到：

deriving.idr:5:15-18:
  |
5 |     deriving (Show)
  |               ~~~~
When checking type of Main.Add:
Type mismatch between
        Type -> Type (Type of Show)
and
        Type (Expected type)

踪迹#2：

data Expr =
      Lit Int
    | Neg Expr
    | Add Expr Expr
    deriving (Show _)

得到：

*deriving> Lit 1
Lit 1 : Expr
*deriving> Add (Lit 1) (Lit 1)
(input):Can't infer argument ty to Add, Can't infer argument deriving to Add

踪迹＃3：

data Expr =
      Lit Int
    | Neg Expr
    | Add Expr Expr
    deriving (Show Expr)

得到：

*deriving> Lit 1
Lit 1 : Expr
*deriving> Add (Lit 1) (Lit 1)
(input):Can't infer argument deriving to Add

deriving我在http://docs.idris-lang.org/和google上搜索过这个关键字，甚至在test/目录下的idris-dev repo中也搜索过这个关键字，但是没有关于idris中派生的使用演示。有人可以帮忙吗？

Answer 1

您可以使用Stefan Hoeck 的 idris2-sop库来生成具有详细反射的实现。