haskell - DataKinds 和类型类实例

Question

以下示例是我现实生活中问题的简化版本。它似乎在某种程度上类似于 Retrieving information from DataKinds constrained existential types ，但我无法完全得到我正在寻找的答案。

假设我们有一个有限的、提升的 DataKind K类型 A和 B , 和多类 Proxy数据类型以生成类型为 * 的术语。

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

data K = A | B

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

现在我想写 Show -每种类型的实例 Proxy a在哪里 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" )相关联，那么删除整个类型类也是可以的我只有类型信息。不过，我不知道该怎么做。

我将非常感谢您提供的任何见解。

Answer 1

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

我不知道全貌，但是可以通过将类字典或字符串本身与您传递的值显式绑定(bind)来解决此问题...