问题标签 [undecidable-instances]

在使用UndecidableInstances之前编写一些代码时，我遇到了一些我觉得很奇怪的东西。我无意中创建了一些我认为不应该进行类型检查的代码：

具体来说，convertFoo当给定任何输入以产生任何输出时，函数会进行类型检查，如evil函数所示。起初，我以为我可能不小心实现了unsafeCoerce，但这并不完全正确：实际上尝试调用我的convertFoo函数（例如，通过执行类似的操作evil 3）只是进入了无限循环。

我有点模糊地理解发生了什么。我对这个问题的理解是这样的：

• ConvertFoo我定义的实例适用于任何输入和输出，a并且b仅受转换函数必须存在的两个附加约束的限制a -> Foo和Foo -> b。
• 不知何故，该定义能够匹配任何输入和输出类型，因此似乎调用 toconvertFoo :: a -> Foo正在选择convertFoo自身的定义，因为无论如何它是唯一可用的定义。
• 由于convertFoo无限调用自身，函数进入一个永不终止的无限循环。
• 由于convertFoo永不终止，该定义的类型是底部，所以从技术上讲，没有任何类型被违反，并且程序类型检查。

现在，即使上面的理解是正确的，我仍然对为什么整个程序进行类型检查感到困惑。具体来说，鉴于不存在此类实例，我预计ConvertFoo a Fooand约束会失败。ConvertFoo Foo b

我确实（至少模糊地）理解在选择实例时约束并不重要 - 仅根据实例头选择实例，然后检查约束 - 所以我可以看到这些约束可能会因为我的ConvertFoo a b实例而很好地解决，这是尽可能宽容的。但是，这将需要解决相同的约束集，我认为这会将类型检查器置于无限循环中，导致 GHC 要么挂起编译，要么给我一个堆栈溢出错误（后者我见过前）。

不过，很明显，类型检查器不会循环，因为它会愉快地触底并愉快地编译我的代码。为什么？在这个特定示例中，实例上下文如何得到满足？为什么这不会给我一个类型错误或产生一个类型检查循环？

最近，我问了一个关于我创建的生成运行时无限循环的实例的问题，我得到了一个很好的答案！既然我明白了发生了什么，我有一个新问题：我可以修正我的尝试来实现我最初的目标吗？

让我重申并具体澄清我的问题是什么：我想创建一个类型类，用于在我的代码中的一些等效数据类型之间进行转换。我创建的类型类既非常简单又非常通用：它包含一个在任意数据类型之间进行转换的转换函数：

但是，此类型类有一个特定目的：在具有规范表示的特定值类之间进行转换。因此，有一个特定的数据类型是“规范的”，我想使用这个数据类型的属性来减轻我的类型类实现者的负担。

具体来说，考虑两种不同的表示，RepA和RepB。我可能会合理地定义一些实例来将这些表示转换为Canonical：

现在，这立即有用，因为我现在可以同时使用convertRep这两种表示形式，但它主要只是作为重载convertRep名称的一种方式。我想做一些更强大的事情：毕竟，我现在已经有效地定义了以下类型的四个函数：

在我看来，根据这些定义，我还应该能够生成以下类型的两个函数：

基本上，由于这两种数据类型都可以转换为/从规范表示，我想直接自动生成相互之间的转换函数。正如我在上述问题中提到的那样，我的尝试看起来像这样：

不幸的是，这个实例过于宽松，当提供两种我认为应该无效的类型时，它会导致生成的代码递归——我还没有定义规范转换的类型。

为了尝试解决这个问题，我考虑了另一种更简单的方法。我想我可以使用两个类型类而不是一个来防止这个递归问题：

现在可以定义一个新函数来执行convertRep我最初感兴趣的转换：

然而，这是以灵活性为代价的：不再可能在两个非规范表示之间创建直接转换实例。

例如，也许我知道这一点RepA并且RepB会非常频繁地互换使用，因此它们会在彼此之间进行相当多的转换。因此，转换为/从的额外步骤Canonical是浪费时间。我想选择定义一个直接转换实例：

它提供了两种常见类型之间的“快速路径”转换。

总结一下：有没有办法使用 Haskell 的类型系统来完成所有这些目标？

