# Typed representation of a memory model

Assume a simple procedural language, where statements write and read from local memory via references and procedures accept arguments of n different scalar types (say floats, ints and strings) and tuples (or records or other structured monomorphic data).

When I try to embed such a language in a type-safe host language (say OCaml) I need to define the type of the memory. (Ok, I could encode it as a heterogeneous list as well, but that seems quite inefficient).

So my intuitive attempt would be to model it like this:

type mem = { floats : float array; ints : int array;
structured : mem array}

type 'a ptr = { read : mem -> 'a; write : mem -> 'a -> unit }

let float_ptr i = { read = (fun {floats} -> floats.(i)) ;
write = (fun m a -> m.floats.(i) <- a) }


A float assignment would then require a float-pointer as target and so on. Since this seems quite useful, I assume that such an encoding has already been done somewhere, but without a useful name I am unable to search for it.

Is there any published work on such a memory encoding (and the required transformations etc.)?

p.s.: If someone could add the tags memory-model and embedding, I would be grateful, I had a hard time finding some adequate tags.

• This approach would work until you have to represent pointers to tuples/records/structs. Unless that is, you add another array for (int,int), one for (int,float), one for (int,(int,((float,int),int))) ... but we can not have infinitely many fields. To do this properly, probably one would require dependent types or some more restricted variant like Haskell's GADTs. Even in that case, it can be tricky to allow for pointers to a first component of a tuple. Further, one can always use a giant sum type, and make an array of that, effectively postponing all type checks at runtime (which is not fun). – chi Jul 22 '16 at 12:49
• Every product type can be encoded into its own mem-record (that is why there is the structured field). – choeger Jul 25 '16 at 8:43