Why does Data.Dynamic contain a witness instead of a typeclass constraint?

Question

Data.Dynamic has the following implementation:

data Dynamic where
    Dynamic :: TypeRep a -> a -> Dynamic

It has occurred to me that the following definition would be equivalent (at least I think):

data Dynamic where
    Dynamic :: Typeable a => a -> Dynamic

Because one can get from TypeRep a to a Typeable constraint using withTypeable, and in the other direction, go from a Typeable constraint to TypeRep a using typeRep.

I ask this question because I often have created GADTs with typeclass constraints, often to create "existential" types, and seeing this type has made me question whether instead of using typeclass constraints I should be adding a "witness" field? What should I consider when choosing between these two approaches?

---

Further thoughts...

Consider something like this:

data SillyListA m where
  SillyListA :: Ord a => (a -> m ()) -> [a] -> SillyList m 

data SillyListB m where
  SillyListB :: (a -> a -> Ordering) -> (a -> m ()) -> [a] -> SillyList m 

Here it being explicit about the argument instead of just including the typeclass constraint has a practical purpose, because you could have different orderings on the same type, and the second definition allows that without newtype silliness.

But that just seems silly where your type is basically a singleton as is the case in TypeRep a.

I guess one slight benefit is that perhaps the witness can be made an argument to functions which means you don't have to use type applications to pull out the constructor.

So like with the first definition I can do:

f (Dynamic tr x) = ...

Instead of

f (Dynamic @a x) = ...

But what I find I do anyway is:

f (Dynamic @a _ x) = ...

Because the type is really handy to have in scope if f has any sub-functions defined that are explicitly typed, and not many functions take TypeRep a as an argument, they usually either require a type application or take Proxy @a, so I end up needing the type in scope anyway.

I have started thinking about this because I have defined the type in my own code (please shout out if I've reinvented the wheel and this exists elsewhere):

data DynamicF f where
  DynamicF :: forall (a :: Type) f. TypeRep a -> f a -> DynamicF f

And I defined it like this basically copying Dynamic, but I'm thinking maybe just:

data DynamicF f where
  DynamicF :: forall (a :: Type). Typeable a => f a -> DynamicF f

Is a better definition.

Answer 1

I suspect the answer is mostly just history. Dynamic is much older than ExistentialQuantification (GHC 6.8.1, according to the manual), which is necessary for both your modern definitions. Before this extension, you could not store a type like a in a datatype and you also could not store a constraint like Typeable a (even if it didn't mention a stored type like a).

E.g. inside the GHC 5.04 sources (which, even as a bzip archive, is <5MB!), I find that Dynamic is defined as follows

data Dynamic = Dynamic TypeRep Obj
data Obj = Obj
-- obviously, neither Dynamic nor Obj is exported!

I think it's reasonable to suggest that part of the reason Dynamic contains a TypeRep now because it's always held a TypeRep.

Since the Dynamic data constructor used to be non-exported, the library authors could have just changed it to use Typeable once it was made public (which happened in base-4.10/GHC 8.2.1) without breaking user code. But there was no strong reason to do this. Actually, there were even two weak reasons to prefer the TypeRep version:

• Getting Typeable a out of a TypeRep a is actually black magic, implemented by (essentially) unsafeCoerceing a Typeable a => r into a TypeRep a -> r. (It is of course still safe, and in recent GHC the trick has apparently been codified into its own withDict primitive.) TypeRep as are "normal" values involving fewer dark arts.
• When you're packing types up into values and moving them around it's nice to be able to actually name them. A TypeRep a is a value that you can bind with a name and can be used as a Proxy-esque token to represent the type a. (Note that many APIs don't require Proxy a but rather proxy a, where proxy is quantified over.) A Typeable a vanishes into the background the moment you get it. This is somewhat moot for Dynamic, since you are also getting an actual value x :: a (so you can do e.g. let proxyOf :: a -> Proxy a in proxyOf x), but it's nice to have a TypeRep already given. Also note that, at the time Data.Dynamic had its constructor exposed, type application patterns did not exist.

Both of these would have been basically just cosmetic considerations at the time and are even less important today.

Now, for writing code today, I will point out that type applications/abstractions still cannot do everything that proxies can do. The ability to name type arguments to lambdas is still missing, and thus there are situations where, for technical reasons, you must prefer a proxy-ish API over a type applications API.

class Eq a => Structure a where
    injZ :: Integer -> a
data SomeStructure where
    SomeStructure :: Structure a => SomeStructure

-- purely types-based API...
withSomeStructure :: SomeStructure -> (forall a. Structure a => r) -> r
withSomeStructure (SomeStructure @a) f = f @a
x :: SomeStructure -> Bool
x s = withSomeStructure s _can'tBindaInThisHole
-- ...doesn't work

-- proxy-based API...
withSomeStructure' :: SomeStructure -> (forall a. Structure a => Proxy a -> r) -> r
withSomeStructure' (SomeStructure @a) f = f (Proxy @a)
y :: SomeStructure -> Bool
y s = withSomeStructure' s (\a -> injZ 0 == injZ 2 `asProxyTypeOf` a)
-- ...works!

If you don't anticipate such a situation happening to you, or if you simply don't mind a minor inconsistency in your code, where withSomeStructure' gives you a Proxy but a hypothetical withDynamicF doesn't, then the Typeable version of DynamicF is fine. I personally would prefer the TypeRep version still.