<div dir="auto">I just realized that dependent types should let us do some things with weak references and stable names less awkwardly. In particular, there are two invariants that are not (and cannot be) expressed in the type system at present:<div dir="auto"><br></div><div dir="auto">1. If two stable names are equal, then their underlying objects are equal.</div><div dir="auto">2. If a weak reference was built using a key and a value, and the key is alive, then the value is also alive.</div><div dir="auto"><br></div><div dir="auto">I hope we'll be able to express these with Dependent Haskell, using whatever the real syntax will be.</div><div dir="auto"><br></div><div dir="auto">data Weak :: k -> Type -> Type</div><div dir="auto">mkWeak :: (key :: k) -> v -> IO () -> IO (Weak key v)</div><div dir="auto">deRefWeakSurely :: (key :: k) -> Weak key v -> IO v</div><div dir="auto">-- Intentionally omitted: finalize</div><div dir="auto"><br></div><div dir="auto"><div dir="auto" style="font-family:sans-serif">data StableName :: k -> Type</div><div dir="auto" style="font-family:sans-serif">makeStableName :: (key :: k) -> IO (StableName key)</div><div dir="auto" style="font-family:sans-serif">eqStableName :: StableName x -> StableName y -> Maybe (x :~: y)</div><div dir="auto" style="font-family:sans-serif"><br></div><div dir="auto" style="font-family:sans-serif">The idea is that we can calculate the StableName of a key, look for that that in a hash table of weak pointers, and if we find it, we get evidence that we can use to dereference the weak pointer (deRefWeakSurely would use touch# under the hood, but that's not our concern).</div></div></div>