DataKinds和类型实例 [英] DataKinds and type class instances

问题描述

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

假设我们有一个有限的，提升的DataKind K 类型 A 和 B ，以及一个多元主角代理 $ b $ $ p $ {code> { - ＃LANGUAGE DataKinds，PolyKinds，GADTs，FlexibleInstances ，FlexibleContexts＃ - }

data K = A | B

数据代理:: k - > *其中代理::代理k


现在我想写 Show -instances为每个类型代理a 其中 a 类型 K

  instance Show（Proxy A）其中show Proxy =A 
实例Show（Proxy B）show proxy =B
  

但是要使用显示 -instance，即使类型限制为 K ：

  test :: Show（Proxy a）=>代理（a :: K） - >字符串
 test p =显示p 
  

我的目标是摆脱类型类约束。这可能看起来并不重要，但在我真正的应用程序中，这有重大影响。

我也可以定义一个单一的，但更一般的 Show <
$ b $ pre code> instance Show（Proxy（a :: K））where show p =code> -instance like this：

？


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

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

实际上，如果可以的话，放弃整个类型类也是可以的只需将各自的类型（ A ， B ）与它们的特定值相关联（这里：一个，B）在我只有类型信息的上下文中。我不知道如何做到这一点。

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

解决方案

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

我不知道完整的图片，但是可以通过明确地捆绑类字典或字符串本身来解决这个问题，并且使用传递的值。

The following example is a boiled-down version of my real-life problem. It seems to be in some way similar to Retrieving information from DataKinds constrained existential types, but I could not quite get the answers I was seeking.

Suppose we have a finite, promoted DataKind K with types A and B, and a poly-kinded Proxy data-type to generate terms with types of kind *.

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

data K = A | B

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

Now I want to write Show-instances for every type Proxy a where a is of kind K, which are exactly two:

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

But to use the Show-instance, I have to explicitly provide the context, even if the kind is restricted to K:

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

My goal is to get rid of the type-class constraint. This may seem unimportant, but in my real application, this has major implications.

I could also define a single, but more general Show-instance like this:

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

This actually allows me to drop the constraint, but the new problem is to differentiate between the two types A and B.

So, is there a way to eat my cake and have it too? That is, not having to provide a type-class constraint in the type of test (kind annotations are fine, though), and still having two different show implementations (e.g. by differentiating the types somehow)?

Actually, it would also be okay to drop the entire type class, if I could simply associate the respective types (A, B) with their specific values (here: "A", "B") in a context where I just have the type information. I have no idea how to do this, though.

I would be very thankful for any provided insights.

解决方案

No, this is not possible. In a context where you have "just the type information", at run-time, you really have no information. Type information is erased. So even for closed kinds, where it is in principle possible to show that given the type in question, you can always come up with a dictionary, you still need the class constraint. The class constraint ensures that at compile time, when GHC knows the type, it can select the appropriate instance to pass along. At run-time, the information which type it is is lost, and there's no chance to do the same. Writing a "one size fits all" instance does indeed work, because then the exact type does not matter for the choice anymore.

I don't know the full picture, but it may be possible to work around this by explicitly bundling up either the class dictionary or the string itself with the value you are passing around ...

这篇关于DataKinds和类型实例的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！