A brief explanation of the lifetimes implementation

[eriksvedang]

How the Carp lifetimes work right now

1. Lifetime variables are unified just like type variables, see

   Carp/src/Constraints.hs

   Line 158 in 5a449b0

   Constraint (RefTy a ltA) (RefTy b ltB) _ _ _ _ ->

2. When analyzing the memory management code, when something has a lifetime in its type, that lifetime gets associated with the original location being referred to, see

   Carp/src/Memory.hs

   Line 589 in 5a449b0

   addToLifetimesMappingsIfRef :: Bool -> XObj -> State MemState ()

3. For the rest of that function definition, when a reference is encountered, those mappings are then checked against the live set of variables (referred to as "deleters" in the code base) to make sure that whatever is being referenced is still alive, see

   Carp/src/Memory.hs

   Line 542 in 5a449b0

   refTargetIsAlive :: XObj -> State MemState (Either TypeError XObj)

Regarding scopes

The reason we're referring to variables (and not to scopes) is that a scope is too coarse of a unit. Within a scope multiple variables can get created in sequence with functions being called in-between. That could be solved by creating one scope per variable but still, we need to also know exactly when a variable is dead -- which might not be at the end of the scope (if it is given away before that.)

Problems / improvements

The problem with point 2 above is that it only assigns the mapping on the first occurence. A more correct behaviour (I think) would be to have a set of variables that each lifetime depends upon. This solves bugs like the second example in this issue: #470

(defn main []
  (let-do [x ""]
    (let [a [@"hi"]]
      (set! x (Array.unsafe-nth &a 0)))
    (println* x))) ; a was already dropped!

Currently this fools the memory system because everything unifies to a single lifetime variable, and that lifetime only depends on x, not on a. Having the lifetime depend on a set solves this neatly and the bug is caught -- it leads to some code in Core not compiling though. Would be nice to re-implement that and look at the problem together!

A second problem with the whole setup is that a bunch of lifetimes can be unified with the static lifetime which just makes the memory system give up and not check those references. I'm kind of at a loss how to fix that one, so would be nice to talk it through.

[redbar0n]

maybe this could serve as some inspiration (grouped allocations/lifetimes): https://www.sophiajt.com/search-for-easier-safe-systems-programming/