问题标签 [gadt]

我试图将 mod-n 计数器表示为将间隔[0, ..., n-1]分成两部分：

使用它，定义两个关键操作很简单（为简洁起见省略了一些证明）：

当试图证明+1并且-1是逆时，问题就来了。我不断遇到需要为这些subst引入的消除器的情况，即类似

但事实证明这是（有点）在乞求问题：类型检查器不接受它，因为subst B x=x' y : B x'和y : B x......

---- 更新 2 ----

最后，他告诉我那是Exists……</p>

谢谢你们。

- - 更新 - -

好的，我们称之为Forsome

ex3: forsome x0::[False,True]. forsome x1::[0,1,2]. (x0 || (0 < x1))

（谁告诉我“什么是 forall”）：

我该怎么做？谢谢

- - 原来的 - -

假设我们有一个公式 ex3

ex3: forall x0::[False,True]. forall x1::[0,1,2]. (x0 || (0 < x1)).

起初我认为 ex3 是False，因为当x0 = False和x1 = 0公式是(False || (0 < 0)) 所以 ex3 是绝对错误的。但有人告诉我 ex3True是

"satisfiable ex3 is true because there is at least one combination from sets x0 and x1 which returns true. So as long as there is 1 valid solution in Forall, it is true."

假设这是正确的……</p>

我认为它需要检查具有相同级别的组合组，但我不知道该怎么做。确定“他们是同一组”似乎很困难。

这是我的代码：

文件：Formula.hs

文件：Solver.hs

任何建议将不胜感激。

我有以下

并且我被要求考虑以下无类型版本才能完成：

我不确定我应该为构造函数写什么。我尝试了以下方法：

此外，由于v可以是任何类型，即int等bool，是否可以将其称为以下（上）并声明v稍后的类型？

任何帮助将非常感激 ：）

编辑：更改了整个帖子以添加更多信息和清晰度（基于我对练习的理解）。

基本上，我需要帮助找出data Expr = Condition v...etc作为参考的 GADT 的构造函数。

对于我的 Haskell 主题，我有一个来自 uni 的延续练习，其中我得到了以下内容：

而且我不确定它的真正作用。它似乎是 中定义的术语的评估者Expr。有人可以向我解释一下吗？我的练习涉及我将其转换为我所做的 GADT：

现在他们要求我静态实现以下内容并使其类型安全：

因此，为了帮助我理解一些更高级的 Haskell/GHC 功能和概念，我决定采用基于 GADT 的动态类型数据实现并将其扩展为涵盖参数类型。（我为这个例子的长度道歉。）

但是，对此的编译在最后一行失败（我的行号与示例不匹配）：

按照我的阅读方式，编译器无法确定 in Inductive :: Equal a b -> Equal (f a) (f b)，a并且b对于非底部值必须相等。所以我试过Inductive :: Equal a a -> Equal (f a) (f a)了，但是在定义中也失败了matchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal a b)：

Changing the type of matchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal a b) to produce matchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal a a) doesn't work (just read it as a proposition). Neither does matchTypes :: TypeRep a -> TypeRep a -> Maybe (Equal a a) (another trivial proposition, and this as I understand it would require users of fromDynamic' to know theain theTypeRep acontained in theDynamic`).

So, I'm stumped. Any pointers on how to move forward here?

我正在努力掌握GADTs，并且我查看了GHC 手册中的GADT 示例。据我所知，可以用以下方法做同样的事情MultiParamTypeClasses：

请注意，我们有与 GHC 示例中完全相同的构造函数和完全相同的代码eval（跨实例定义传播）GADTs。

那么所有的绒毛是GADTs什么？有什么我可以做而GADTs我不能做的事情MultiParamTypeClasses吗？还是他们只是提供了一种更简洁的方式来做我可以做的事情MultiParamTypeClasses？

我在这里阅读 GADT 介绍，我发现限制程序员只创建正确类型的语法树的想法很棒，我把这个想法放到我的简单 lambda 演算解释器中，但后来我意识到我无法将字符串解析为这个语法树，因为一个解析函数需要根据输入返回不同类型的语法树。这是一个例子：

在使用 GADT 之前，我使用的是这个：

GADT 在这里有很大的优势，因为现在我不能创建像Lambda (Application ..) ...

但是使用 GADT，我无法解析字符串并创建解析树。以下是 Lambda、Ident 和 Application 表达式的解析器：

现在的问题是：

这显然是行不通的，因为每个解析器都返回不同的类型。

那么，有没有办法使用 GADT 解析字符串并创建语法树？

我想在 GHCi 不支持的平台（即 mipsel 上的 GNU/Linux）上编写一个以交互方式使用 GADT 的 Haskell 程序。问题是，可用于在 GHC 中定义 GADT 的构造，例如：

似乎不适用于拥抱。

1. GADT 真的不能在 Hugs 中定义吗？我在 Haskell 课堂上的助教说拥抱是可能的，但他似乎不确定。
2. 如果不能，是否可以使用 Hugs 支持的其他语法或语义对 GADT 进行编码，就像 GADT 可以在 ocaml 中编码一样？