代码之家 › 专栏 › 技术社区 › Tobias Weck

DataKinds和类型类实例

data-kinds typeclass haskell

6

Tobias Weck · 技术社区 · 9 年前

下面的例子是我现实生活中问题的简化版。它似乎在某种程度上类似于 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"

但要使用 显示 -例如,我必须明确地提供上下文,即使这种类型仅限于 K :

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

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

我也可以定义一个单一的,但更一般的 显示 -实例如下:

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

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

那么,有没有办法既吃我的蛋糕又吃呢?也就是说,不必在类型 test (虽然种类注释很好),但仍然有两种不同的 show 实现(例如通过以某种方式区分类型)?

实际上,如果我可以简单地将各个类型关联起来,那么也可以删除整个类型类( A. , B )其特定值(此处: "A" , "B" )在我只有类型信息的上下文中。不过,我不知道该怎么做。

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

3 回复 | 直到 7 年前

1

6

kosmikus 9 年前

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

我不知道全貌,但可以通过将类字典或字符串本身与传递的值显式绑定来解决这个问题。。。

2

5

dfeuer 9 年前

您可以添加其他类。

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

3

2

Ben 9 年前

知道:

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

足以证明 Show (Proxy a) 持有。但类型类不仅仅是我们需要证明与类型一起使用的命题,它还提供了实现。实际使用 show (x :: Proxy a) 我们不仅需要证明 显示(代理a) 存在 ,我们需要知道是哪一个。

Haskell类型变量(无约束)是参数化的:在 一 ,还能够检查 一 提供不同的行为 A. 和 B 。您想要的“不同行为”是尽可能“接近参数化”,因为它只是为每种类型选择不同的实例,而您知道每种类型都有一个实例。但这仍然是违反合同的东西 test :: forall (a :: K). Proxy a -> String 方法

类型类约束允许您的代码在受约束的类型变量中是非参数的,尽可能使用类型类从类型到实现的映射来根据代码调用的类型切换代码的行为。所以 test :: forall (a :: K). Show (Proxy a) => Proxy a -> String 作品(就实际实现而言,选择类型的最终调用者 一 还提供了 显示(代理a) 从函数生成的代码的实例)。

您可以使用 instance Show (Proxy (a :: K)) 主意现在你的函数是类型中的参数化 a :: K 仍然可以使用 show(x::代理a) 因为有一个实例适用于所有人 a::K 但实例本身也遇到了同样的问题;实施 show 在实例中是参数化的 一 ,因此无论如何都不能检查它,以便根据类型返回不同的字符串。

您可以使用类似dfeuer的答案,其中 Kish 利用受约束类型变量的非参数性,基本上允许您在运行时检查类型;传递的实例字典满足 Kish a 约束基本上是为变量选择的类型的运行时记录 一 (以迂回的方式)。进一步推动这个想法会让你 Typeable 。但仍需要某种约束才能使代码在 一 .

您还可以使用一个类型,该类型是 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 非参数化 一 基本上与 基什 约束,但避免了向类型签名添加额外约束的需要。在这篇文章的早期版本中,我指出 测验 能够做到这一点,同时保持“仅”参数化 一 ,这是不正确的。

当然,现在要传递代理,您必须实际编写 KA 或 KB 你要写的地方一点都不麻烦 Proxy :: Proxy A 实际选择类型(这通常是代理的情况,因为您通常只使用它们来修复一个否则会不明确的类型)。但是,如果你与调用的其他部分不一致,编译器会抓住你,但你不能只写一个像这样的符号 代理 并让编译器推断正确的含义。您可以寻址那个具有类型类:

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

instance KProxyable A
  where kproxy = KA

instance KProxyable B
  where kproxy = KB

然后你可以使用 灵魂 而不是 代理::代理A 和 kproxy 而不是让编译器推断裸机的类型 代理 .愚蠢的示例时间:

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

GHCI:

Î» foo KA kproxy
"KA KA"

注意,我实际上不需要 KProxyable 任何地方的约束;我使用 kproxy公司 在类型是已知。这仍然必须“从顶部进入”,尽管(正如实例字典满足您的 显示(代理a) 约束将);无法在类型中使用参数化函数 a::K 提出相关的 KProxy a 它自己。

因为这是构造函数和类型之间的对应关系,所以我不相信您可以像在运行时使用空的那样以这种方式创建通用代理 代理 TemplateHaskell当然可以为您生成这样的代理类型;我认为 单身者 这里的大意是什么 https://hackage.haskell.org/package/singletons 可能提供了您需要的内容,但我不太熟悉如何实际使用该包。