问题标签 [rank-n-types]

我正在尝试了解 RankNTypes。

为什么编译器在这种情况下抱怨a不能[a]？

虽然以下类型检查正常？并且t可以t a。

上述编译失败是否仅在启用时发生RankNTypes。了解正在发生的事情的任何指示都会很棒。

谢谢。

在 Haskell 我不能写

因为

但我可以快乐地做

因此，正如我所见，GHC 确实支持与上面的错误消息相矛盾的暗示性多态性。为什么(->)在这种情况下要对类型构造函数进行特殊处理？是什么阻止了 GHC 将此功能推广到所有数据类型？

请向下滚动以阅读对此问题的重要编辑

原始（冗长）问题

我的网络应用程序的代码是用类型类约束的 monad 编写的，看起来像这样：

每个模块都有自己的server块，如下所示：

现在，该runForUser函数是“一对”单子的来源。我想要runForUser以下类型-sig，它将“内部单子”n转换为外部单子，m而不会使它们中的任何一个具体化：

这种“类型类魔法”需要尽可能长时间地不提交具体的 monad，希望这将允许我编写测试。

当最终为生产应用程序连接时，以下是runForUid将发生变化的内容：

当进行测试时：

我正在努力为该runForUid函数编写一个类型类。我尝试了各种技术，我得到的最接近的是以下技术：

如果我上面提出的解决方案是在正确的轨道上，那么我的问题是 - 我如何告诉编译器不要担心perms？这是实施的一项工作runForUser。我可以RankNTypes以任何方式使用并粘在forall perms某个地方并让它工作吗？

另一方面，如果上面给出的方法完全是垃圾，有什么更好的方法来完成这项工作？

编辑

我可能已经找到了一个可接受的解决方案，但我仍在寻找一种更好的方法来避免与类型相关的样板。

由于我不熟悉 rank-N 类型，因此类型签名gfoldl对我来说很麻烦：

我能想到的唯一功能是\xs y -> ($y) <$> xs和pure，分别。

其他功能如gunfold和gmapT也有类似问题。那么它们的重要用途有哪些值得注意的例子呢？

我试过这个实验：

但它给了我错误：

是否可以创建函数包装器，例如：

我一直在尝试实现似乎相当简单的类型。下面是一个演示该问题的人为示例。在它的核心，我想实现某种ComplexThing类型，它是一个由更简单的类型参数化的 GADT MyEnum，. 但是，有许多构造函数ComplexThing仅在应用于 的某些（可能很多）成员时才有效MyEnum。

解决此问题的一种方法是将这些构造函数分解为更简单的变体。下面我有一个这样的构造函数 ，NotSimple它可能被重铸为NotSimple_Bor NotSimple_C。一般来说，这似乎是一个不太优雅的解决方案。

我更喜欢这种类型的用户应该能够编写类似NotSimple ThingBor的东西NotSimple ThingC，并且不NotSimple ThingA应该进行类型检查。出于定义的目的ComplexThing，我还希望允许的子集的规范MyEnum相当通用（即在规范中重复元素应该是可以的，顺序不重要，并且在允许的数量方面应该是灵活的元素）。出于这个原因，我在单例类型的帮助下，追求使用类型级列表和遍历该列表的类型族SMyEnum。

我已经非常接近得到我想要的了。我实际上可以使用我设置的东西，但不存在完整的可用性。特别是，单独编写NotSimple SThingB对于类型检查器来说太多了。使用适当的类型签名，它变得站得住脚，但我认为这对潜在用户来说负担太大了。

请参阅下面的实现，以及一些测试及其结果。

我想我理解这种类型检查失败背后的原因。我希望它x0可以与 的参数神奇地统一NotSimple，但类型检查器看到的是它必须将该类型族（参数SThingB）产生的最终类型与通用的、普遍量化的规范统一起来该构造函数的参数。但是，我不确定解决此限制的最佳方法是什么。

任何关于我如何解决这个问题的建议都值得赞赏！如果我证明了任何概念或术语上的误解，也欢迎对此发表评论。

如何将 Haskell 中的约束含义编码为新的约束？在我的示例中，我想要求每个Functor c d f需要都Obj c x意味着Obj c (f x). 我正在写约束forall x . Obj c x => Obj d (f x)。

但这会产生以下错误：

我在这里做错了什么？我应该给编译器什么额外的提示？有没有更好的方法来实现这一点？

我的猜测是我需要使用Data.Constraintand :-，但是如何使用呢？

一般来说，我想知道是否有一种方法可以编写通用折叠来概括应用以下forall类型的函数：

给定一些数据类型D（instance Data (D a)可能对 有约束a）。具体来说，考虑一些简单的事情False `mkQ` isJust，或者一般来说，对更高种类数据类型的构造函数的查询。类似地，考虑一个mkT (const Nothing)只影响一种特定的高级类型的转换。

如果没有明确的类型签名，它们就会失败No instance for Typeable a0，这可能是工作中的单态限制。很公平。但是，如果我们添加显式类型签名：

相反，我们被告知forall外部签名的类型不明确：

我无法解决这个问题。如果我真的正确理解那a0是变量t :: forall a0. Data a0 => a0 -> a0，它怎么比说更模棱两可mkT not？如果有的话，我本来会mkT抱怨的，因为它是与isJust. 此外，这些函数比具体类型的分支更具多态性。

我很想知道这是否是证明内部约束的限制isJust :: Data a => ...——我的理解是，任何类型的实例Data都Maybe a必须Data a由实例约束有效instance Data a => Data (Maybe a)。

我正在尝试使用类型系统来确保永远不会从 monad M 中取出 X。我希望它的工作方式类似于runST，在这种情况下，不可能混合来自不同线程的环境。

但是，以下代码不会导致类型错误：

为什么 ST monad 中的类似代码会抛出错误而我的不会？据我了解，sinM s a应该被绑定，使sinX s成为自由类型变量，从而导致类型检查器出错。

在 Idris 中，这有效：

但是，有些不同的版本没有。这编译：

但如果我尝试使用它：

然后我得到Can't find implementation for Monad m第一个并且：

对于第二个。

我注意到即使只有return 5. 例如，如果我在 repl 中尝试：

有没有办法获得具有接口多态类型的值？我对 Idris 类型检查背后的原则有什么误解吗？（我来自 Haskell，这可能已经很明显了。）