Someone mentioned to me recently that they were interested in having a way to indicate space constraints into a type system such that you can tell if memory is close or far from any other given memory. Honestly I’m not sure what their ultimate goal is (the only thing I can think of is that they want to ensure good cache usage), but by itself this is a very interesting problem to consider.
My immediate thought is that you can use a dependent typing system and embed pointer addresses into the type signatures. Then all you are going to need is a “these objects are sufficiently close” proof and you’re done.
However, I doubt my naive solution would ever actually be useful for anything. For starters stack randomization is going to ensure that none of your proofs for stack allocated data hold. But maybe that’s not really a big problem. You can just create an abstract address that’s relative to wherever your program’s stack starts. The big problem, though, is going to be dynamically allocated memory. Last I checked we didn’t have a way to control when heap space starts to get fragmented in a way that’s analyzable at compile time. And really this is just the start. For example, I don’t think I really want to be the one in charge of type checking that an arbitrary value on the stack is within a specific distance of an arbitrary value on the heap.
I assert that the problem has to do with trying to get whole program validation. If we narrow our vision a bit, I suspect we might end up with a plausible solution.
If we can subdivide our memory constrained problems into atomic chunks, then we can implement them, individually, as part of a DSL. The DSL itself can be type checked (easiest example would to be to just use GADTs) to ensure that our memory distance constraints hold. Additionally the DSL can also ensure that our mini program’s total memory usage will stay smaller than whatever amount we are confident our allocator can contiguously provide at runtime. At runtime our program can still fail if the allocator can’t provide a sufficient amount of contiguous memory, but that’s the world we live in right now anyway (malloc can fail and GCs can throw out of memory exceptions).
