[Haskell-cafe] Dependent types, weak references, and stable names

[David Feuer]

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:

1. If two stable names are equal, then their underlying objects are equal.
2. If a weak reference was built using a key and a value, and the key is
alive, then the value is also alive.

I hope we'll be able to express these with Dependent Haskell, using
whatever the real syntax will be.

data Weak :: k -> Type -> Type
mkWeak :: (key :: k) -> v -> IO () -> IO (Weak key v)
deRefWeakSurely :: (key :: k) -> Weak key v -> IO v
-- Intentionally omitted: finalize

data StableName :: k -> Type
makeStableName :: (key :: k) -> IO (StableName key)
eqStableName :: StableName x -> StableName y -> Maybe (x :~: y)

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).
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180828/e8cc372d/attachment.html>