deriving instances about idris-dev HOT 5 CLOSED

@corazza The answer is "elaborator reflection", which gives the tools for writing deriver scripts for various interfaces, as well as other forms of metaprogramming/program automation.

from idris-dev.

@edwinb Can you expand a bit on what @david-christiansen has been doing, I'm interested in what "to make instance creation much easier, and more general than deriving." means, thank you

from idris-dev.

Is elaborator reflection really a suitable alternative to deriving? It doesn't seem easier at all...

from idris-dev.

The reason why this issue has been left open for so long is that 'deriving' involving Dependent Types is not so straightforward in comparison to non-dependent types. If deriving were to be supported then it should be available for both kinds of types, and no special cases should be added. It is all or nothing.

from idris-dev.

I'm going to close this because it's a bit open ended, and it's not even obvious that deriving is exactly what we want. There is work going on by @david-christiansen to make instance creation much easier, and more general than deriving.

from idris-dev.