问题标签 [gadt]

您能否告诉我 Enum 类的 Haskell 派生机制是否有任何扩展？我的意思是除了“空构造函数”之外还有很多合理的情况。有没有关于这个主题的作品？

考虑以下代码：

尽管fun是一个详尽的匹配项，但在使用 -Wall 编译时，GHC 会抱怨缺少案例。但是，如果我添加另一个构造函数：

然后 GHC 正确地检测到乐趣是全部的。

我在我的工作中使用了与此类似的代码，并且希望 GHC 在我错过案例时发出警告，如果我没有，则不发出警告。为什么 GHC 抱怨第一个程序，我怎样才能在不添加虚假构造函数或案例的情况下编译第一个示例而不发出警告？

我正在开发一个包含这些数据类型定义的 haskell 程序：

和数据公式 ts where

还有一个 eval 函数，它将每个 Term t 评估为：

以下检查公式是否可满足任何可能的值替换的函数：

现在，我被要求编写一个求解给定公式的求解函数：

另外，我有以下公式作为测试示例，期望我的解决方案表现得像这样：

解决方案函数应返回：

到目前为止，我的这个函数的代码是：

辅助功能是：

最后，这是我的问题：使用此解决方案函数，我可以毫无问题地解决类似于 ex1 和 ex2 的公式，但问题是我无法解决 ex3 。这意味着我的函数不适用于包含嵌套的公式“福罗尔”。任何有关如何执行此操作的帮助，将不胜感激，在此先感谢。

Test.test 中的错误似乎不合理：

有几种方法可以使错误更改或消失：

如果我们删除特征 A（和案例类 B）上的 V 参数，错误的“GADT-skolem”部分就会消失，但“构造函数无法实例化”部分仍然存在。

如果我们将 Test 类的 U 参数移到 Test.test 方法中，错误就会消失。为什么 ？（同样，Test2.test2 中不存在该错误）

以下链接也确定了该问题，但我不理解提供的解释。http://lambdalog.seanseefried.com/tags/GADTs.html

这是编译器中的错误吗？(2.10.2-RC2)

感谢您为澄清这一点提供的任何帮助。

2014/08/05：我设法进一步简化了代码，并提供了另一个示例，其中 U 绑定在立即函数之外而不会导致编译错误。我仍然在 2.11.2 中观察到这个错误。

像这样简化，这看起来更像是编译器错误或限制。还是我错过了什么？

我最近了解了一点 F 代数： https ://www.fpcomplete.com/user/bartosz/understanding-algebras 。我想将此功能提升到更高级的类型（索引和更高级别）。此外，我检查了“给 Haskell 一个提升”（http://research.microsoft.com/en-us/people/dimitris/fc-kind-poly.pdf），这很有帮助，因为它给了我自己模糊的名字“发明”。

但是，我似乎无法创建适用于所有形状的统一方法。

代数需要一些“载体类型”，但我们正在遍历的结构需要某种形状（本身，递归应用），所以我想出了一个可以携带任何类型的“虚拟”容器，但形状符合预期。然后我使用一个类型族来耦合这些。

这种方法似乎有效，为我的“cata”函数带来了一个相当通用的签名。

然而，我使用的其他东西（Mu，Algebra）仍然需要为每个形状单独的版本，只是为了传递一堆类型变量。我希望像 PolyKinds 这样的东西可以提供帮助（我成功地使用它来塑造虚拟类型），但它似乎只是为了反过来工作。

由于 IFunctor1 和 IFunctor2 没有额外的变量，我试图通过附加（通过类型族）索引保留函数类型来统一它们，但由于存在量化，这似乎是不允许的，所以我在那里留下了多个版本也。

有没有办法统一这两种情况？我是否忽略了一些技巧，或者这只是目前的限制？还有其他可以简化的事情吗？

以及 2 个可使用的示例结构：

ExprF1 似乎是一个正常有用的东西，将嵌入式类型附加到对象语言。

ExprF2 是人为设计的（恰好也被提升的额外参数（DataKinds）），只是为了找出“通用” cata2 是否能够处理这些形状。

输出：

这似乎是一件合理的事情，但我遇到了类型问题。我想要一个Client可以向 a 发送选项列表的 a Server，它将选择一个并返回所选元素。所以是这样的：

这个想法是服务器可以a -> String在列表的每个元素上调用该函数以将它们显示给用户。只要列表和函数匹配，我希望能够改变 a。

这样的事情可能吗？也许我想要的约束可以以某种方式编码到 GADT 中？

我希望一些 Haskell 专家可以帮助澄清一些事情。

是否可以以Nat通常的方式定义（通过 Haskell 中的@dorcard Singleton 类型）

（或其一些变体），然后定义一个LessThan关系，使得 foralln和m

然后编写一个类型如下的函数：

我明确地想在输出类型中使用“LessThan” foo，我意识到人们当然可以写出类似的东西

但这不是我所追求的。

谢谢！

兰吉特。

在讨论VoidHaskell Libraries 邮件列表时，有这样的评论：

回到过去，它曾经是由unsafeCoerceConor McBride 的要求实现的，他不想为遍历整个Functor 内容和替换其内容而付费，而类型告诉我们它不应该有任何内容。如果应用于适当的 Functor，这是正确的，但在 GADT 存在的情况下是可颠覆的。

的文档unsafeVacuous还说：

IfVoid是无人居住的，比任何Functor只持有该类型值的人Void都不持有任何值。

这仅对不对参数执行类似 GADT 分析的有效函子是安全的。

这样一个恶作剧的 GADTFunctor实例会是什么样子？（当然只使用总函数，不使用undefined等error）

理解我在问什么需要以下定义：

我想使用这些定义编写一个函数，其工作方式如下：

在哪里

和

基本思想是接受不同形状的输入并根据用于 S 的构造函数和构建 R 时选择的参数产生不同形状的输出。我一直在尝试使用具有数据类型的类来做到这一点，但我得到了种类不匹配错误。我想知道是否有一种直观、干净的方式来编码这种类型的东西。

我目前的尝试如下：

这种方法抱怨 R 的第一个参数应该有 kind Param 但 Param 有 kind *，我不知道如何纠正这个问题。添加约束并使用变量时，我到了这里：

当然，Haskell 拒绝让我使用 Kind 作为约束。我很迷茫，我不知道该去哪里。任何帮助或指导都是无价的。

我为表达式创建了一个 GADT。当我对具有约束的构造函数进行模式匹配时，类型检查器无法推断构造函数约束中使用的类型变量的约束。我认为代码和错误消息更清楚。

我得到的错误：

编辑：如果我注释掉Show (Expr a)实例并添加以下代码，它工作正常：

我希望显示实例基本上打印类似Cast (Value bigvalue).