Open Kmeakin opened 1 year ago
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?
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?
Do you mean in the semantic domain (i.e.
core::semantics::Value
)? Like how I useLazy.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.
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
Actually, I was able to fix the lifetime errors: just required being explicit about lifetimes in some fn
signatures that previously kept lifetimes implicit
Oh nice - yeah, can be hard to figure out whether adding explicit lifetimes can help when trait elision is involved…
We may at some point want to implement lazy evaluation:
I tried to copy the
LazyValue
implementation from Pikelet, butLazyValue
usesOnceCell
, which makesValue
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