Typeable constraint on fromAddHandler

[HeinrichApfelmus]

It would be very nice if we could get rid of the Typeable constraint on the fromAddHandler function, so that its type signature becomes

fromAddHandler :: AddHandler a -> NetworkDescription (Event a)

Not sure if that is possible, but this issue will remind me to look for a solution.

[ehird]

I may be wrong, but it looks like the only use of Typeable is here.

These should be replaceable with unsafeCoerce (this seems to be a running theme in my solutions!), as long as fromUniverse is never called with the right channel but expecting the wrong type.

[HeinrichApfelmus]

That would probably work, but I'm hesitant to use unsafeCoerce again. Instead, I'd like to use an existing package, like vault or thelike. The Universe type might be an interesting addition to the vault package; after all, it's a disjoint sum, dual to the "infinite" product Vault.

[ehird]

To be honest, I'm not entirely sure what the Universe type's semantics are; the closest API that does not let the user perform an unsafe coercion seems to be:

data Universe
data Portal a
toUniverse :: a -> (Portal a, Universe)
fromUniverse :: Portal a -> Universe -> Maybe a

where fromUniverse p u is Just x iff (p,u) = toUniverse x and Nothing otherwise. The issue with this API is that two different calls of toUniverse with the same arguments are distinguishable from another, because the portal of one will not work with the universe of the other; thus breaking referential transparency. Or possibly

data Universe
data Portal a
newPortal :: IO (Portal a)
toUniverse :: Portal a -> a -> Universe
fromUniverse :: Portal a -> Universe -> Maybe a

where fromUniverse p u is Just x iff u = toUniverse p x, and Nothing otherwise. The issue there is that after one uses toUniverse on a portal, that portal cannot be used to create any more universes, or type-safety is violated; so toUniverse would have to be in IO (or at least ST), which seems a shame.

I admit that I can't figure out a use for these safe APIs — it seems like portals would only be useful through an existential, and I'm not sure how you'd achieve that in practice — but after looking at fromAddHandler's implementation I've implemented a variant of the first API with toUniverse in ST (or IO) and reusing the keys used for vaults in place of portals in the universe branch of my fork of vault, to distract myself from some ugly Template Haskell issues in another project.

Unfortunately this required turning (Key k) pattern matches into (Key (I.Key k)) pattern matches, but since these are only used in the small implementation modules of the structures themselves, it shouldn't matter too much. The runtime representation is identical.

[HeinrichApfelmus]

I think that the second API looks good. It must be safe because it can be implemented in terms of Vault. :-)

type Universe = Vault
type Portal a = Key a
newPortal = newKey
toUniverse key a = insert key a empty
fromUniverse     = lookup

Of course, the type is to be understood as a newtype whose implementation is not exported.

Since this is so very simple, it may not be worth adding it to the vault package, after all; or at least under a different name, something paralleling Data.Dynamic would probably be more fitting. (I originally chose Universe because it's "the universal type" which contains all others.)

[ehird]

Hmm, yes, it can be implemented in terms of Vault, but the problem is that the same Portal can be used with multiple universes. There's no type error, but you can still get "the wrong value" out.

I suppose this isn't a problem; you might even want to do it intentionally, to "modify" (persistently) the value inside the universe.

[HeinrichApfelmus]

Ah, I see. You mentioned the same issue with Vault. One can add a type parameter and make it Vault s to enforce different keys for different vaults, but that's probably more trouble than it's worth.

Thanks a lot for this discussion, I now have a clear idea of how to get rid of the Typeable constraint by using Vault. I'll leave this open until I get around to implementing the change.

[HeinrichApfelmus]

I've removed the Typable constraint from the fromAddHandler function with the help of the Data.Vault module from the vault package.