HigherOrderCO / Kind

A modern proof language
https://higherorderco.com
MIT License
3.55k stars 141 forks source link

Improve compilation of cases to Javascript #68

Closed Eloitor closed 4 years ago

Eloitor commented 4 years ago

This has a recursive call inside each case

toBrainFuck(p : List(Instruction)) : String case p | nil => nil() | cons => case p.head as ins | right => cons( '>', toBrainFuck(p.tail)) | left => cons( '<', toBrainFuck(p.tail)) | inc => cons( '+', toBrainFuck(p.tail)) | dec => cons( '-', toBrainFuck(p.tail)) | write => cons( '.', toBrainFuck(p.tail)) | read => cons( ',', toBrainFuck(p.tail)) | loop => concat( concat( cons( '[' , toBrainFuck(ins.code)), "]"), toBrainFuck(p.tail))

So, when compiled to JS, every case would recurse, being accidentally exponential.

A temporary solution: insert + toBrainFuck : List(Instruction) -> String inside toBrainFuck, below the second case. This will pass the recursive calls linearly to each branches, preventing this problem from happening. it is also a very good practice in general, interaction nets like that style.

On the long term, we can make the JS compiler lazy by wrapping every value inside a ()=>... closure

VictorTaelin commented 4 years ago

To elaborate, the current JS back-end evaluates all branches of a case expression, because those are compiled to raw function applications (val(case_a, case_b, case_c, ...)), which aren't evaluated lazily in JavaScript. This can be avoided by manually inserting + func : T below the case, as suggested on the documentation. A more long-term solution would be to make the JS compiler lazy, or to make -r default to the upcoming Haskell compiler, which is lazy.

VictorTaelin commented 4 years ago

Formality was reworked entirely and the compiler is much smarter, but it still lacks laziness on cases. Must be added.

VictorTaelin commented 4 years ago

Fixed on https://github.com/moonad/Formality/commit/e314755ff7d7b39a1ec0fb76eeb9cdf2dc8cac20!