6

我正在尝试在 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 中派生的使用演示。任何人都可以帮忙吗？

4

1 回答 1

1

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

于 2022-02-07T23:44:41.363 回答