哈Ha
几天前，在我的一个兴趣项目中，任务就是编写度量标准存储库。
任务本身非常简单地解决了，但是我与Haskell的问题（尤其是在我自己娱乐的项目中）是不可能仅解决并解决问题。 有必要确定，扩展，抽象，抽象，然后进一步扩展。 因此，我想使度量的存储可扩展，以免事先不指定它们的存储位置。 这本身是另一篇文章的主题，今天我们将考虑一个小问题：为以前未知的类型编写类型安全的包装。 类似于动态类型，但是具有静态保证，我们不会胡说八道。
我认为，这篇文章不会为有经验的Haskellists打开任何新内容，但是现在我们至少要把这种成分开箱即用，并且在以后的文章中也不会分心。 好吧，或者您不能那么谦虚地说我已经提出了一个完整的设计模式。
因此，首先我们提出问题。 我们需要能够将某些对象与以前未知类型的值相关联。 或者，换句话说，必须将先前未知类型的值用作某种映射中的键。
自然，我们并不疯狂，我们将不需要任何类型的值的支持。 我们要求类型（即使未知）也要支持排序。 用Haskell术语，这意味着我们支持实现Ord a类的type a 。
请注意，我们可能需要支持以获取哈希值并检查是否相等，但是出于多种原因，将自己限制在比较范围内会更加方便和明确。
当存储已知实现某种类型的类的值时，Haskell中通常使用存在性类型：
data SomeOrd where MkSomeOrd :: Ord a => a -> SomeOrd
因此，如果为我们提供了SomeOrd类型的对象，并SomeOrd进行了模式匹配：
foo :: SomeOrd -> Bar foo (MkSomeOrd val) = ... (1) ...
那么在第(1)点，我们不知道val具有哪种类型，但是我们知道（最重要的是，计时器也知道） val实现了Ord时间类。
但是，如果类的类型函数隐含两个（或更多）参数，则使用这样的记录几乎没有用处：
tryCompare :: SomeOrd -> SomeOrd -> Bool tryCompare (MkSomeOrd val1) (MkSomeOrd val2) = ?
要使用Ord方法，必须使val和val2相同的类型，但这根本不必做！ 事实证明，我们的SomeOrd无用的。 怎么办
尽管Haskell是一种具有激进类型擦除功能的编译语言（编译后，它们通常不存在），但是如果被询问，编译器仍然可以生成运行时类型代表。 类型a的角色代表是类型TypeRep a的值，并且 要求 生成由Typeable typeclass回答。
顺便说一句顺便说一下， a不必是通常意义上的类型，即属于一个* 。 它可以是任何其他类型的k ，从理论上讲，您可以通过存储所学习类型等的运行时表示来做一些很酷的事情，但是我还没有弄清楚到底是什么。
另外，如果我们有两个不同的rep1 :: TypeRep a, rep2 :: TypeRep b实例，那么我们可以比较它们并检查它们是否代表相同的类型。 而且，如果它们实际上表示相同的类型，则显然a与b重合。 而且，最重要的是，检查类型表示形式是否相等的功能返回的结果可以使打字员信服：
eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~~: b)
这里写什么废话？
首先， eqTypeRep是一个函数。
其次，它是多态的，但不仅是类型，而且还包括这些类型的变体。 这由forall k1 k2 (a :: k1) (b :: k2) -这意味着a和b不仅可以是Int或[String]类的普通类型，还可以是例如臭名昭著的构造函数（请参见DataKinds和其他使Haskell认证的尝试。 但是我们不需要所有这些。
第三，它接受两个可能不同类型的运行时表示形式TypeRep a和TypeRep b 。
第四，它返回Maybe (a :~~: b)类型的值Maybe (a :~~: b) 。 最有趣的事情发生在这里。
如果类型不匹配，则该函数返回通常的Nothing ，一切都很好。 如果类型匹配，则该函数返回Just val ，其中val的类型为a :~~: b 。 让我们看看它是什么类型：
现在让我们谈谈。 假设我们得到a类型的val值a :~~: b 。 如何建造？ 唯一的方法是使用HRefl构造函数，该构造函数要求图标的两侧:~~:它应该相同。 因此， a与b一致。 而且，如果我们在val上进行zapternnom-match，那么taypcheker也将对此有所了解。 因此，是的， eqTypeRep函数返回证明两个潜在不同的类型实际上相同的证明。
但是，在上面的段落中，我撒了谎。 没有人阻止我们在Haskell中编写类似
wrong :: Int :~~: String wrong = wrong
或
wrong :: Int :~~: String wrong = undefined
或以一堆不太明显的方式破坏系统。 这是众所周知的狭义圈子的一种表现，说Haskell作为逻辑是不一致的。 在具有更强类型系统的语言中，此类定义未加盖章。
因此，在上面引用的文档中提到了终止价值 。 上面wrong实现的两个变体都不会产生这个极高的终止值，这给了我们一点理由和信心：如果我们在Haskell上的程序终止 （并且没有遇到undefined ），那么其结果对应于所写的类型。 但是，这里有一些与懒惰有关的细节，但是我们不会打开这个主题。
顺便说一下，上面代码中Haskell弱点的第二个表现是eqTypeRep函数的类型。 在更强的语言中，它将返回一个更强的类型的值，这不仅会证明类型相等，如果它们实际上相等，还会证明其不平等，如果它们实际上是不相等的。 但是，Haskell逻辑的不一致会使这些功能变得毫无意义：当您将该语言用作定理的证明者而不是编程语言，并且不将Haskell用作证明者时，这一切都很重要。
噢，对数和类型理论足够多了，让我们回到指标上来。 现在只要画一只猫头鹰 上面的讨论暗示了将其存储在我们的存在类型中就足够了，这也是该类型的大多数运行时表示形式，一切都会很好。
这导致我们对包装器类型进行以下实现：
data Dyn where Dyn :: Ord a => TypeRep a -> a -> Dyn toDyn :: (Typeable a, Ord a) => a -> Dyn toDyn val = Dyn (typeOf val) val
现在，我们编写一个具有以下功能的函数：
Dyn类型的两个值；- 一个为任何类型的两个值产生一些东西的函数，
仅基于创建Dyn时提到的常量（对此， forall负责），
如果两个Dyn存储相同类型的值，则调用该方法； - 如果类型仍然不同，则调用后备功能，而不是前一个功能：
withDyns :: (forall a. Ord a => a -> a -> b) -> (SomeTypeRep -> SomeTypeRep -> b) -> Dyn -> Dyn -> b withDyns f def (Dyn ty1 v1) (Dyn ty2 v2) = case eqTypeRep ty1 ty2 of Nothing -> def (SomeTypeRep ty1) (SomeTypeRep ty2) Just HRefl -> f v1 v2
SomeTypeRep是TypeRep a上任何a的现有包装。
现在，我们可以实现例如相等性检查和比较：
instance Eq Dyn where (==) = withDyns (==) (\_ _ -> False) instance Ord Dyn where compare = withDyns compare compare
在这里，我们利用了SomeTypeRep可以相互比较这一事实，因此排序的后备功能也可以compare 。
做完了
直到现在，不归纳是一个罪过：我们注意到在Dyn ， toDyn和withDyns内部，我们没有专门使用Ord ，并且这可以是任何其他常量集，因此我们可以启用ConstraintKinds扩展并通过Dyn特定的限制对Dyn参数化来归纳在我们的特定任务中需要：
data Dyn ctx where Dyn :: ctx a => TypeRep a -> a -> Dyn ctx toDyn :: (Typeable a, ctx a) => a -> Dyn ctx toDyn val = Dyn (typeOf val) val withDyns :: (forall a. ctx a => a -> a -> b) -> (SomeTypeRep -> SomeTypeRep -> b) -> Dyn ctx -> Dyn ctx -> b withDyns (Dyn ty1 v1) (Dyn ty2 v2) f def = case eqTypeRep ty1 ty2 of Nothing -> def (SomeTypeRep ty1) (SomeTypeRep ty2) Just HRefl -> f v1 v2
然后， Dyn Ord将成为我们的Dyn Monoid类型，例如， Dyn Monoid将允许您存储任意的monoid，并对其进行单项操作。
让我们为新的Dyn编写所需的实例：
instance Eq (Dyn Eq) where (==) = withDyns (==) (\_ _ -> False) instance Ord (Dyn Ord) where compare = withDyns compare compare
...只有这是行不通的。 打字员不知道Dyn Ord还实现了Eq ，
因此，您必须复制整个层次结构：
instance Eq (Dyn Eq) where (==) = withDyns d1 d2 (==) (\_ _ -> False) instance Eq (Dyn Ord) where (==) = withDyns d1 d2 (==) (\_ _ -> False) instance Ord (Dyn Ord) where compare = withDyns d1 d2 compare compare
好吧，现在确定。
...也许在现代的Haskell中，您可以做到这一点，以便计时器本身显示表单的实例
instance C_i (Dyn (C_1, ... C_n)) where ...
因为出现了一些逻辑上的东西，但是我还没有做到，所以我不得不坐在那里。 请继续关注。
而且，如果您仔细地quin着眼睛，您会发现我们的Dyn看起来像可疑语言中的一对依赖类型(ty : Type ** val : ty) 。 但是，仅在我所熟悉的语言中，无法匹配类型，因为参数化（在这种情况下，恕我直言，解释得太广泛了），但在这里似乎是可能的。
但是最重要的是-现在，您可以放心使用Map (Dyn Ord) SomeValue并使用任何值作为键，只要它们本身支持比较即可。 例如，带有度量描述的标识符可用作键，但这是下一篇文章的主题。