问题标签 [gadt]

我正在尝试使用可组合的逻辑创建复杂的数据结构。也就是说，数据结构具有通用格式（本质上是具有某些类型可以更改的字段的记录）和一些通用功能。特定结构具有通用功能的特定实现。

我尝试了两种方法。一种是使用类型系统（使用类型类、类型族、功能依赖等）。另一个是创建我自己的“vtable”并使用 GADT。两种方法都以类似的方式失败 - 我在这里似乎缺少一些基本的东西。或者，也许，有更好的 Haskell-ish 方式来做到这一点？

这是失败的“键入”代码：

它会导致以下错误：

这是失败的“vtable”代码：

它会导致以下错误：

当整个事情明确地在 ScopedTypeVariables 和“forall 块”下时，我不明白为什么 GHC 会选择“block1”。

编辑 #1：添加功能依赖项，感谢 Chris Kuklewicz 指出这一点。但问题仍然存在。

编辑#2：正如克里斯指出的那样，在 VTable 解决方案中，摆脱所有“块〜块状态端口”，而不是在任何地方写“块状态端口”可以解决问题。

编辑#3：好的，所以问题似乎是对于每个单独的函数，GHC 需要参数中有足够的类型信息来推断所有类型，即使对于根本不使用的类型也是如此。所以在（例如）上面的 logicState 的情况下，参数只给我们状态，这不足以知道端口和传入和传出类型是什么。没关系，这对 logicState 函数并不重要；GHC 想知道，不能，所以编译失败。如果这确实是核心原因，那么如果 GHC 在编译 logicState 声明时直接抱怨会更好——它似乎有足够的信息来检测那里的问题；如果我在该位置看到“未使用/确定端口类型”的问题，那会更清楚。

编辑#4：我仍然不清楚为什么 (block ~ Block state ports) 不起作用；我想我将它用于意外目的？似乎它应该起作用了。我同意 Chris 的观点，即使用 CPP 来解决它是可憎的。但是写“B trp e”（在我有更多参数的真实代码中）也不是一个好的解决方案。

现在，假设有人建了一Foo棵树，我想检查 Foo 值的参数是否有效。构造函数参数的规则是：

• Bar2 Bar1 Foo
• Bar3 (Bar2|Bar3|Bar4)
• Bar4 Bar1 Bar1 (Bar1|Bar4)

我知道值的构造函数，只想检查直接参数，没有递归。像这样：

例如，对于 Bar4 类似：

我怎样才能最简洁地表达这些条件？在某些情况下，列出所有组合有点过多。据我所知，不存在用于模式匹配的“OR”语法。

更新

我改编了丹尼尔的解决方案并得出了这个结论：

我喜欢这个的原因是我不必更改我的数据类型，除了添加派生子句，而且它是可读的。当然，缺点是这些是动态检查。就我而言，这很好，因为它只是用于类似断言的检查以发现编程错误。

我正在尝试实现类型安全的二项式堆。为此，我有两种数据类型，它们的元素类型由它们的类型编码索引参数化：

Vec使用递减的数字参数对值进行编码，其中最后一个元素始终由 参数化Zero。RVec使用增加的数字参数对值进行编码，没有其他限制（这就是为什么RNil可以产生RVec任何数字的原因）。

这允许我（例如）拥有一个高度增加/减少的树木列表，由类型系统检查。在实现了我的大部分项目之后，我意识到我需要一个看似简单的函数，但我无法实现：

它应该简单地颠倒给定列表的顺序。有任何想法吗？提前致谢。

I have found that I really like combining GADTs with Data Kinds, as it gives me further type safety than before (for most uses, almost as good as Coq, Agda et al.). Sadly, pattern matching fails on the simplest of examples, and I could think of no way to write my functions except for type classes.

Here's an example to explain my sorrow:

We have 2 type classes (one for the theorem, one for a utility operation) and 5 instances - just for a trivial theorem. Ideally, Haskell could look at this function:

And type-check each clause on its own, and per-call decide which cases are possible (thus worth trying to match) and which are not, so when calling trans Le_base Le_base Haskell will notice that only the first case allows for the three variables to be the same, and only attempt matching on the first clause.

我有以下 GADT

使用类对固定长度向量进行建模

我试图在向量上编写一个附加函数：

类型检查器不喜欢它：

谁能解释类型变量的 GHC 问题nm？~错误消息中的确切含义是什么？

有时我遇到需要返回存在量化类型的值。当我使用幻像类型（例如表示平衡树的深度）时，这种情况最常发生。AFAIK GHC 没有任何exists量词。它只允许存在量化的数据类型（直接或使用 GADT）。

举个例子，我想有这样的功能：

到目前为止，我有 2 个可能的解决方案作为答案添加，我很高兴知道是否有人知道更好或不同的东西。

在Haskell 中的 Type-Safe Observable Sharing 中， Andy Gill 展示了如何在 DSL 中恢复存在于 Haskell 级别的共享。他的解决方案是在data-reify 包中实现的。可以修改此方法以与 GADT 一起使用吗？例如，给定这个 GADT：

我想通过将上述 AST 转换为

通过函数

（我不确定 的类型recoverSharing。）

请注意，我不关心通过 let 构造引入新绑定，而只关心恢复存在于 Haskell 级别上的共享。这就是为什么我recoverSharing返回一个Map.

如果它不能作为可重复使用的包完成，至少可以为特定的 GADT 完成吗？

在这段代码中有重复的片段：

所以很想写一个函数：

并在任何地方使用它，例如：

有没有办法写insert2？天真的方法不进行类型检查。

我有一个 GADT，它只与两个不同的参数 ForwardPossible 和 () 一起使用：

我想派生足够的 Data.Data 实例来涵盖 OrForward t () 和 OrForward t ForwardPossible。我认为一般 (Data t, Data forward) => OrForward t forward 实例是不可能的，除非它普遍忽略 OFForward，但是 Data t => OrForward t ForwardPossible 和 (Data t, Data forward) => 的重叠实例如果有办法让 ghc 派生这些实例，OrForward t 前向实例可能是一个解决方案。

我试过定义：

但随后 ghc 给了我一个这样的错误：

我正在尝试在 Haskell 中实现组合逻辑，并且我想为该语言编写解析器。我无法让解析器通过 Parsec 工作。基本问题是我需要一种方法来确保解析器返回的对象类型正确。有没有人对如何做到这一点有任何创造性的想法？