问题标签 [gadt]

我想为 Data.Map 创建一个特殊的智能构造函数，对键/值对关系的类型有一定的约束。这是我试图表达的约束：

对于每个字段，只有一种类型的值应该与之关联。就我而言，将Speed字段映射到ByteString. 一个Speed字段应该唯一地映射到一个Float

但我收到以下类型错误：

使用-XKindSignatures：

我明白为什么我会得到 Kind 不匹配，但是我该如何表达这个约束，以便toPair在不匹配的Field和Value.

#haskell 建议我使用 a GADT，但我还没有弄清楚。

这样做的目标是能够写

这样我就可以Map在尊重键/值不变量的地方制作安全的 s。

所以这应该类型检查

但这应该是编译时错误

编辑：

我开始认为我的具体要求是不可能的。使用我原来的例子

为了在Fooand上强制执行约束，必须有某种方法在类型级别Bar区分 a FooIntand并且类似地 for 。因此我需要两个 GADTFooFloatBar

现在我可以编写一个实例Pair，仅当Foo和Bar都被标记为相同类型时才成立

我有我想要的属性

但我失去了写作的能力，xs = [FooInt, FooFloat]因为那需要一个异构的列表。此外，如果我尝试使用Map同义词type FooBar = Map (Foo ?) (Bar ?)，我会坚持使用Map只有Int类型或只有Float类型，这不是我想要的。它看起来相当绝望，除非有一些我不知道的强大的类型类魔法。

假设我有以下 GADT：

我现在想要一个像这样工作的函数：

我将如何构建这样的功能？

我尝试了不同的绑定类型的方法，但没有成功。是否有我缺少的扩展可以实现更广泛的类型绑定？

这是错误消息：

我想要完成的描述：我想设计一个 DSL 和一个函数运行，它可以尝试以几种不同的方式运行 DSL 的一些代码（每种方式我有多个不同的运行函数）。run 函数将尝试运行尽可能多的代码，然后报告它不能运行的代码以及它可以运行的代码的结果是什么。

以下程序类型检查和编译：

但是，当我尝试为 添加案例时eval (Branch m)，请键入检查炸弹。某种类型的东西

是预期的，但当然我的方式是

有人对如何写作有建议eval (Branch m)吗？

编辑我

作为对@sabauma 评论的回应，我认为 for 的类型签名eval将不得不改变，但我不确定它应该是什么。

编辑二

这是应该发生的事情的示例：

应该给，

这就是@sabauma 的提议所做的。

假设我有以下 GADT AST：

现在我想构造一个函数来替换树中所有L类型的（屋檐） ，如下所示：a

有可能构建这样的功能吗？（可能使用类？）如果对 GADT 进行更改，是否可以完成？

我已经有一个 typeof 函数：typeof :: a -> Type在一个类中。

GADT 是何时在 GHC 中引入的？（版本+日期）

此外，它们是否仍被视为语言扩展，或者它们现在是否是 Haskell 标准的一部分？

在 Haskell 中，为递归树创建数据类型很简单，就像我们在 XML 文档中所拥有的那样：

及其相关的折叠：

我现在的问题是我不知道如何为我的树数据类型添加一些额外的限制以对 HTML 进行建模。在 HTML 中，每个元素节点只能出现在正确的上下文中，并且每个元素对应于其子元素的不同上下文。例如：

• 像img这样的void 元素有一个空的上下文模型，并且不允许有任何子元素。
• 具有 Text 内容模型的元素，例如title，只能将文本节点作为子节点（不允许嵌套标签）
• div元素不能出现在 Phrasing 上下文中，因此不允许作为span元素的后代。

所以我的问题是：

1. 在 Haskell98 中我需要做什么来模拟这些限制？（我问这个是因为我猜 Haskell98 模型应该更好地翻译成其他编程语言）

   我想我们可能必须为不同的上下文创建许多不同的数据类型，但我不知道如何以有原则和清晰的方式做到这一点。我怎样才能在不迷路的情况下做到这一点，折叠功能最终会是什么样子？

2. 如果允许我们使用现代 GHC 功能（例如 GADT），模型会是什么样子？

   我有一种预感 GADT 可能有助于将限制推入类型检查器，保持折叠功能简单，但我对它们没有太多经验......

我不需要 100% 有效的解决方案，因为这显然超出了 Stack Overflow 讨论的范围。我只需要能够更好地掌握 GADT 之类的东西，并且能够自己完成剩下的工作。

假设我有以下代码：

然后，以下实例声明有效，对没有约束t：

并做我期望它做的事情。

但是下面的实例声明不起作用：

由于 GHC - 我正在使用 7.6.1 - 抱怨说：

当然，添加Typeable t到上下文中是可行的。但是添加以下实例也是如此：

有没有办法让 GHC 为我编写后一个实例？如果是这样，怎么做？如果不是，为什么不呢？

我希望 GHC 能够Typeable从构造函数的上下文中提取约束Wrap，就像它对Eq约束所做的那样。我认为我的问题归结为 GHC 明确禁止写作deriving instance Typeable (Wrapper t)，并且标准(Typeable1 s, Typeable a) => Typeable (s a)实例无法“查看内部”s a来查找Typeable a字典。

我们能否将没有给定构造函数约束的 GADT 转换为具有上述约束的 GADT？我想这样做是因为我想深度嵌入 Arrows 并用（目前）似乎需要的表示做一些有趣的事情Typeable。（一个原因）

我们可以尝试以下from函数，但由于我们没有 Typeable递归点的信息，所以很快就会中断

因此，我们尝试在类型类中捕获转换。然而，这将被打破，因为我们将失去存在主义的Typeable b信息。b

还有其他建议吗？最终，我想创建一个深度嵌入Category并与类型参数信息Arrow一起。Typeable这样我就可以使用箭头语法在我的 DSL 中构造一个值，并拥有相当标准的 Haskell 代码。也许我必须求助于 Template Haskell？

我正在为我正在做的一个小实验测试一些代码，但一开始我遇到了一个我不知道如何解决的障碍。

好的，这是一些测试代码，驱动程序函数会比这复杂得多，但即使在这个测试中，我也会收到错误“约束中的歧义类型变量‘a0’：（字段 a0）由使用 `fieldName 引起'。所以编译器确实看到 fieldName 被应用于一个字段，但显然它在这里需要一个更具体的类型。我想让函数保持多态会使 pgsqlDriver 不是一个具体的类？

但想法是这些函数是多态的。这就是我在这里选择使用 GADT 的原因，因此我可以对这些驱动程序函数的参数进行类型约束，而不必在每次实例化中重复它们。计划是定义的数据库驱动程序可以与任何 Field 和 Table 实例一起使用。这不能简单地完成，我的 DatabaseDriver 类型也必须是一个类型类吗？

假设我有以下（错误的）代码。

然后 GHC 会给我这个错误：

这个错误信息不是完全错误的吗？该错误与 AApply 无关。