haskell 为什么Data.dynamic包含见证服务器而不是类型类约束？

Data.Dynamic有以下实现：

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

字符串
我认为下面的定义是等价的（至少我认为是这样）：

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

型
因为可以使用withTypeable从TypeRep a得到Typeable约束，而在另一个方向上，可以使用typeRep从Typeable约束得到TypeRep a。
我问这个问题是因为我经常使用类型类约束创建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

型
这里明确参数而不是仅仅包含类型类约束有一个实际的目的，因为你可以在同一类型上有不同的顺序，第二个定义允许这样做，而不会愚蠢地使用newtype。
但是，如果你的类型基本上是一个单例，就像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

型
是一个更好的定义。

我怀疑答案大多只是历史。Dynamic比ExistentialQuantification古老得多。（GHC 6.8.1，根据手册），这是必要的两个现代定义。在此扩展之前，你不能在数据类型中存储像a这样的类型，也不能存储像Typeable a这样的约束。（即使它没有提到像a这样的存储类型）。
例如，在GHC 5.04源代码（即使作为bzip存档，也小于5 MB！）中，我发现Dynamic的定义如下

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

字符串
我认为这是合理的建议，部分原因是Dynamic现在包含一个TypeRep，因为它 * 总是 * 持有一个TypeRep。
由于Dynamic数据构造函数过去是不可导出的，因此库作者 * 可以 * 在base-4.10/GHC 8.2.1中公开它时将其更改为使用Typeable，而不会破坏用户代码。但没有强烈的理由这样做。实际上，甚至有两个弱理由更喜欢TypeRep版本：

从TypeRep a中获取Typeable a实际上是一种黑魔法，（本质上）是通过unsafeCoerce将Typeable a => r转化为TypeRep a -> r来实现的。（当然，它仍然是 * 安全的 *，在最近的GHC中，这种技巧显然已经被编入了自己的withDict原语中。）TypeRep a s是“正常”值，涉及较少的黑魔法。
当你把类型打包成值并移动它们时，能够真正地给它们命名是很好的。TypeRep a是一个值，你可以用一个名称绑定它，它可以用作Proxy-esque标记来表示类型a。（注意，许多API不需要Proxy a，而是需要proxy a，其中proxy被量化。）Typeable a在您得到它的那一刻就消失在背景中。这对于Dynamic来说有点无意义，因为你也得到了一个实际的值x :: a（所以你可以这样做，例如let proxyOf :: a -> Proxy a in proxyOf x），但是已经给出了一个TypeRep是很好的。还要注意，在Data.Dynamic公开其构造函数的时候，类型应用模式还不存在。

这两点在当时基本上都只是表面上的考虑，在今天甚至不那么重要。
现在，对于今天的代码编写，我将指出类型应用程序/抽象仍然不能做代理可以做的所有事情。将类型参数命名为代理的能力仍然缺失，因此，出于技术原因，您必须选择代理式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没有，那么DynamicF的Typeable版本就可以了。我个人还是更喜欢TypeRep版本。

haskell 为什么Data.dynamic包含见证服务器而不是类型类约束？

1条答案

相关问题

热门标签

最新问答