Lazy evaluation

[Kmeakin]

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]

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]

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]

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]

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]

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]

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