如何在Idris中使用“派生”？

Question

我试图在Idris中导出Show、Eq、Ord等，但下列任何一种测试都不起作用：

第一条线索：

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

got：

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)

第二条线索：

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

got：

*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

第三条线索：

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

got：

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

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

Answer 1

您可以使用斯特凡·霍克( Stefan Hoeck) idris2-sop库生成带有精心设计反射的实现。