I wanted to point you to two almost similar efforts [0] [1] then I found your post [2]. You may be interested also in [3].<p>[0] <a href="https://github.com/moonad/Formality" rel="nofollow">https://github.com/moonad/Formality</a><p>[1] <a href="http://imar.ro/~mbuliga/chemlambda-v2.html" rel="nofollow">http://imar.ro/~mbuliga/chemlambda-v2.html</a><p>[2] <a href="https://www.reddit.com/r/haskell/comments/dih8xu/optimal_reduction_without_oracle_prototype/" rel="nofollow">https://www.reddit.com/r/haskell/comments/dih8xu/optimal_red...</a><p>[3] <a href="https://mbuliga.github.io/kali24.html" rel="nofollow">https://mbuliga.github.io/kali24.html</a>
Did you demonstrate that your trick is sound and optimal? Optimal reduction is a tricky beast and you might need to use a very high order function to find a counterexample.