为什么 Data.Dynamic 包含见证而不是类型类约束？

Question

Data.Dynamic有以下实现：

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

我想到以下定义是等效的（至少我认为）：

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

因为可以使用 到达TypeRep a约束Typeable，withTypeable而在另一个方向上，可以使用Typeable到达约束。TypeRep atypeRep

我问这个问题是因为我经常创建带有类型类约束的 GADT，通常是为了创建“存在”类型，并且看到这种类型让我怀疑是否应该添加“见证”字段，而不是使用类型类约束？在这两种方法之间进行选择时我应该考虑什么？

---

进一步的想法...

考虑这样的事情：

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 

在这里，明确参数而不是仅包含类型类约束具有实际目的，因为您可以对同一类型有不同的排序，并且第二个定义允许这样做，而不会出现新类型愚蠢的情况。

但这似乎很愚蠢，因为您的类型基本上是单例，就像TypeRep a.

我想一个小小的好处是，也许证人可以作为函数的参数，这意味着您不必使用类型应用程序来提取构造函数。

就像我可以做的第一个定义一样：

f (Dynamic tr x) = ...

代替

f (Dynamic @a x) = ...

但我发现我所做的是：

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

f因为如果定义了任何显式类型化的子函数，则类型在范围内非常方便，并且没有很多函数TypeRep a将其作为参数，因此它们通常需要类型 application 或 take Proxy @a，所以我最终需要范围内的类型反正。

我已经开始考虑这个问题，因为我已经在自己的代码中定义了类型（如果我重新发明了轮子并且这存在于其他地方，请大声喊出）：

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

我将其定义为基本上复制Dynamic，但我想也许只是：

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

是一个更好的定义。

Answer 1

我怀疑答案大多只是历史。比（GHC 6.8.1，根据手册）Dynamic要老得多，这对于您的现代定义都是必需的。ExistentialQuantification在此扩展之前，您无法存储类似a数据类型的类型，也无法存储类似的约束Typeable a（即使它没有提到类似的存储类型a）。

例如，在 GHC 5.04 源代码中（即使作为 bzip 存档，也小于 5MB！），我发现其Dynamic定义如下

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

我认为建议部分原因Dynamic包含TypeRepnow 是合理的，因为它始终包含TypeRep。

由于Dynamic数据构造函数过去是非导出的，因此库作者可以将其更改为公开后使用Typeable（这发生在base-4.10/GHC 8.2.1 中），而不会破坏用户代码。但没有充分的理由这样做。实际上，甚至有两个更薄弱的理由更喜欢这个TypeRep版本：

• 摆脱Typeable aaTypeRep a实际上是黑魔法，通过（本质上）将unsafeCoercea 转换Typeable a => r为 a 来实现TypeRep a -> r。（当然它仍然是安全的，并且在最近的 GHC 中，该技巧显然已被编入其自己的withDict原语中。）TypeRep as 是涉及较少黑暗艺术的“正常”值。
• 当您将类型打包成值并移动它们时，能够实际命名它们是很好的。ATypeRep a是一个可以与名称绑定的值，并且可以用作Proxy表示类型的 -esque 标记a。（请注意，许多 API 不需要，Proxy a而是需要量化。） A在您获得它的那一刻就消失在背景中。这对于 来说有点没有意义，因为您还获得了实际值（因此您可以执行例如），但很高兴已经给出了。另请注意，在公开其构造函数时，类型应用程序模式并不存在。proxy aproxyTypeable aDynamicx :: alet proxyOf :: a -> Proxy a in proxyOf xTypeRepData.Dynamic

在当时，这两者基本上只是表面上的考虑，而在今天则显得不那么重要了。

现在，对于今天编写的代码，我将指出类型应用程序/抽象仍然无法完成代理可以完成的所有操作。仍然缺少为 lambda 命名类型参数的能力，因此在某些情况下，由于技术原因，您必须更喜欢代理式 API 而不是类型应用程序 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!

如果您没有预料到这种情况会发生在您身上，或者您只是不介意代码中的微小不一致，其中withSomeStructure'给您 aProxy但假设withDynamicF没有，那么Typeable的版本DynamicF就可以了。我个人还是更喜欢这个TypeRep版本。