Idris 2 implementation

[mb64]

In this implementation, I took the liberty of not following the guide to the letter. For example, there's no special-forms switch statement, or TCO loop, or functions with underscores. Instead, all special forms are implemented directly as built-in functions, and TCO is provided courtesy of Idris's scheme backend.

Idiomatic Idris tends to look like Haskell, but with extra type-level magic. This is no exception, although it doesn't really make that much use of Idris's dependent types.

(One bit of type-level magic in this code is in the MalFunction and MalType typeclasses, which will turn an Idris function into a Mal builtin. This doesn't use any Idris-specific features, though: it's the same trick as Haskell's Text.Printf. Another bit of type-level magic is that the parser, by virtue of using the builtin parser combinators, is proven to always make forward progress.)

In terms of completeness, it has everything but metadata. In addition, there's another soft-failing test in the bootstrapped Mal that probably shouldn't be failing. Its failure seems to indicate the presence of a subtle bug somewhere in some builtin where a map is evaluated once more than it should be. I haven't been able to find it yet.

I did my best to include a Dockerfile, but I don't use Docker, so I'd appreciate input on it. Note that since Idris 2 is still in its early stages, there's no binary install available for it, so the Dockerfile has to install it from source.

[kanaka]

Hi @mb64. Apologies for the very slow response to reviewing PR. It's not personal, I just haven't been doing any mal/open source activity for the past year or so. I am interested in merging this implementation if you are willing to make some structural changes to fit with the pedagogical goal of mal. The idiomatic Idris adaptions that you made to the guide are fine (the guide is somewhat dynamic/OOP language focused admittedly). The main issue that will need to be addressed before merging is that the code more directly related to the eval process needs to be structured into code steps that correspond to each of the incremental steps. This enables future learners to be able to compare between steps and also compare steps between implementation languages. Currently you have most of the incremental eval code in files that are common between steps (Eval, Core, and Class).

It does feel a little weird to be duplicating common code, and for your own learning process it's perfectly fine. But for the overall mal project goal it's important that included implementations have comparable steps and incremental process displayed clearly for future reference/learning. See the FAQ for more details: https://github.com/kanaka/mal/blob/master/docs/FAQ.md#will-you-add-my-new-implementation I know it's been months since you did this, but if you are willing to make those changes I would be happy to merge it. If you don't want to make the change or don't otherwise have time to make the changes (I certainly understand life changes that may get in the way), I'm happy to link to your repo/implementation in the README in lieu of merging into the main tree.

I also run into an error building the docker image. It's likely that it is due to the amount of time that has passed since you wrote the Dockerfile and versions are no longer in sync.

Step 14/15 : RUN chmod -R a+x /idris2/idris2-0.2.0
 ---> Running in 010e18f67720
chmod: cannot access '/idris2/idris2-0.2.0': No such file or directory
The command '/bin/sh -c chmod -R a+x /idris2/idris2-0.2.0' returned a non-zero code: 1