也许这是一个愚蠢的问题。以下是来自《Hasochism》论文的一句话:
One approach to resolving this issue is to encode lemmas, given by parameterised equations, as Haskell functions. In general, such lemmas may be encoded as functions of type:
∀ x1 ... xn. Natty x1 → ... → Natty xn → ((l ~ r) ⇒ t) → t
我本以为我理解了RankNTypes
,但是我不能理解这个命题的最后一部分。 我非正式地阅读它为“给定需要l〜r
的术语,返回该术语”。 我确信这种解释是错误的,因为它似乎导致循环性: 我们在证明本身的结论之前不知道l〜r
,那么我如何期望作为证明假设提供需要那个的术语呢?
我本来希望一个等式证明具有更接近以下类型:
Natty x1 → ... → Natty xn → l :~: r
Informally, "给定一些Natty,返回一个证明命题
l
和r
相等的证明"(使用GHC的Data.Type.Equality)。这对我来说更有意义,似乎与其他依赖类型系统中的说法一致。我猜它相当于论文中的版本,但我很难理解这两个版本之间的关系。简而言之,我感到困惑。我觉得我缺少一个关键的洞察力。我应该如何阅读类型
((l ~ r) => t) -> t
?
Π
投射到夜空中以引起他的注意。 - Benjamin Hodgsona
,forall v. (a -> v) -> v
和a
之间有什么区别?然后观察到,在GHC中,=>
基本上是作为函数实现的,你已经发现了一种表示类型l ~ r
的值的方式,即它在CPS形式下表达为forall v. ((l ~ r) => v) -> v
,尽管这不是在GHC-Haskell中可以居住的类型。 - Daniel Wagner((l ~ r) => t) -> t
理解为:“假设l ~ r
是类型正确的,返回一个同样的表达式,并在证明l ~ r
并消除这个假设的上下文中返回它”。请注意,翻译保持原文意思不变,同时使其更加通俗易懂。 - Daniel Wagner