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

Determine how to make bound-style alpha substitution work with hash consing #3

Open
kozross opened this issue Dec 17, 2024 · 2 comments
Assignees
Labels
milestone-1 Library for Covenant question Further information is requested

Comments

@kozross
Copy link
Member

kozross commented Dec 17, 2024

bound provides a really good method to simplify alpha substitution and perform it efficiently. While we may not use bound itself, its approach should 100% be part of how Covenant is represented in Haskell. However, a disadvantage of bound is that it forces a tree-like structure on anything it's used with.

This can be quite inefficient for sharing, which bloats representation size and potentially makes it more difficult for tooling to work. In particular, it inhibits hash consing, which we ideally would like to be possible.

We need to investigate how the bound approach (even in a simplified form) could be combined with hash consing, or if it's not possible, what exactly blocks it.

@kozross kozross added question Further information is requested milestone-1 Library for Covenant labels Dec 17, 2024
@itsfarseen
Copy link
Collaborator

@kozross My plan is to:

  • Define a simple lambda calculus interpreter
  • Implement hash consing.
  • Investigate how to implement alpha substitution by referring to bound and other general ways to do it.

Does this sound good?

@kozross
Copy link
Member Author

kozross commented Dec 19, 2024

@itsfarseen - seems good to me. Let us know what you find.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
milestone-1 Library for Covenant question Further information is requested
Projects
None yet
Development

No branches or pull requests

2 participants