您在Haskell中发现了哪些高阶类型的用法?

19

高阶类型看起来很有趣。从Haskell wikibook获得以下示例:

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

现在我们可以在不让编译器爆炸的情况下评估foo id了。这个例子很快就被书中的真实世界例子所跟随,我在其他地方也看到过:ST单子和runST。那很酷。

但我还没有遇到过通过编写具有高阶参数的自己的函数来解决问题的情况。你有吗?你们有什么关于排名2或排名n多态性的例子吗?

4个回答

8

Weirich和Washburnn的“Boxes go Bananas”!(论文, 幻灯片)

这是一个非常粗略且可能稍有不准确的解释:给定归纳类型,BGB允许您表示从该类型到“正面”的函数空间 - 它们从不在其参数上进行情况区分。最多,它们将其参数包括为其他值的一部分(通常是相同类型的值)。

Weirich+Washburn使用这个来获得一个可能-足够的HOAS表示lambda演算在-XRankNTypes Haskell中(是否有人已经证明它是足够的?)。

我在这里(警告:代码混乱)使用它来转换一个

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

转换为一个

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

这段代码之所以有效,是因为二阶多态类型无法“检查”其参数的结构——它只能将该参数“粘贴”到更大的结构中。一些诡计让我找出了粘贴发生的位置,然后将粘贴点(如果有)穿回GArrow的输入。
使用Control.Arrow类无法做到这一点,因为整个Haskell函数空间通过arr泄漏到其中。

7
请查看Darcs源代码中的withRepoLock等函数。
Darcs支持多种存储库格式,并通过类型类表达该支持。因此,您可以编写通用于存储库格式的代码。实际上读取磁盘上的存储库时,您需要通过一些公共代码进行分派,该代码确定存储库的格式并选择正确的类型类实例化。

3
可能你曾经遇到过需要使用更高级别类型的问题,但却没有意识到。例如在Darcs示例中,他们可以轻松地实现它而不使用更高级别的类型。相反,某些函数将有前提条件,调用者必须确保它们符合要求,比如为存储库格式选择正确的函数实例化。
更高级别类型的优点是将正确性的责任从程序员转移到编译器。采用传统方法,如果Darcs开发人员在存储库类型上犯了错误,结果将是运行时错误或损坏的数据。而使用更高级别的类型,开发人员将在编译时获得类型错误。

0
一个相对简单的高阶类型示例可以在Luke Palmer的无IO可分割供应中找到 - 他展示了如何使使用简单的唯一值供应更容易:
runSupply :: (forall a. Eq a => Supply a -> b) -> b

网页内容由stack overflow 提供, 点击上面的
可以查看英文原文,
原文链接