为什么 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 a

 约束到 

typeRep。

我问这个问题是因为我经常创建带有类型类约束的 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

作为参数，因此它们通常需要类型应用程序或采用

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

我怀疑答案大多只是历史。

Dynamic

比

ExistentialQuantification

更古老（GHC 6.8.1，根据手册），这对于您的现代定义都是必要的。在此扩展之前，您无法在数据类型中存储像

a

这样的类型，也无法存储像

Typeable a

这样的约束（即使它没有提到像

a

这样的存储类型）。

例如在 GHC 5.04 源代码中（即使作为 bzip 存档，<5MB!), I find that

Dynamic

定义如下

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

我认为现在认为

Dynamic

包含

TypeRep

的部分原因是合理的，因为它 always 持有

TypeRep

。

由于

Dynamic

数据构造函数过去是非导出的，库作者 could 可以将其更改为在公开后使用

Typeable

（这发生在

base-4.10

/GHC 8.2.1 中），而不会破坏用户代码。但没有充分的理由这样做。实际上，甚至有两个微弱的理由更喜欢

TypeRep

版本：

• 从

  Typeable a

  中获取

  TypeRep a

  实际上是黑魔法，通过（本质上）将

  unsafeCoerce

  Typeable a => r

  转换为

  TypeRep a -> r

  来实现。 （当然它仍然是安全，并且在最近的 GHC 中，该技巧显然已被编入其自己的

  withDict

  原语中。）

  TypeRep a

  是涉及较少黑暗艺术的“正常”值。
• 当您将类型打包成值并移动它们时，能够真正地命名它们是很好的。

  TypeRep a

  是一个可以与名称绑定的值，并且可以用作

  Proxy

  式标记来表示类型

  a

  。 （请注意，许多 API 不需要

  Proxy a

  ，而是需要

  proxy a

  ，其中

  proxy

  已被量化。）

  Typeable a

  在您获得它时就会消失在背景中。这对于

  Dynamic

  来说有点没有意义，因为您还获得了实际值

  x :: a

  （因此您可以执行例如

  let proxyOf :: a -> Proxy a in proxyOf x

  ），但是已经给出了

  TypeRep

  是很好的。另请注意，在

  Data.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'

会给您

Proxy

但假设的

withDynamicF

则不会，那么

Typeable

版本的

DynamicF

很好。我个人还是更喜欢

TypeRep

版本。