gistfile1.txt

// Consider a "relative" pointer to some offset within
// a buffer with some base address.

struct RelativePtr {
  void* base;
  int offset;
}

// Now consider some operation to compute the relative address:

void* absolute(RelativePtr p) {
  return p.base + p.offset;
}

// Is there any language out there that would let me
// abstract over when and where the value of `base` is known?

// For example, let's say you have a structure with
// two relative pointers with the same offset:

struct Foo {
  RelativePtr a;
  RelativePtr b;
}

// Ideally, the runtime representation of Foo would be:

struct Foo {
  void* base;
  int offsetA;
  int offsetB;
}

// And the absolute function should still work:

Foo foo = ...;
void* p = absolute(foo.a);

// There needs to be some way to express the shared-base pointer
// constraint, but no language that I know of offers this.

// Does this exist somewhere? Is there relavant literature?

Basic version using dependent records in Idris:

data RelativePtr : (base : Nat) -> Type where
  RP : Nat -> RelativePtr base

absolute : {base : Nat} -> RelativePtr base -> Nat
absolute {base} (RP offset) = base + offset

record Foo where
  constructor MkFoo
  base : Nat
  a    : RelativePtr base
  b    : RelativePtr base

test : Foo -> (Nat, Nat)
test foo = (absolute (a foo), absolute (b foo))

With more work, it'd be possible to distinguish at the type level between absolute pointers and offsets (i.e., points and vectors) and also to record the extents of the data pointed to.

I figured there was a dependent typing scheme, but I don't read Idris yet. I suspect you could do something similar in F*. In F# it is fairly common to make the concrete representation opaque, and to use Active Patterns and constructor functions to provide the appropriate semantics. Of course it requires that Foo and Relative have to be defined in the same scope, limiting its utility somewhat. But if you squint it kind of looks like a fancy type system solution. 😉

module Pointers

type Foo            = private { Base : Ptr; A : Offset; B : Offset }
and Relative        = private { Base : Ptr; Offset : Offset }
and private Ptr     = Address ref
and private Offset  = uint32
and Address = uint64

let mkFoo ptr a b = { Foo.Base = ref ptr; A = a; B = b } // TODO bounds checking
let (|Pointers|) (f : Foo) = { Base = f.Base; Offset = f.A }, { Base = f.Base; Offset = f.B }
let dereference (rp : Relative) (f : Address -> 'o) : 'o =
  // lock rp.Base
  !rp.Base + (uint64 rp.Offset) |> f
let move (f : Foo) (a' : Address) =
  // lock f.Base
  let a = f.Base
  a := a'
  f

It's just a sketch of the semantics, but I think that's germane when thinking about the shared base address constraint. Anyway, I know the above is not what you're positing, but it was fun nonetheless. Cheers!