DataKinds和类型类实例

Question

以下示例是我现实生活中问题的简化版本。它似乎在某种程度上类似于 从DataKinds约束的存在类型中检索信息，但我无法完全获得我正在寻找的答案。

假设我们有一个有限的升级数据类型K，其中包含类型A和B，并且有一个多类型的Proxy数据类型来生成类型为*的项。

{-# LANGUAGE DataKinds, PolyKinds, GADTs, FlexibleInstances, FlexibleContexts #-}

data K = A | B

data Proxy :: k -> * where Proxy :: Proxy k

现在我想为每种类型Proxy a编写Show实例，其中a是K类型，这些实例恰好有两个。

instance Show (Proxy A) where show Proxy = "A"
instance Show (Proxy B) where show Proxy = "B"

但是要使用 Show 实例，即使类型被限制为 K，我也必须明确提供上下文：

test :: Show (Proxy a) => Proxy (a :: K) -> String
test p = show p

我的目标是去除类型类约束。这可能看起来不重要，但在我的实际应用中，这具有重大意义。

我也可以像这样定义一个单一但更通用的Show实例：

instance Show (Proxy (a :: K)) where show p = "?"

这实际上允许我删除约束条件，但新问题是区分两种类型A和B。

那么，有没有一种方法既不必在test的类型中提供类型类约束（种类注释可以），又可以有两个不同的show实现（例如通过某种方式区分类型）？

实际上，如果我能够简单地将相应的类型（A，B）与它们的特定值（这里是"A"，"B"）关联起来，在只有类型信息的情况下，也可以放弃整个类型类。我不知道如何做到这一点。

非常感谢提供任何见解。

- Tobias Weck

Answer 1

不，这是不可能的。在一个只有“类型信息”的上下文中，在运行时，你真的没有任何信息。类型信息被擦除了。因此，即使对于封闭种类，从原则上讲，可以显示出对于所讨论的类型，你总是可以提供一个字典，但你仍然需要类约束。类约束确保在编译时，当 GHC 知道类型时，它可以选择适当的实例进行传递。在运行时，丢失了哪种类型的信息，没有机会做同样的事情。编写“一刀切”实例确实是有效的，因为对于选择来说，确切的类型不再重要。

我不知道整个情况，但通过明确捆绑类字典或字符串本身与传递的值，可能是可以解决这个问题的...

- kosmikus

---

谢谢你的回答，我担心这是不可能的。我想我必须找到一个解决办法。 - Tobias Weck

Answer 2

您可以添加另一个类。

class Kish (k :: K) where
  toK :: proxy k -> K

instance Kish A where
  toK _ = A

instance Kish B where
  toK _ = B

instance Kish k => Show (Proxy k) where
  showsPrec n _ = case toK (Proxy :: Proxy k) of
    A -> ...
    B -> ...

现在你仍然需要使用上下文，但这是一个更通用的上下文，对其他事情也可能非常有用。

如果发现你需要经常区分代理，那么你应该切换到一个GADT，可以根据需要检查而不是使用代理。

- dfeuer

---

这样的东西可能会很有用，我会记在心里的，谢谢。 - Tobias Weck

Answer 3

知道以下内容：

1. a是K种类的； 2. K种类只有A和B两种类型； 3. Show（Proxy A）成立； 4. Show（Proxy B）成立；

就足以证明Show（Proxy a）成立。但是，类型类不仅是我们需要证明其为真以与我们的类型一起使用的命题，它还提供了实现。要实际使用show（x :: Proxy a），我们不仅需要证明存在一个适用于Show（Proxy a）的实现，还需要知道这个实现是哪一个。

Haskell类型变量（没有约束）是参数化的：没有办法在a中完全多态，并且能够检查a以提供不同的A和B行为。你想要的“不同行为”大约就是“接近参数化”的，因为当你知道每种类型都有一个时，它只是为每种类型选择不同的实例。但它仍然打破了test :: forall（a :: K）。Proxy a -> String的合同。

类型类约束允许您的代码在受约束的类型变量中是非参数化的，因为您可以使用类型类的从类型到实现的映射来根据调用它的类型切换代码的行为。所以test :: forall（a :: K）。Show（Proxy a）=> Proxy a -> String有效。（在实际实现方面，相同的最终调用者既可以选择类型a，也可以为从您的函数生成的代码提供Show（Proxy a）实例以供使用。）

您可以使用instance Show（Proxy（a :: K））的想法；现在，对于类型a :: K的参数化函数仍然可以使用show（x :: Proxy a），因为有一个适用于所有a :: K的实例。但是，实例本身遇到了同样的问题；实例中show的实现在a中是参数化的，因此无法以任何方式检查它以根据类型返回不同的字符串。

您可以使用类似于dfeuer的答案，其中Kish利用约束类型变量的非参数性，基本上允许您在运行时检查类型; 传递给满足Kish a约束的实例字典基本上是关于哪种类型被选择为变量a（以迂回的方式）的运行时记录。将这个想法推得更远，就可以到达Typeable。但是，您仍然需要某种约束来使您的代码对a不具有参数性。

您还可以使用一个显式的运行时表示A或B选择的类型（与Proxy相反，在运行时是一个空值，并且仅提供编译时选择的表示），例如：

{-# LANGUAGE DataKinds, GADTs, KindSignatures, StandaloneDeriving #-}

data K = A | B

data KProxy (a :: K)
  where KA :: KProxy A
        KB :: KProxy B

deriving instance Show (KProxy a)

test :: KProxy a -> String
test = show

（注意，我不仅可以实现Show（Kproxy a），而且实际上可以导出它，尽管这确实需要独立的导出）

这里使用GADT KProxy，允许test在a中是非参数化的，从本质上说与dfeuer答案中的Kish约束执行相同的工作，但避免了在类型签名中添加额外的约束的需要。在此贴子的早期版本中，我声明test能够保持“只”对a进行参数化而完成此操作，但这是不正确的。

当然，现在要传递代理，您必须实际编写KA或KB。如果您需要编写Proxy :: Proxy A来选择类型（通常情况下，鉴于您通常只使用代理来修复原本可能会产生歧义的类型），那么这没有问题。但在编译器会抓住您是否与调用的其余部分不一致的情况下，如果本来就不会产生歧义，则无法仅编写一个符号（如Proxy）并使编译器推断正确的含义。您可以通过类型类解决这个问题：

class KProxyable (a :: K)
  where kproxy :: KProxy a

instance KProxyable A
  where kproxy = KA

instance KProxyable B
  where kproxy = KB

那么你可以使用 KA 替代 Proxy :: Proxy A，并使用 kproxy 代替让编译器推断裸的 Proxy 的类型。下面是一个简单的示例:

foo :: KProxy a -> KProxy a -> String
foo kx ky = show kx ++ " " ++ show ky

GHCI:

λ foo KA kproxy
"KA KA"

请注意，实际上我不需要在任何地方使用 KProxyable 约束; 我在类型已知的情况下在某个点使用kproxy。 不过这仍然必须从上层传递进来(就像满足您的Show(Proxy a)约束的实例字典一样);没有办法让一个泛型函数参数化一个类型a :: K 并自己产生相关的KProxy a。

因为构造函数与类型之间的对应关系使此方法可行，所以我认为你无法像使用运行时空的Proxy那样使用此样式创建通用代理。虽然TemplateHaskell可以为您生成这样的代理类型;我认为单例的概念是这里的基本思想，因此https://hackage.haskell.org/package/singletons可能提供了您需要的内容, 但我并不熟悉如何实际使用该软件包。

- Ben

---

foo 无法通过模式匹配学习 a 吗？这样的信息通常可以在 GADT 模式匹配的 RHS 上获得。此外，KProxy 可能是一个不好的名称，因为它在 Data.Proxy 中使用。 - dfeuer

@dfeuer 你说得很对，foo 可以通过在 kx 上进行模式匹配来了解 ky 的类型... 所以 GADTs 打破了参数性？ - Ben

@dfeuer 我当然认为他们会，这就是很多观点的关键。听起来像是心智模型在更新 - Ben

这就是为什么据我所知，Agda区分“参数”和“索引”的原因。这也与GHC的有些混乱/受限的“类型角色”机制有关。 - dfeuer