[Tarean]

Twee (an equational theorem prover in Haskell used by quickspec) has an interesting take on this. Terms are slices of arrays, but you get a normal interface including pattern matching via synonyms. It can also be nice to use phantom types of your references (array offsets), so if you project them into flat view types you can do so type safely

Requires the language to have something equivalent to pattern synonyms to be as invisible as twee, though.

In twee a TermList is a slice of a bytearray (two ints for offset/length plus a pointer).

And a term is an int for the function symbol and an unpacked TermList for the arguments.

The pattern match synonyms load a flat representation from the array into a view type, and the allocation of the view type cancels out with the pattern matching so everything remains allocation free.

https://hackage.haskell.org/package/twee-lib-2.4.2/docs/Twee...

[Tarean]

Forgot to mention: In the twee style, the int for the function id contains metadata (is it a unification variable or constant name? how many args does it take?). That way f1(f3(f5(), f7())) would be serialised as something like [1,3,5,7], without even references to other offsets