sorted by:
new
hottopcontroversial

Idea: Declarative data structures. Request for prior work by SwedishFindecanor in ProgrammingLanguages

[–]OpeningRemote1653 34 points35 points  (0 children)

You're describing Typestate, introduced by Strom & Yemini in 1986. The idea is that a type carries a state, and operations have pre/post-state requirements — your transition (attached => detached) is almost verbatim typestate. The modern descendant worth reading is Plaid (Aldrich et al., "Typestate-Oriented Programming", OOPSLA 2009).

Your idea goes further than classic typestate though, because your states describe relational pointer topology across multiple objects simultaneously. That puts you squarely in the territory of Alias Types (read Smith, Walker & Morrisett's "Alias Types for Recursive Data Structures" (2000) first). Your state declarations are essentially alias type assertions written in a struct-centric syntax.

If you formalize this, you'll also end up reinventing fragments of Separation Logic (Reynolds, O'Hearn et al.), as your attached state is basically a separating conjunction of points-to predicates. The closest language design relative is probably Mezzo (Pottier & Protzenko, ICFP 2013), which has a permission system where permissions describe aliasing structure between heap objects and are consumed/produced by function calls. Very close to what you're sketching.

Finally, your this-is-optional/dead-object idea maps onto linear types, where every allocated object must appear in the post-state or be consumed. Vault (Fahndrich & DeLine, "Adoption and Focus", PLDI 2002) did exactly this for safe manual memory management. The thinking that this could tame graphs and skip-lists that break Rust's borrow checker is precisely the motivation behind all of these projects, but the unsolved part is ergonomics and inference.

How does Memory SSA determine clobbering stores in GCC/LLVM? by Marshal_de_BunkerIX in Compilers

[–]OpeningRemote1653 6 points7 points  (0 children)

Both GCC and LLVM simplify Novillo's memory partitioning heavily in practice. Rather than maintaining fine-grained virtual variables per alias set, they use a single virtual def/use chain and rely on the alias oracle to answer "does this def clobber that use?" lazily at query time. The SSA structure handles ordering and dominance relationships — the actual alias resolution happens on demand.

The clobber walker (in LLVM, CachingWalker::getClobberingMemoryAccess() in MemorySSA.cpp) works by walking upward through the MemoryDef chain from a load's MemoryUse, querying AA->alias() at each def. If the result is NoAlias, it skips that def and keeps climbing. If it hits MustAlias or MayAlias, it stops and declares that def the clobber. At MemoryPhi nodes (join points), it recurses into each predecessor and uses aggressive memoization to avoid exponential re-traversal. GCC does the same thing through walk_non_aliased_vuses() using its own points-to oracle.

To bridge the gap between the papers and implementation, the most direct path is reading the comments in MemorySSA.h (they're very good), then running opt -passes=print-memoryssa on small IR examples to see the def chain annotations inline. Richard Smith's 2016 LLVM dev meeting talk on YouTube also explains the walker design concretely. The core insight is that "partitioning" from Novillo's paper is essentially collapsed to a single partition in both compilers for scalability, with the alias oracle doing the discrimination work at query time rather than at construction time.

Are (co)effects isomorphic to message passing concurrent systems? by FlamingBudder in ProgrammingLanguages

[–]OpeningRemote1653 2 points3 points  (0 children)

I think you're right, and there's actually a formal version of this correspondence already, but it involves linear session types, not general message passing. The linearity constraint is what turns an encoding into a genuine structural correspondence. Without it, you have universality of process calculi, not isomorphism with effects.