How to use `deriving` in Idris?

Question

I'm trying to deriving Show, Eq, Ord etc in Idris, but none of the following trials works:

trail #1:

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)

trail #2:

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

trail #3:

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

I have searched the keyword deriving on http://docs.idris-lang.org/ and google, and even in the idris-dev repo under test/ directory, but there is no demo for the usage of deriving in idris. Anyone can help?

Myrilla

There is no deriving syntax. There is only elaborator reflection, which is like Template Haskell. – Masinissa

@Masinissa but the weird thing is when I'm trying to use the deriving syntax, it passed the syntax checking, so I think there must be something similar ? – Myrilla

It's parsed as data Expr = ... | Add (Expr) (Expr) (deriving) (Show), where deriving is just a (existential) type variable. You get an error because constructor field types must be Types, but Show isn't. If you remove the Show "field" you get a constructor Add : {deriving : Type} -> Expr -> Expr -> deriving -> Expr – Masinissa

@Masinissa Oh, that explains everything... I'm still wondering how to use elaborator reflection to do the same thing as deriving, is there any document? – Myrilla

There's the documentation on the mechanism itself, and there's this (bitrotten?) library that implements some classes. It seems you'll have to put in a bit of work for this. – Masinissa

@Masinissa So there is no corresponding handy feature in Idris yet? – Myrilla

Correct: there isn’t. – Masinissa

Answer 1

You can use Stefan Hoeck's idris2-sop library to generate implementations with elaborator reflection.

Maier