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.

Sign up for GitHub

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

Jump to bottom

Lazy evaluation #471

Open
Kmeakin opened this issue Jan 20, 2023 · 6 comments · May be fixed by #476
Open

Lazy evaluation #471

Kmeakin opened this issue Jan 20, 2023 · 6 comments · May be fixed by #476

Comments

@Kmeakin
Copy link
Contributor

Kmeakin commented Jan 20, 2023

We may at some point want to implement lazy evaluation:

  • I believe it would be necessary to support recursive definitions (Add letrec terms #469)
  • Could make elaboration faster by avoiding unnecessary evaluation

I tried to copy the LazyValue implementation from Pikelet, but LazyValue uses OnceCell, which makes Value invariant over its 'arena lifetime, and introduces lifetime errors everywhere. Not sure if they can be fixed, or if we can implement lazy evaluation some other way
@brendanzab
Copy link
Member

Do you mean in the semantic domain (i.e. core::semantics::Value)? Like how I use Lazy.t here? Or having explicit laziness in Fathom itself?

@brendanzab
Copy link
Member

I think yeah, if we wanted to do this we might need to use some sort of defunctionalised approach – is that what I had in Pikelet?

@Kmeakin
Copy link
Contributor Author

Kmeakin commented Jan 23, 2023

Do you mean in the semantic domain (i.e. core::semantics::Value)? Like how I use Lazy.t here? Or having explicit laziness in Fathom itself?

Just in the semantic domain for now. We could add laziness as a user facing feature later, if it's useful.

@Kmeakin
Copy link
Contributor Author

Kmeakin commented Jan 23, 2023

I think yeah, if we wanted to do this we might need to use some sort of defunctionalised approach – is that what I had in Pikelet?

Doesn't matter if its defunctionalised or not, the problem is that if a type has an UnsafeCell in any of its fields (transitively), it becomes invariant over its lifetimes. So Value -> Elim::FunApp -> LazyValue -> OnceCell -> UnsafeCell makes Value invariant

@Kmeakin Kmeakin linked a pull request Jan 23, 2023 that will close this issue
Open
@Kmeakin
Copy link
Contributor Author

Kmeakin commented Jan 23, 2023

Actually, I was able to fix the lifetime errors: just required being explicit about lifetimes in some fn signatures that previously kept lifetimes implicit

@brendanzab
Copy link
Member

Oh nice - yeah, can be hard to figure out whether adding explicit lifetimes can help when trait elision is involved…

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Lazy evaluation Kmeakin/fathom
2 participants
@brendanzab @Kmeakin