问题标签 [data-kinds]

我在让 GHC 在一个应该很明显的地方推断出一个类型时遇到了问题。以下是演示问题的完整片段。

在中，正如我所期望的那样，我可以在不给出明确类型的情况下进行test1打印。的类型由 : 上的显式签名推断，即has type中的第一个元素。cccxHListInt

然而test2，在 中，c需要显式签名。如果我只是print $ untag c在test2，我得到

为什么 GHC 不能从给定的显式类型推断出c类型？xtest1

我有一个常见的模式，其中我有一个 kind 的类型级别列表[*]，我想将 kind 的类型构造函数应用于* -> *列表中的每个元素。例如，我想将类型更改'[Int, Double, Integer]为'[Maybe Int, Maybe Double, Maybe Integer].

这是我实现类型级别的尝试map。

这会导致错误

我尝试添加大量类型注释，但错误或多或少是相同的：GHC 甚至无法推断 HList 的第一个元素是（正常）列表。我在这里做傻事吗？有什么违法的？或者有什么办法吗？

这是上一个问题的后续：Type-level Map with DataKinds，从它收到的两个答案开始。

我的目标是采用HList任意类型并将其转换为相关/派生类型的列表

当我实际上尝试使用几种类型来执行此操作时，我遇到了一个问题。TypeMap 的 type-function " 参数必须将HList元素类型作为其最后一个参数并返回一个新类型。这有时可以正常工作：

但是如果我想在 test 的定义中切换元组的顺序呢？我的第一次尝试是定义一个类型同义词：

但是，当然，您不能部分应用 type synonyms，这肯定会奏效。有没有（其他）方法可以实现这一目标？

这是一个代表现实世界物理单元的数据类型：

和 Show 实例：

这样，我只能显示值而不显示类型（是时间还是速度或长度类型）。我想知道如何获取类型参数m，s，kg然后显示它？

完整的代码在这里。

我想在 Haskell中实现阴阳谜题。这是我的尝试（不成功）：

当查看类型时，显然callCC $ \k -> return (Cl k)给出了 a m (Cl m)，所以yin是 type Cl m。yang是一样的。所以我期望goOn yin yang给出最终类型m (Cl m)。

这个实现看起来不错，但问题是它无法编译！这是我得到的错误：

有什么想法可以解决这个问题吗？

更新

尽管我自己找到了答案，但我仍然不明白该错误消息的含义。谁能给我解释一下？我已经知道的是，在有问题的版本中，goOn c返回类似 的东西Cl m -> m (Cl m)，而不是预期的m (Cl m). 但这不是您可以从错误消息中得到的。

我最近一直在阅读vinyl，它使用了奇怪的“种类列表”类型。在阅读了一些关于种类和乙烯基的文章后，我对它们有了一些直观的理解，并且我已经能够将它们组合在一起

:i HList产量

我从中收集到'[]的是糖 for'[] *和x ': yfor (':) * x y。那个*在那里做什么？它是列表元素的那种吗？另外，这样的列表到底是什么？它是语言内置的吗？

我正在尝试找到对 DataKinds 扩展的解释，这对我来说是有意义的，因为我只阅读了 Learn You a Haskell。有没有一个标准的资源对我来说是有意义的，我所学的很少？

编辑：例如文档说

使用 -XDataKinds，GHC 自动将每个合适的数据类型提升为一种类型，并将其（值）构造函数提升为类型构造函数。以下类型

并给出了例子

产生以下种类和类型构造函数：

我不明白这一点。虽然我不明白什么BOX意思，但这些陈述似乎说明了 ZeZe :: Nat和Su :: Nat -> NatSu 是正常的数据构造函数的情况，正如您期望在 ghci 中看到的那样

谁能解释或猜测GHC 用户指南第 7.9.2 节中讨论的数据类型提升限制背后的动机？

以下限制适用于促销：

• 我们只推广类型为 的数据类型* -> ... -> * -> *。特别是，我们不推广更高种类的数据类型，例如data Fix f = In (f (Fix f))，或种类涉及提升类型的数据类型，例如Vec :: * -> Nat -> *.

特别是，我对有关提升类型的最后一点感兴趣，例如Vec :: * -> Nat -> *. 推广一些这样的类型似乎很自然。在尝试将我的一个库转换为对各种幻像类型使用特定的提升类型而不是对所有内容使用类型时，我很快就遇到了它*，以提供更好的文档等。

通常，像这样的编译器限制的原因会在你稍微思考一下的情况下跳出来，但我没有看到这个。所以我想知道它是否属于“还不需要，所以我们没有构建它”或“那是不可能/不可判定/破坏推理”的类别。

Here is the code where I'm having an issue:

So I want to extend Tup to be defined over arbitrarily many arguments, same with sum. But a formulation involving lists would constrain the the final Term to one type of a:

I could just get rid of the a and do something like:

But then I lose the very things I'm trying to express.

So how do I express some polymorphic Term without loss of expressiveness?

有什么方法可以创建仅在一种特定类型中唯一的主键（假设我在这里问了正确的问题！-如果没有，请道歉）我注意到有一个“IdentityType.APPLICATION”选项，但“应用程序”似乎是“最小”的可用选项！！

我有以下内容：

但是当我创建一个新条目时，ID 在我的应用程序中的所有项目中都是唯一的，因此联系人、管理员、约会、服务等都是单独的“表”（或种类？），所以可以彼此都是唯一的，但是审计跟踪可以有自己的计数空间，这样它就不会干扰我的“实际数据”的计数

我是否以正确的方式问这个问题，我真的试图弄清楚这个实体/种类/属性/关键的东西，但我不确定我是否完全理解这一切实际上是如何运作的！