问题标签 [gadt]

您如何使用 GADT 在 OCaml 中定义一个简单的类似于 lambda 演算的 DSL？具体来说，我无法弄清楚如何正确定义类型检查器以从无类型的 AST 转换为有类型的 AST，也无法确定上下文和环境的正确类型。

这是使用 OCaml 中的传统方法的类似 lambda 演算的简单语言的一些代码

现在，我正在尝试将其转化为使用 GADT 的东西。这是我的开始

这就是问题所在。首先，我不确定如何在类型 texp 中为 TLam 和 TVar 定义正确的类型。通常，我会为类型提供变量名，但我不确定如何在这种情况下执行此操作。其次，我不知道函数类型检查中上下文的正确类型。以前，我使用某种列表，但现在我确定列表的类型。第三，在省略上下文之后，类型检查函数本身不会进行类型检查。它失败并显示消息

这是完全有道理的。这更像是一个我不确定类型检查的正确类型应该是什么的问题。

无论如何，您如何修复这些功能？

编辑 1

这是上下文或环境的可能类型

编辑 2

环境的诀窍是确保环境的类型嵌入到表达式的类型中。否则，没有足够的信息来确保内容的类型安全。这是一个完整的解释器。目前，我没有一个有效的类型检查器来从无类型表达式移动到有类型表达式。

那么，我们有

假设我有一些 ADT，比如

现在说我想强加某种额外的类型安全，摆脱“幻数类型”：

由于b只是构造函数中的一个幻像参数，没有约束或其他任何东西，因此它基本上没有意义——除了类型检查器。因此，它可以编译成与 相同的Foo，而没有任何性能等成本吗？

这可以按预期工作...直到您取消注释asFunction!的第二个子句 这实际上只是其他两种模式已经匹配的特殊情况的内联版本，所以我希望它没问题。但是 ( ghc-7.6.2, 或者也ghc-7.4.1)

为什么会发生这种情况，为什么不在其他条款中？在更复杂的应用程序中究竟应该做些什么来防止这种麻烦？

我有以下代码，我希望这不能通过类型检查：

这个想法是 GADT 中的每个条目都有一个相关的错误，我正在用一个Prism更大的结构对其进行建模。当我“解释”这个 GADT 时，我提供了一个具体类型，e它包含所有这些Prisms 的实例。但是，对于每个单独的情况，我不希望能够使用未在构造函数的关联上下文中声明的实例。

上面的代码应该是一个错误，因为当我进行模式匹配时，Two我应该知道我只能使用Increment e，但我正在使用Greet. 我可以看到为什么这有效 -Either String Int有一个实例Greet，所以一切都检查出来了。

我不确定解决此问题的最佳方法是什么。也许我可以使用来自 的蕴涵Data.Constraint，或者也许有更高等级类型的技巧。

有任何想法吗？

为什么用数据类型构建值更难，而与它们进行模式匹配却相对容易？

我正在尝试构建一种数据类型来控制类似于列表的结构，不同之处在于我们可能会向元素添加箭头。此外，我要求某些函数仅在向上箭头和向下箭头的数量正好等于 1 的列表上运行。

在上面的代码中，函数listToChain编译失败，而chainToList编译正常。我们如何修复listToChain代码？

当我尝试以proc语法模式匹配 GADT 时（使用 Netwire 和 Vinyl）：

我从 ghc-7.6.3 得到（相当奇怪的）编译器错误

当我将模式放入模式中时，我得到了类似的错误proc (...)。为什么是这样？它是不健全的，还是只是未实现？

我无法让 GHC 注意到箭头表达式中的两种类型相等。

完整的错误是：

为什么它不能告诉它as已经有类型PolyList as？

编辑：这最终还是有点没用，因为修复似乎触发了ghc #344，但仍未解决。最好知道问题出在哪里。

我在 ghc 7.8.2 上玩 GADT 和明确的 forall。让我们看下面这个简单的例子：

这里 ghc 失败了：

何时T2注释掉类型检查成功。但是T1和T2似乎是等价的。这是 ghc 中的错误还是 GADT 的某些限制？如果是后者，那么两者有什么区别？

我一直在尝试使用 Data.Singletons 库的依赖类型程序，在论文“使用 Singletons 的依赖类型编程”中开发了长度注释向量之后，我遇到了以下问题。

这段代码，不包括 function 的定义indexI，在 GHC 7.6.3 中进行类型检查，并在没有它的情况下按预期工作：

包含 后indexI，GHC 产生两个错误，

和，

任何一个错误的根源似乎是该术语withSing index具有类型FlipList a b n -> BiPreMap a b a0，并且无法推断a0 ~ m，GHC 无法证明BiPreMap a b m ~ BiPreMap a b a0。我知道类型族的类型推断缺乏我们在使用 ADTS 时获得的大部分便利（注入性、生成性等），但我对这种情况下的问题究竟是什么以及如何规避它的理解非常有限. 我可以指定一些可以清除它的约束吗？

我在 Haskell 中编写了以下线性代数向量

当我尝试实现Foldable时，我遇到了具有不同定义的问题（即*和* -> *）Zero。Succ

这个问题有明显的解决方案吗？