6

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

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

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

data K = A | B

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

现在我想为kindShow的每种类型编写 -instances Proxy a，它们正好是两个：aK

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 Show (Proxy (a :: K)) where show p = "?"

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

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

实际上，如果我可以在只有类型信息的上下文中简单地将各个类型（ A, B）与它们的特定值（这里："A", ）相关联，那么删除整个类型类也是可以的。"B"不过，我不知道该怎么做。

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

4

3 回答 3

6

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

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

于 2015-09-05T00:23:43.613 回答
5

您可以添加另一个类。

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

于 2015-09-05T06:58:54.377 回答
2

知道：

  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. 但是实例本身也遇到了同样的问题；in 实例的实现show是参数 in a，因此无论如何都不能检查它，以便根据类型返回不同的字符串。

您可以使用 dfeuer's answer 之类的东西，其中Kish利用约束类型变量的非参数性基本上允许您在运行时检查类型；Kish a为满足约束而传递的实例字典基本上是为变量选择了哪种类型的运行时记录a（以迂回的方式）。进一步推动这个想法会让你一路走来Typeable。但是您仍然需要某种约束来使您的代码在a.

A您还可以使用明确表示or选择的运行时表示的类型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)，我实际上可以派生它，尽管它确实需要独立派生）

这是使用 GADTKProxy来允许testin 中的非参数化a，本质上与 dfeuer 的答案中的约束执行相同的工作，Kish但避免了向类型签名添加额外约束的需要。在这篇文章的早期版本中，我说test能够做到这一点，同时保持“只是”参数a，这是不正确的。

当然，现在要传递代理，您必须实际编写KAor 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的。

因为构造函数和类型之间的对应关系使这项工作有效，所以我不相信您可以像使用 empty-at-runtime 那样制作这种风格的通用代理Proxy。TemplateHaskell 当然可以为你生成这样的代理类型；我认为单例的概念是这里的一般概念，因此https://hackage.haskell.org/package/singletons可能提供了您需要的东西，但我不太熟悉如何实际使用该包。

于 2015-09-07T03:07:03.617 回答