1. 给定在表示和规范形式之间转换的函数，在表示之间“生成”转换。
2. 可选择在通常转换的实例之间提供“快速路径”。
3. 拒绝没有明确定义的实例；也就是说，不允许ConvertRep Canonical Canonical（和类似的）创建无限重复并产生底部的实例。

Haskell 类型系统令人印象深刻，但我担心在这种情况下，它的实例解析规则不足以同时完成所有这些目标。

当我第一次阅读有关-XUndecidableInstances.

事实上，我遇到过很多需要不可判定实例的应用程序，但没有一个应用程序实际上会导致与不可判定性相关的任何问题。卢克的例子是有问题的，原因完全不同

– 好吧，这显然会与任何适当的实例重叠，所以不确定性Group是我们最不担心的：这实际上是不确定的！

但很公平，因为我一直在脑海中保留“不可判定的实例可能会使编译器挂起”。

当我在 CodeGolf.SE 上阅读这个挑战时，它是从哪里获得的，要求提供可以无限挂起编译器的代码。好吧，这听起来像是在不确定的情况下工作，对吧？

事实证明我无法让他们这样做。以下内容立即编译，至少从 GHC-7.10 开始：

我什至可以使用类方法，它们只会在运行时导致循环：

但是运行时循环并不罕见，您可以在 Haskell98 中轻松编写这些代码。

我还尝试了不同的、不那么直接的循环，例如

同样，在编译时没有问题。

那么，在解析不可判定的类型类实例时，实际上需要什么来挂起编译器呢？

Sipser 的 TOC 书中的定理 5.3 是关于 Regular_TM = {M | M 是图灵机 (TM)，L(M) 是常规语言}。为了达到矛盾，假设 TM R 是 Regular_TM 的决定者，然后 R 用于决定 Acceptance 问题，如打击 TM S 所示：

S = "On input (M,w) where M is a TM and w is a string: 1. Construct the code of TM M2 as follows: M2 = "On input x: (a) If x of the form 0^n1^n, accept. (b) else, run M on w and if M accepts w, then accept." 2. Run R on (M2). 3. If R accepts, accept; if R rejects, reject."

我有两个问题。第一个是 M_2 中的 x 固定吗？如果不是，它来自哪里？

第二个问题。为什么我们关心 M2 中的 x。如果 R 真的是一个决策者，我们为什么要关心检查 x 是否在 0^n1^n 中。那么下面的 TM S' 有效吗？

S = "On input (M,w) where M is a TM and w is a string: 1. Construct the code of TM M2 as follows: M2 = "On input x: //ignore x (a) run M on w and if M accepts w, then accept else reject." 2. Run R on (M2). 3. If R accepts, accept; if R rejects, reject."

我正在尝试为 Cofree 编写以下 Monoid 实例：

但我收到以下错误：

我以前遇到过 Undecidable Instances ，但我不确定为什么这是不可判定的，我该如何解决？我需要添加 UndecidableInstances 吗？谢谢！！

1) 接受语言 L = {ε} 的图灵机 M 是否不接受任何条目？

一方面，我认为它可能是错误的，因为空词可能是一个条目，但另一方面，我认为这可能是一个无法确定的问题。

2）是否每台可判定语言的图灵机在任何输入时都会停止？

同样的想法，直觉上我会说是的，由于可判定的定义，但我不知道，有什么困扰我。

3）回文的语言是否可以确定，无论 aphabet 是什么？

对于这一点，我几乎毫不怀疑它是错误的，因为有了赖斯定理，我们可以证明，这个问题是不可判定的。

我正在尝试使用索引嵌套注释构建 AST。我添加了一个用于在顶层剥离注释的类型类，并尝试提供默认实例，有效地说明“如果您知道如何自行剥离注释，那么您就知道如何在特定 AST 节点处剥离注释。”

由于我的一个树节点是一个Nat索引谓词，并且它的父节点存在地量化了这个变量，所以当我尝试为父节点编写实例时，我陷入了帕特森的条件。也就是说，我在断言中的类型变量比在头脑中的要多。

如果我打开UndecidableInstances，则 GHC 无法将变量与 kind 统一起来Nat。

