Automatic class instance for has_string or has_repr

Stream: general

[Jason Rute]

Is there a way to automatically generate the instances has_string or has_repr for inductive and structure types (assuming the types they use for the arguments also have has_string and has_repr)? I know Rust for example has an autogenerated debug type class thing that lets you make a representation for standard classes (forgetting the proper Rust terminology). Does Lean have something similar?

[Jason Rute]

Rust: https://doc.rust-lang.org/std/fmt/trait.Debug.html
Python: Can do it with the@dataclass(repr=True) decorator: https://docs.python.org/3/library/dataclasses.html
Lean: ???

[Bhavik Mehta]

Haskell can do this by deriving Show, maybe we could adapt the method that uses

[Jason Rute]

Lean has derive handlers, but I don't know how to find one for:
@[derive [has_repr]]

[Jason Rute]

I realize I don't even know where @[derive [monad]] comes from. I tried searching in both lean and mathlib and I came up short. Is there a list of all the current derive handlers (and how to import them)?

[Bryan Gin-ge Chen]

I'm not really sure how they work, but it looks like "derive handlers" are set up in core. Searching for the derive_handler attribute might help.

It would be good to add some docs on this.

[Reid Barton]

I don't think there is any structural way to derive monad--I think we have a default handler that just copies the instance from the right-hand-side of the definition

[Jason Rute]

Ok, so one doesn't need a derive handler if the right-hand-side already has the desired instance? That explains monad. I think we have very few right now. Maybe one day I'll get around to writing one for has_repr. (I might cheat first and make one in python that just spits out the instance code I want.)

[Mario Carneiro]

No, you do need a derive handler, but there is a blanket derive handler for proof by unfolding

[Mario Carneiro]

Examples of "real" derive handlers include inhabited, decidable_eq and has_reflect

[Jason Rute]

@Mario Carneiro Are to saying there is a way to get has_repr (or similar functionality) without a derive handler? If so, how?

[Mario Carneiro]

I'm saying you have to write your own derive handler, which is just a tactic that does this construction

[Mario Carneiro]

you can register your own derive handlers

[Jason Rute]

Sorry, I read the “No, you do” as “No you do not”. :facepalm: