问题标签 [rank-n-types]

镜头可以像任何普通功能一样组成。我们有：

现在考虑这个例子：

展开我们得到：

并且函数组合的类型是：

它缺乏任何通用量化和类型类约束。现在我的问题是，编译器/类型检查器如何处理这两个特性，以便函数组合运算符可用于组合镜头？

我的猜测是，可以有通用量化的函数和类型类约束，只要它们与正在组合的两个函数匹配。

我试图在 F# 中表达 Free monad 的 Church 编码。Free专门用于特定的函子，Effect.

我可以同时写return_ : 'T -> Free<'T>，bind: ('T -> Free<'U>) -> Free<'T> -> Free<'U>没有任何问题。

下面给出了我的实现草图。

当我尝试为这种编码编写解释器时，我遇到了一个问题。

给定以下代码：

Free.runFree我在函数内的第三个参数中收到类型错误interpret：

我理解为什么会发生这种情况（第一个函数的结果类型确定'R === string*int）并怀疑可以使用 rank-2 函数来解决（可以在 F# 中编码，例如http://eiriktsarpalis.github.io/typeshape/#/ 33 ) 但我不知道如何应用它。

任何指针将不胜感激。

迈克尔

Apologies for the potentially vague question title - I'm not sure how to phrase it because I have a pretty poor understanding of what the problem is.

Basically, how do I make the following compile? :-p

GHC (v8.2.2) complains that a is a rigid type variable and can't seem to cope with the idea that (g val) and (g valM) could produce values of different types. I've tried using RankNTypes but to no avail.

Is there an extension I can use to help the compiler, or is there something conceptually broken with what I'm trying to do from a type-inference point of view?

当我声明这个新类型时：

这将定义假设的 rank-2 类型ListScott :: ((a -> ListScott a -> r) -> r -> r) -> ListScott a，编译器抱怨r不在范围内。从我想将一流的多态函数传递给的类型签名不是很明显ListScott吗？

为什么我需要一个明确的类型量词来r处理这种情况？

我不是类型理论家，可能忽略了一些东西......

我有以下定义

如您所见，我已经定义了一个 Symbol 类，它在类型签名中使用 ExampleCharacters。示例用法是使用let sym = Terminal "xyy" :: Symbol Variable名称创建变量符号"xyy"。

现在，显而易见的下一步是推广ExampleCharacter到Character c. 我尝试了以下方法：

但我收到以下错误：

我不太确定错误想告诉我什么。为什么是forall (c :: * -> *) a. Character c非法约束以及如何呢？有什么办法吗？

下面的代码（与位置内联注释）给出了我遇到的令人费解的行为的一个最小示例。

本质上，为什么 (2) 会导致糟糕的空间/时间性能，而 (1) 不会？

以下代码在 ghc 版本 8.4.3 上编译并运行如下： ghc -prof -fprof-auto -rtsopts test.hs; ./test +RTS -p

一个。使用 (1) 和 (3) 注释，编译时不使用-O2，代码只输出“hello”三次，正如我所期望的那样。

湾。使用 (2) 和 (3) 注释，编译时不使用-O2，代码输出“hello”八次。它似乎每一步输出一个额外的“你好”。我不明白为什么会这样。

C。使用 (1) 和 (4) 进行注释，编译时不使用-O2，代码运行速度非常快。

d。使用 (2) 和 (4) 注释，编译时不使用-O2，代码运行速度非常慢，性能报告（包括在下面）显示，vstate与 variant 相比，调用次数和使用的内存更多c。我也不明白为什么会这样。

e. 使用注释 (2) 和 (4) 进行编译， -O2代码的行为与变体相同c。很明显 ghc 能够优化掉变体中发生的任何病理行为d。

这是变体c（快速）的分析报告：

这是变体的分析报告d（慢；没有-O2）：

以下是关于为什么会发生这种情况的一些注释/猜测/问题：

• 性能下降与“hello”计数增加有什么关系？病态的版本似乎每增加一步就会多输出一个“你好”。为什么？
• 我知道 Haskell 中的多态性很慢，如StackOverflow question中所述。这可能是问题的一部分，因为当vstate被单态化为时，病态行为就会消失vstate :: Float。但我不明白为什么在位置 (2) 中缺少 let-binding 会导致如此糟糕的时间/空间性能。
• 这是更大代码库中性能错误的最小版本，我们通过使用“单态化”浮点类型数字来修复它realToFrac（提交在这里，以防有人好奇）。我知道编译-O2修复了最小示例中的行为，但我在更大的代码库中尝试了它，它并没有解决性能问题。（我们在更大的代码库中需要 rank-2 多态性的原因是为了使用ad库进行 autodiff。）是否有比 using 更有原则的解决方法realToFrac，例如可以应用的内联特化？

考虑以下最小示例：

正如预期的那样，这种类型检查很好。但是，将 ifa重构为使用let语句：

它突然无法进行类型检查，并出现以下错误：

为什么会这样？这不违反等式推理吗？

在原始代码中可以看到我只是将一个表达式提取到一个绑定中，这是 haskell 声称应该始终可能的基本内容之一。

最小案例（在 freenode 上 @dminuoso 的帮助下创建）

我想g保持多态性（这样我就可以将它提供给其他期望它的函数）：

错误：

#haskell IRC 上发布的原始问题（动机）：

但我得到：

基于https://ghc.haskell.org/trac/ghc/ticket/12587我尝试显式应用类型来帮助类型检查器：

但后来我得到：

考虑这个实现on

它是什么类型的？GHC 会说(b -> b -> c) -> (a -> b) -> a -> a -> c，这是一个很好的猜测。但它错过了实例on (+) toInteger。让我们尝试解决这个问题（使用、RankNTypes和KindSignatures）：AllowAmbiguousTypesConstraintKinds

然后进行类型检查。但是当我们尝试

我们得到

那是什么意思？

我正在玩一个使用存在量化的 ConduitT 风格的 monad，我正在玩 whack-a-mole 试图让类型统一。这个场景有两个版本：

在这里，Await i有一个存在量化的a，它允许await方法传递它i -> Await i -> a想要的任何类型。

失败：

该runYield方法已损坏，因为它无法在Await iwith中统一存在限定的类型参数a。

第二种情况：

为了修复runYield，Await现在指定a，与Await i a统一Yield i a。但是，既然a指定了，yield就不能将它传递给它喜欢的Yield i b任何值b：

失败：

所以我似乎需要两种方式，有时是存在量化的，有时是具体的。我已经尝试创建包装器来隐藏额外的类型参数，切换newtype为 有任何想法吗？dataAwait i a -> Await i b