如果我进一步打开AllowAmbiguousTypes，那么我会得到一个更荒谬的错误，它说它找不到实例，尽管它正在寻找的实例在类型实例的断言中。

我的问题是：

1. 这实际上是一个不好的实例，还是类型检查器过于保守？
2. 如果它不好或无法解决问题，我还能如何提供这种默认的剥离行为？

这是最小的代码（我去掉了对类型错误不重要的位，所以有些位可能看起来是多余的）：

这是没有的确切错误UndecidableInstances：

这是它的一个：

这是一个AllowAmbiguousTypes：

编辑：

正如 Daniel Wagner 建议的那样，一种解决方案是在实例中进行PeelableAnn PredicateAnn ann断言。PeelableAST Literal ann但是，我从来没有peelA在定义中使用由 PeelableAnnPeelableAST Literal ann定义的，我希望这个实例作为默认行为并且能够通过直接提供一个PeelableAST (Predicate n) ann实例来覆盖它。换句话说，剥离可能本质上是上下文相关的。

既然PeelableAnn PredicateAnn ann是要求PeelableAST (Predicate n) ann，我觉得GHC应该能找到并满足这个条件。

我可以简单地拥有一个虚假PeelableAnn PredicateAnn ann实例，而只会被更具体的实例忽略，但这很hacky

以下代码段使 GHC（使用 8.6.2 和 8.4.4 检查）在编译期间卡住：

我认为它被卡住了，因为tGHC 试图找到C T，这导致F T C通过类型族扩展F回C T，这就是它正在寻找的（无限循环）。

我想理论上 GHC 可以说它C T从自身达到了它的要求，并且任何依赖于自身的东西都可以递归地工作，还是我误解了什么？

旁注：在我偶然发现这种行为的真实示例中，我能够实现我想要的，而编译器不会被替换为UndecidableSuperClasses卡住Data.Constraint.Dict。

我想在实例头中使用AllBFfrom ，如下所示：barbies

由于隐藏的种类多态性，这失败了。西蒙 说：

• 变量k在约束中出现的频率AllBF MyClass f b 高于在实例头部中出现的频率MyClass (Barbie b f) （UndecidableInstances用于允许这样做）

我想避开UndecidableInstances这里。我尝试过的一件事是使我的实例单态为f：

但是，这会导致另一个错误：

• 非法嵌套约束AllBF MyClass f b （ UndecidableInstances用于允许这样做）

天真地，我尝试内联 的定义AllBF，但这并没有改变任何东西：

• 非法嵌套约束AllB (ClassF MyClass f) b （ UndecidableInstances用于允许这样做）

有没有办法在不打开的情况下创建这个实例UndecidableInstances？

我正在使用 Dominic Orchard 的type-level-sets库，该库非常接近他的论文。

我正在构建一个 DSL，用于在同步并发程序期间表达各方之间的通信。我需要的一件事是能够表达涉及原始社区子集的“子程序”；这将与fromUniversal.

这是我的代码的简化版本：

在_clique中，有提供Subset recipients clq和的上下文Subset csl parties；我需要 GHC 以某种方式理解这意味着Subset recipients parties. 但是没有这样的实例可用。

为了类型级别集的目的，我如何表示“子集”的传递性？

这是错误消息：

我试着简单地添加

to Lib.hs (apparently Subset isn't closed-world; I think); this gives a variety of different error messages depending what compiler options I use, or if I swap out OVERLAPS for INCOHERENT. The jist of it seems to be that GHC can't pick an instance to use, even if I promise it'll be ok.

I tried making the recipient type explicit in _clique (so I can just add the needed Subset recipients parties to the context), but it seems like no matter what I do reinterpret always introduces/requires a "fresh" x and/or recipients; I haven't found a way of providing the context for the type-variable that's actually used.

It seems unlikely that this is impossible, but I've been stuck on it for a day and I'm out of my depth.

Edit

我一直在使用以下解决方案进行该项目；这显然是平庸的。具体来说，除了传递性之外，还有很多属性很好，比如两个集合都是第三个集合的子集，那么它们的并集也是第三个集合的子集。对于 Haskell 的类型系统来说，“免费”获得这样的属性可能太过分了……