Structs with cyclic dependencies

[ismailkuru]

Hi,

I have a quick question. As far as I understand, goose can generate gooselang version of the following type A struct { a uint64 b *B } type B struct { b uint64 a *A } but we cannot get it compiled in Perennial, am I right?

Thanks Ismail

[ismailkuru]

Oh! I see my answer here: https://github.com/tchajed/goose/blob/master/docs/future-work.md Thanks!

[tchajed]

Glad you found an answer yourself! This is pretty tricky to support correctly. We don't currently need it, but might eventually want recursive structs (although not mutual recursion).

The good news is that we no longer support type-checking arbitrary GooseLang code using the GooseLang type system, so we don't need general recursive types in that type system. The bad news is the semantics does rely on knowing something about the structure of types to store values in memory (this is because product types are split into a heap cell per value, so that they can be loaded/stored independently).

We could still solve this, by annotating any loads of these recursive fields with the correct type rather than relying on the struct definition for the type information (because the struct can't record the cyclic dependency). From there things should work in Iris, with the caveat that you still need termination for your predicates in Coq. A classic example is that you can write a linked-list representation predicate in separation logic, and the predicate is structurally recursive in the list.

[ismailkuru]

Yes, I actually anticipated this justification as I also tried to follow the goose_lang development from the commits :) Thank you so much for the clarification!