Dependent types, weak references, and stable names

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

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).

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Dependent types, weak references, and stable names

Richard Eisenberg-4
I'm not very familiar with these features, but the APIs you write below seem quite plausible. This is the kind of thing dependent types are very good at!

Richard

> On Aug 28, 2018, at 9:27 PM, David Feuer <[hidden email]> wrote:
>
> 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).

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.