Reduce coercion terms to normal form
|Reported by:||simonpj||Owned by:|
|Keywords:||Cc:||batterseapower@…, chak@…, tom.schrijvers@…|
|Type of failure:||Compile-time performance bug||Test Case:|
|Related Tickets:||Differential Rev(s):|
Sometimes coercion terms in a Core program grow absurdly big, and can readily be simplified to be much more compact. Example:
Big coercion terms have no runtime impact, but they may make compilation slower.
I speculate that it should be possible to use transformations such as those Max suggests in his comment on #2440, as a confluent, terminating rewriting system that makes coercion terms smaller, or, better still, rewrites them to a normal form. Then we can use "smart constructors" for coercion terms, so that they are always kept in normal form.
Identity coercions occur a lot, but are not so easy to recognise. I've also wondered about having some special representation for the identity.
This ticket is to remind us to look for such a rewrite system. Max, perhaps?
Change History (5)
comment:4 Changed 5 years ago by igloo
- Milestone changed from 6.12.3 to 6.14.1
- Priority changed from normal to low