DataKinds 和类型 class 个实例

Question

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

假设我们有一个有限的、提升的 DataKind K，类型为 A 和 B，以及一个多类型的 Proxy 数据类型来生成类型为 term种类 *.

{-# 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

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

我也可以定义一个单一的，但更通用的 Show-实例，如下所示：

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

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

那么，有没有办法既吃我的蛋糕又吃呢？也就是说，不必在 test 类型中提供 type-class 约束（虽然种类注释很好），并且仍然有两个不同的 show 实现（例如通过区分以某种方式输入）？

实际上，如果我可以简单地将各个类型（A、B）与其特定值（此处: "A", "B") 在我只有类型信息的上下文中。不过，我不知道该怎么做。

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

Answer 1

不，这是不可能的。在你有 "just the type information" 的情况下，在运行时间，你实际上没有信息。类型信息被删除。所以即使对于封闭类型，原则上可以证明给定所讨论的类型，你总是可以想出一个字典，你仍然需要 class 约束。 class 约束确保在编译时，当 GHC 知道类型时，它可以 select 传递适当的实例。在运行-时间，它是什么类型的信息丢失了，而且没有机会做同样的事情。编写一个 "one size fits all" 实例确实有效，因为这样一来，确切的类型对于选择就不再重要了。

我不知道全貌，但可以通过明确地将 class 字典或字符串本身与您传递的值捆绑在一起来解决这个问题...

Answer 2

您可以再添加一个 class。

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

知道：

a是种K
种类 K 的唯一类型是 A 和 B
Show (Proxy A) 持有
Show (Proxy B) 持有

足以证明Show (Proxy a)成立。但是类型 class 不仅仅是一个我们需要证明与我们的类型一起使用的命题，它还提供了实现。要实际使用 show (x :: Proxy a)，我们不仅需要证明 Show (Proxy a) 的实现存在 ，我们还需要真正知道它是哪一个。

Haskell 类型变量（无约束）是参数化的：无法在 a 中实现完全多态，也无法检查 a 为 A 和 B。您想要的 "different behaviour" 与实际上可能没有参数化的 "close to parametric" 差不多，因为当您知道每种类型都有一个实例时，它只是为每种类型选择一个不同的实例。但这仍然违反了 test :: forall (a :: K). Proxy a -> String 的含义。

类型 class 约束允许您的代码在受约束的类型变量中是非参数的，只要您可以使用类型 class' 从类型到实现的映射来切换您的代码代码的行为基于它被调用的类型。所以 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。但是实例本身运行s 陷入了同样的问题；实例中 show 的实现在 a 中是参数化的，因此无法以任何方式检查它以便 return 基于类型的不同字符串。

您可以使用类似 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 约束相同但避免需要为您的类型签名添加额外的约束。在这个 post 的早期版本中，我说 test 能够做到这一点，同时在 a 中保留 "just" 参数，这是不正确的。

当然，现在要通过代理，您必须实际编写 KA 或 KB。在您不得不编写 Proxy :: Proxy A 来实际选择类型的地方（这通常是代理的情况，因为您通常只使用它们来修复一个否则会模棱两可的类型）并不麻烦。但是无论如何，如果您与调用的其余部分不一致，编译器会抓住您，但您不能只写一个符号，如 Proxy 并让编译器推断出正确的含义。您可以使用类型 class:

来解决 that

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。不过，这仍然必须 "come in from the top"，（与满足 Show (Proxy a) 约束的实例字典完全一样）；没有办法让类型 a :: K 中的函数参数化自己提出相关的 KProxy a。

因为它是构造函数和类型之间的对应关系，所以我不相信您可以像在空运行时那样以这种方式制作通用代理Proxy。 TemplateHaskell 当然可以为您生成此类代理类型；我认为 singletons 的概念是这里的一般概念，因此 https://hackage.haskell.org/package/singletons 可能提供了你所需要的，但我不太熟悉如何实际使用该包.

DataKinds 和类型 class 个实例

DataKinds and type class instances

haskell

typeclass

data-kinds