问题标签 [rank-n-types]

快速示例：

这里：

• l l1类型检查
• l l2不进行类型检查
• k k1不进行类型检查
• k k2类型检查
• m m1类型检查
• m m2不进行类型检查

虽然我对发生的事情完全没问题，l但m我不明白这k部分。存在某种“更多态”的关系，例如，forall a. a -> a比forall b. [b] -> [b]因为可以替换而更多态a/[b]。但是，如果多态类型位于逆变位置，为什么这种关系会翻转呢？

正如我所看到k的，“一台机器可以在任何产生 Int 的列表上运行机器”。k1是“一台机器，它采用任何产生 int 的内同态机器”。k1因此，它提供的远比k想要的多，为什么它不符合它的要求呢？我觉得我的推理有些错误，但我无法理解......

我试过这个：

但它不起作用，有没有办法做到这一点？我环顾四周，所有类似的东西都非常复杂和有限。

错误消息，根据要求：

我有一个函数f op = (op 1 2, op 1.0 2.0)，它需要像这样工作：

但是在不声明它的类型的情况下，f它的工作方式如下：

我正在努力声明f. 它应该采用一个适用于所有实例的运算符Num。在 Haskell 中甚至有可能吗？

rank2classes包提供了一个版本，Functor其映射函数似乎是类型构造函数之间的自然转换。

按照这个想法，这是 2 级版本Bifunctor：

似乎很清楚，Foo可以给这种类型一个Rank2Bifunctor实例：

但是Bar这种嵌套f和的类型呢g：

对于初学者来说，似乎我们需要Functor p在 , 的签名中要求rank2bimap能够转换.gf

是Bar有效的“rank-2 双函子”吗？

haskell 中是否有任何绑定器来引入在类型中量化的类型变量（和约束）？

我可以添加一个额外的论点，但这违背了目的。

我正在尝试使用Test.QuickCheck.Monadic.

该模块提供了一个线束

执行ST-based 测试和一个函数

将任何动作提升到测试单子中。

在我的代码中，我有一个多态单子动作：

以下函数

编译失败：

但是这个

编译没有问题。

谁能解释一下？

在 Haskell 中，如果启用RankNTypes扩展

然后可以定义自然数，因为它们在 System-F 中编码：

耶！下一步是定义案例操作：想法是

当然这不是直接可能的。可能的一件事是正常定义自然数并定义and{data Nats = Zero | Succ Nats}之间的“转换” ，然后使用Haskell 内置的句法构造。NatNatscase

在无类型 lambda 演算中，caseN可以写为

遵循显然由 Kleene 发现的用于定义前置函数的技巧。这个版本caseN看起来确实应该使用上面给出的类型进行类型检查。 (zero, b) :: (Nat, b)和\(n0, _) -> (succ n0, f n0) :: (Nat, b) -> (Nat, b)，所以fold (zero, b) (\(n0, _) -> (succ n0, f n0)) n :: (Nat, b)。

但是，这不会在 Haskell 中进行类型检查。试图\(n0, _) -> (succ n0, f n0)用

表明ImpredicativeTypes可能需要扩展，因为succf似乎需要扩展。对于更典型{data Nats = Zero | Succ Nats}的 ，caseN构造确实有效（在更改为适当的fold, 和Zero, 之后Succ）。

可以直接caseN上班Nat吗？需要不同的技巧吗？

我不明白为什么会这样，指的是：Rank2Types的目的是什么？-> @dfeuer 解释：

... 要求参数是多态的不仅允许它与多种类型一起使用；它还限制了该函数可以用它的参数做什么以及它如何产生它的结果......

...实际上，返回不在给定列表中的元素的任何函数都不会进行类型检查

在对等级 N 类型的任何解释中，我都没有看到描述的这种效果（或好处），大部分时间是关于让被调用者选择类型等的故事……这对我来说很清楚且易于掌握，但是我看不出我们可以通过哪种优点（仅扩展等级）来控制/限制功能域（和共同域）......

如果有人可以更深入地了解这里涉及的 rankN 机制。谢谢

也许有更好的方法来实现我想要的，但这是我目前的尝试。

我正在使用该singletons包以将值具体化为类型。这很好用，但在某些时候，我将不得不运行一个在具体类型中具有多态性的函数，并期望它有一个Typeableinstance。当然，Haskell 中的所有类型都有这样的实例（至少 afaik？），但由于类型变量在编译时是未知的，类型检查器无法找到这样的实例。让我举例说明：

这给了我错误

这很有意义。withSomeSing不保证Sing a传递给 continuation 满足Typeable a.

我可以通过隐藏一些导入来解决这个问题，Data.Singleton而是使用相关约束定义我自己的版本：

这使一切正常，但感觉绝对是糟糕的风格。

因此我的问题是：有什么方法可以导入 and 的原始定义SomeSing，withSomeSing但是用这个额外的约束来增加它们的类型？或者，您如何建议以更好的方式解决这个问题？