您在Haskell中找到了更高级别类型的用途？

Question

较高等级的类型看起来很有趣.从Haskell wikibook到这个例子:

foo :: (forall a. a -> a) -> (Char,Bool)
foo f = (f 'c', f True)

现在我们可以在foo id没有编译器爆炸的情况下进 这个例子在书中很快被我在其他几个地方看到的真实世界的例子:ST monad和runST.那很酷.

但是我还没有遇到过这样一种情况:我通过使用更高级别的参数编写自己的函数来解决问题.你呢？您在野外有什么样的rank-2或rank-n多态性？

Answer 1

Weirich和Washburnn的"Boxes go Bananas"!(纸,幻灯片)

这是一个非常原始的,可能稍微不准确的解释它的全部内容:给定一个归纳类型,BGB允许你代表那种"积极"类型的函数空间 - 它们从不区分它们的论点.它们最多包括他们的参数作为其他值的一部分(通常是相同类型).

Weirich + Washburn使用它来获得Haskell中lambda演算的可能足够的 HOAS表示-XRankNTypes(有人证明它足够吗？).

我在这里使用它(警告:凌乱的代码)转一个

(forall g . GArrow g => g () x -> g () y)

进入

(forall g . GArrow g => g x y)

这是有效的,因为rank-2多态类型不能"检查"其参数的结构 - 它所能做的就是将该参数"粘贴"到更大的结构中.一些技巧让我弄清楚粘贴发生的位置,然后我将粘贴点(如果有的话)反馈回到输入GArrow.

你不能用这个Control.Arrow类做这个,因为整个Haskell函数空间通过它"泄漏"到它arr.

Answer 2

看看Darcs源代码withRepoLock中的函数.

Darcs支持多种存储库格式,并且通过类型类表示支持.因此,您可以编写通用存储库格式的通用代码.在实际读取磁盘存储库时,您希望通过一些公共代码调度到该代码,该代码确定存储库所处的格式并选择正确的类型类实例化.

Answer 3

最近有人在Stack Overflow上问了一个问题,可以用更高级别的类型来解决.

另一个应用是在Scrap Your Boilerplate文件中.