Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Idris 2 implementation #522

Open
wants to merge 17 commits into
base: master
Choose a base branch
from
Open

Idris 2 implementation #522

wants to merge 17 commits into from

Conversation

mb64
Copy link

@mb64 mb64 commented Jul 3, 2020

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
Copy link
Owner

kanaka commented Apr 18, 2021

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

@kanaka
Copy link
Owner

kanaka commented Aug 7, 2024

@mb64 I know it's been a few years, but any interest in finishing this up and getting it merged.

If so, then in addition to updating to follow the structure I described above, could you also:

  • Rebase the code onto the current HEAD
  • The recommended process has changed slightly: the eval_ast is no longer seperate from eval and macroexpand is not longer a standalone function. It would be good if you could update to follow the new structure.
  • Make sure that the Github CI tests all pass for your implementation. By rebasing you will pick up improvements to the CI process that no longer require me to manually build/push a docker image.

If you aren't interested in pushing this forward, could you let me know so that I can close this ticket out? Also, if that's the case, then also let me know if you want me to add a link to the top-level README pointing to your implementation in the "Other Implementations" section (where I point to re-implementations of the same language or implementations that diverge from the normal structure/process significantly).

Thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants