notes

Whitespace back-end for Idris

Whitespace could become a code generation back-end of the Idris 2 compiler.

This is something that Edwin Brady, the creator of both languages, has considered building:

By the way, at one point I implemented a Whitespace interpreter in Idris, just to see how far Idris had come along. Whitespace is unfortunately a bit too limited to work as an Idris back end (at least, not without a lot of effort), but sometimes I wonder what extensions it would need to make it work, just to complete the loop, as it were.

This interpreter, WS-idr, is even listed in the list of 3rd-party code generation targets for Idris 1, reflecting this early intent.

The Idris 2 documentation describes how to build a custom back-end, that uses Idris as a library. Edwin also wrote a paper on the IRs generated by Idris and its FFI, with an example PHP back-end.

The main language gaps that would need to be filled for Whitespace would be closures, algebraic data types, and garbage collection. I am unsure for the dependently-typed parts. Concurrency would not be able to be implemented efficiently and parallelism is not possible.

Debug information with Idris source locations could be encoded as comments in the generated Whitespace program, where whitespace characters are escaped.

Since the higher-level constructs for Whitespace are not specific to Idris, the compiler should expose a higher-level language, that the Idris back-end can generate code for. This also helps minimize the Idris code I’d need to write, because I’m not an expert with Idris (though may become one, if I build this).

If the back-end became mature enough to compile the Idris compiler, it enables a loop. Idris could compile itself with the Whitespace back-end, then that could compile WS-idr, which could interpret the Idris compiler.