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

Eliminate indexing errors in compiler #438

Open
joelberkeley opened this issue Dec 15, 2024 · 1 comment
Open

Eliminate indexing errors in compiler #438

joelberkeley opened this issue Dec 15, 2024 · 1 comment
Labels
feature:internal Feature that helps develop framework internals perf:runtime

Comments

@joelberkeley
Copy link
Owner

We use List and Nat for stack and pointer, respectively. This means we have to handle indexing errors, which risk failing at runtime, and require either use of idris_crash/die, or (slow?) EitherT monad. If instead we use Vect n and Fin n, we can remove this problem at compile time. This would probably require changing the way we handle nested functions, but that might be a good thing on its own.

@joelberkeley joelberkeley added perf:runtime feature:internal Feature that helps develop framework internals labels Dec 15, 2024
@joelberkeley
Copy link
Owner Author

This might be impossible as we don't want to expose this indexing in the user API

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
feature:internal Feature that helps develop framework internals perf:runtime
Projects
None yet
Development

No branches or pull requests

1 participant