问题标签 [data-kinds]

给定一个 ADT

该DataKinds扩展允许我们将其提升为种类和类型/类型构造函数

有没有办法向K类型构造函数添加一个构造函数

?

如何定义对 kind 类型的新计算GHC.TypeLits.Nat？我希望能够定义一个类型族

这样WIDTH 0 ~ 0和WIDTH (n+1) ~ log2 n

我有一个宇宙类型和一个工人类型。工人可以改变宇宙。我想要实现的是确保宇宙只能由来自该宇宙的工人修改（而不是将来或​​过去）。

我能做到的最好的是：

如果我更改w2 = head $ _allWorkers u2为，w2 = head $ _allWorkers u我会收到我想要的编译错误。

我不太喜欢的是现在我有一个附加到每个宇宙的版本，我必须手动增加它。这可以以不需要显式版本控制的另一种方式完成吗？类似于让doSomething函数返回Universe otherType类型检查器知道otherType的与 . 不同的地方t。

谢谢你的时间。

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

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

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

但要使用Show-instance，我必须明确提供上下文，即使类型仅限于K：

我的目标是摆脱类型类约束。这似乎并不重要，但在我的实际应用中，这具有重大意义。

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

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

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

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

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

首先简要概述我的一般问题然后显示我卡在哪里可能更容易。

我想接收一些单例索引类型的 JSON 列表，其中索引类型也具有关联的类型族。在代码中：

通过存在量化，我应该能够隐藏变化的索引并且仍然能够获得值（使用一些类似延续的更高级别的类型函数 - 可能有一个更好的名称）。我最终会按照以下方式运行我的程序

whereSome来自exinst包，但也在下面重新定义。在我不解析的情况下，我可以解析 JSON MyFamily mt，但我无法找到从 JSON 解析它的最佳方法。

到目前为止我所拥有的如下：

我显然需要添加一个FromJSON (MarketIndex mt)约束，但我还需要能够将它绑定到Some CompoundType我为其生成实例的那个。

简单添加一个FromJSON (MyFamily mt)约束

给出模棱两可的类型错误

我可以看到类型检查器正在谈论mt0而不是mt一个大问题，但我不知道如何哄骗它mt在约束的右侧出现类型。

（我也意识到我没有包含FromJSON (MyFamily mt)实例，但如果类型检查器无法弄清楚mt ~ mt0我认为目前并不重要）。

希望有解决办法？

我花了相当多的时间尝试不同的事情，但有很多不同的事情发生（单身，存在主义等）。我正在慢慢地让自己达到一定的熟练程度，但我只是没有足够的知识或经验来确定他们是如何（或没有）促成这个问题的。

我目前正在玩一些善良的 nats，并在尝试定义矢量数据类型的应用实例时卡住了。

我认为，一个合理的例子是，它pure 1 :: Vec 3 Int会给我一个长度为 3 的向量，所有元素的值都是 1，并且<*>运算符会将函数与值压缩在一起。

我被卡住的问题是它将是递归的，但取决于 nat 种类的值。

正如您在下面看到的，我使用了很多 pragma（我什至不知道哪些是必要的）和一些我发现的技巧（n ~ (1 + n0)和OVERLAPPINGpragma），但似乎没有一个对我有用。

问题是是否可以在 Haskell 中进行编码，如果可以，我错过了什么？

编辑：

我得到的错误是：

我对 Servant 是如何使用打字来实现它的魔力感到非常困惑。网站上的例子已经让我很困惑：

我得到“日期”、“时间”[JSON]和“tz”是类型级文字。它们是具有“成为”类型的值。好的。

我明白了，:>并且:<|>是类型运算符。好的。

我不明白这些东西在变成类型之后如何被提取回值。这样做的机制是什么？

我也不明白这种类型的第一部分如何让框架期待签名的功能IO Date，或者这种类型的第二部分如何让框架期待Timezone -> IO Time我的签名功能。这种转变是如何发生的？

那么框架如何调用一个它最初不知道类型的函数呢？

我敢肯定，这里有许多我不熟悉的 GHC 扩展和独特的功能在发挥作用，它们结合起来使这种神奇的发生。

有人可以解释这里涉及哪些功能以及它们如何协同工作吗？

我对以下会话结束时收到的错误感到困惑：

为什么会出错？

未来的实验表明：

[Int]可以 有 居住 的 价值观 所以 它 是 善良 的*, 但 它 也是 善良 的 也 有 道理[*].

更多数据点：

我只是在学习有关 ExistentialQuantification 和 GADTs 和 KindSignatures 等的一切。为此，我尝试提出一些小程序来帮助我更好地理解一切。

现在我有这个小片段（它实际上可以编译，所以你可以自己尝试，需要矢量和mtl包）并且想知道是否有可能做我想要完成的事情或指导我如何让它发挥作用

如您所见，我正在尝试在其中获取 MenuItemReferences 的向量...我做错了什么，因为目前我得到了错误：

有人可以解释错误背后的原因是什么，以及我如何处理（如果可能的话）我想要完成的事情。

我想为动态语言制作一个类型化的 AST。目前，我被困在处理收藏品上。这是一个有代表性的代码示例：

虽然我可以构建实例List足够好的实例：

我完全不确定如何在Exprfor中编码这种类型EList。我什至在正确的道路上吗？