Laziness and Sharing

[ejgallego]

This is a general issue to discuss laziness and sharing w.r.t. the seralization of objects.

A motivating example is the following usual Coq snippet:

type a = { foo : bar (* some data *) ; env : Environ.env}

now imagine we have in Python, an object a of type a_class, with methods a.foo and a.env.

It would be great if we could avoid the conversion of a.env until it is actually accessed, as env is actually a huge object. That would mean which a.foo could be done quickly.

A problem we have with the delay in indeed the imperative nature of some code. So that approach, could be only used for objects that we mark as "safe" [that is to say, purely functional so themselves are closed].

Another approach could be actually to use some form of sharing, as done in the OCaml "runtime"; however, this may still be too expensive in some use cases.

Improvements on this pattern are also due in Coq's side.