DataKinds和类型实例

Question

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

假设我们有一个有限的，晋升DataKind K与类型A和B，和聚kinded Proxy数据类型，产生与各类样的条件*。

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

data K = A | B 

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

现在我想写Show -instances对每种类型Proxy a其中a是样K，这是完全二：

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

但使用Show -instance，我要明确提供上下文，即使该种类仅限于K：

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

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

我还可以定义一个单一的，但更普遍的Show -instance这样的：

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

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

那么，有没有办法吃我的蛋糕，也有吗？也就是说，不必提供类型为test的类型约束（种类注释很好，但是），并且仍然有两个不同的show实现（例如通过区分类型）？

其实，这也将是好放弃整个类型的类，如果我可以简单地在各自的类型（A，B）与他们的特定值（在这里："A"，"B"）相关联的情况下，我只是有类型信息。不过，我不知道该怎么做。

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

Answer 1

不，这是不可能的。在具有“只是类型信息”的上下文中，在运行时，您确实有没有信息。类型信息被删除。因此，即使对于封闭类型，原则上可以显示给定类型的问题，您仍然可以创建一个字典，但仍需要类限制。类约束确保在编译时，当GHC知道类型时，它可以选择合适的实例传递。在运行时，输入它的信息会丢失，并且没有机会这样做。编写一个“一刀切”的实例确实有效，因为那样确切的类型对于选择就不重要了。

不知全貌，但它可能可以解决此通过明确捆绑起来或者类字典或字符串本身与要绕过值...

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，您可以根据需要检查而不是使用代理。

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)的实现存在，我们需要真正知道它是哪一个。

哈斯克尔类型变量（没有限制）的参数：有没有办法得到充分多态性在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为非-p参数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可能提供您需要的东西，但我并不十分熟悉如何真正使用该软件包。