相关疑难解决方法(0)

也许这是一个愚蠢的问题.下面是一个报价的Hasochism纸:

解决此问题的一种方法是将由参数化方程给出的引理编码为Haskell函数.通常,这种引理可以编码为类型的函数:

? x1 ... xn. Natty x1 ? ... ? Natty xn ? ((l ~ r) ? t) ? t

Run Code Online (Sandbox Code Playgroud)

我以为我理解了RankNTypes,但我无法理解这个命题的最后部分.我正在非正式地阅读它"给出一个需要的术语l ~ r,返回那个术语".我确信这种解释是错误的,因为它似乎导致了循环:我们l ~ r直到证明本身的结论才知道,那么我怎么能期望作为证据的假设提供一个需要的术语呢？

我本来期望一个等式证明有一个更像这样的类型:

Natty x1 ? ... ? Natty xn ? l :~: r

非正式地,"给定一堆Nattys,返回命题证明l并且r相等"(使用GHC的Data.Type.Equality).这对我来说更有意义,并且似乎与你在其他依赖类型系统中所说的一致.我猜它相当于论文中的版本,但我正在努力精神上消除这两个版本.

总之,我很困惑.我觉得我错过了一个关键的洞察力.我该怎么读这个类型((l ~ r) => t) -> t？