How to convert Dynamic to Forall something

Question

I have a cache with Dynamic values. Some of them have the type Delayed a.

Normally when I access the cache, I know the type a, so it's not a problem, I can use fromDynamic to cast to Maybe a.

I would like to call a function which doesn't need to know anything about the type a on a list of Dynamic. (The method is cancel :: Delay a -> IO ()). Is there a way to do so ?

Basically I need a way to do get from Dynamic to Forall a . Delayed a ?

Edit

For information, Delayed holds a pending asynchronous value and a MVar to start or Cancel it. It is equivalent to

 data Delayed m a = Delayed { blocker :: MVar Bool, async :: Async m a }

Such values are stored in a cache (which use Dynamic and store other things). When displaying the cache status, I need to be able to get the status of Delayed value (which involve accessing the blocker but has nothing to do with the actual value.

Answer 1

A value of type forall a . X a is a value which can be instantiated to any of X Int, X Bool, X String, etc. Presumably, your cache stores values of many different types, but no single value is valid at every possible type parameter. What you actually need is a value of type exists a . Delayed a. However, Haskell doesn't have first-class existential quantifiers, so you must encode that type in some way. One particular encoding is:

castToDelayed :: (forall a . Typeable a => Delayed a -> r) -> Dynamic -> r

Assume that you have this function; then you can simply write castToDelayed cancel :: Dynamic -> IO (). Note that the function parameter to castToDelayed provides a Typeable constraint, but you can freely ignore that constraint (which is what cancel is doing). Also note this function must be partial due to its type alone (clearly not every Dynamic is a Delayed a for some a), so in real code, you should produce e.g. Maybe r instead. Here I will elide this detail and just throw an error.

How you actually write this function will depend on which version of GHC you are using (the most recent, 8.2, or some older version). On 8.2, this is a very nice, simple function:

{-# LANGUAGE ViewPatterns #-}
-- NB: probably requires some other extensions

import Data.Dynamic
import Type.Reflection

castToDelayed :: (forall a . Typeable a => Delayed a -> r) -> Dynamic -> r
castToDelayed k (Dynamic (App (eqTypeRep (typeRep :: TypeRep Delayed) -> Just HRefl) a) x)
  = withTypeable a (k x) 
castToDelayed _ _ = error "Not a Delayed"

(Aside: at first I thought the Con pattern synonym would be useful here, but on deeper inspection it seems entirely useless. You must use eqTypeRep instead.)

Briefly, this function works as follows:

• It pattern matches on the Dynamic value to obtain the actual value (of some existentially quantified type a) stored within, and the representation of its type (of type TypeRep a).

• It pattern matches on the TypeRep a to determine if it is an application (using App). Clearly, Delayed a is the application of a type constructor, so that is the first thing we must check.

• It compares the type constructor (the first argument to App) to the TypeRep corresponding to Delayed (note you must have an instance Typeable Delayed for this). If that comparison is successful, it pattern matches on the proof (that is Just HRefl) that the first argument to App and Delayed are in fact the same type.

• At this point, the compiler knows that a ~ Delayed x for some x. So, you can call the function forall a . Typeable a => Delayed a -> r on the value x :: a. It must also provide the proof that x is Typeable, which is given precisely by a value of type TypeRep x - withTypeable reifies this value-level proof as a type-level constraint (alternatively, you could have the input function take as argument TypeRep a, or just omit the constrain altogether, since your specific use case doesn't need it; but this type is the most general possible).

On older versions, the principle is basically the same. However, TypeRep did not take a type parameter then; you can pattern match on it to discover if it is the TypeRep corresponding to Delayed, but you cannot prove to the compiler that the value stored inside the Dynamic has type Delayed x for some x. It will therefore require unsafeCoerce, at the step where you are applying the function k to the value x. Furthermore, there is no withTypeable before GHC 8.2, so you will have to write the function with type (forall a . Delayed a -> r) -> Dynamic -> r instead (which, fortunately, is enough for your use case); or implement such a function yourself (see the source of the function to see how; the implementation on older versions of GHC will be similar, but will have type TypeRep -> (forall a . Typeable a => Proxy a -> r) -> r instead).

Here is how you implement this in GHC < 8.2 (tested on 8.0.2). It is a horrible hack, and I make no claim it will correctly in all circumstances.

{-# LANGUAGE DeriveDataTypeable, MagicHash, ScopedTypeVariables, PolyKinds, ViewPatterns #-}

import Data.Dynamic
import Data.Typeable
import Unsafe.Coerce
import GHC.Prim (Proxy#)
import Data.Proxy

-- This part reifies a `Typeable' dictionary from a `TypeRep'.
-- This works because `Typeable' is a class with a single field, so 
-- operationally `Typeable a => r' is the same as `(Proxy# a -> TypeRep) -> r'
newtype MagicTypeable r (kp :: KProxy k) =
  MagicTypeable (forall (a :: k) . Typeable a => Proxy a -> r)

withTypeRep :: MagicTypeable r (kp :: KProxy k)
            -> forall a . TypeRep -> Proxy a -> r
withTypeRep d t = unsafeCoerce d ((\_ -> t) :: Proxy# a -> TypeRep)

withTypeable :: forall r . TypeRep -> (forall (a :: k) . Typeable a => Proxy a -> r) -> r
withTypeable t k = withTypeRep (MagicTypeable k) t Proxy

-- The type constructor for Delayed
delayed_tycon = fst $ splitTyConApp $ typeRep (Proxy :: Proxy Delayed)

-- This is needed because Dynamic doesn't export its constructor, and
-- we need to pattern match on it.
data DYNAMIC = Dynamic TypeRep Any

unsafeViewDynamic :: Dynamic -> DYNAMIC
unsafeViewDynamic = unsafeCoerce

-- The actual implementation, much the same as the one on GHC 8.2, but more 
-- 'unsafe' things
castToDelayed :: (forall a . Typeable a => Delayed a -> r) -> Dynamic -> r
castToDelayed k (unsafeViewDynamic -> Dynamic t x) =
  case splitTyConApp t of
    (((== delayed_tycon) -> True), [a]) ->
      withTypeable a $ \(_ :: Proxy (a :: *)) -> k (unsafeCoerce x :: Delayed a)
    _ -> error "Not a Delayed"

I don't know what Delayed actually is, but lets assume it's defined as follows for testing purposes:

data Delayed a = Some a | None deriving (Typeable, Show)

Then consider this simple test case:

test0 :: Typeable a => Delayed a -> String
test0 (Some x) = maybe "not a String" id $ cast x
test0 None     = "None"

test0' =
  let c = castToDelayed test0 in
   [ c (toDyn (None :: Delayed Int))
   , c (toDyn (Some 'a'))
   , c (toDyn (Some "a")) ]