idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.48k stars 372 forks source link

Document `%transform` #2023

Open andrevidela opened 2 years ago

andrevidela commented 2 years ago

%transform has been a successful part of the compiler for some time now and I couldn't find any good reference for how it is supposed to work and what it is supposed to do. The only page I could find that mentions it is https://idris2.readthedocs.io/en/latest/reference/builtins.html?highlight=transform#builtin-integertonatural

Shouldn't there be a more descriptive tutorial about %transform?

gallais commented 2 years ago

Note that %transform is not mature enough to express e.g. fusion rules. So whatever doc we write now will have to be rewritten once it's fixed.

andrevidela commented 2 years ago

One could argue that the fusion rules should be replaced by linearity optimisations :)

gallais commented 2 years ago

I'm not sure I understand what you're saying. Fusion turns two (or more) traversals into a single one. It's not just about allocation.

andrevidela commented 2 years ago

I haven't looked into this recently but I was under the impression that Fusion could be replaced by deforestation allowing you to ensure the traversals are properly inlined and merged. The problem with fusion being that its heuristics don't always predictably trigger, but relying on linear use makes a non-optimised tree traversal a type error