应该如何理解“引理”函数的一般类型？

也许这是一个愚蠢的问题。这是引用自the 哈索主义 paper https://personal.cis.strath.ac.uk/conor.mcbride/pub/hasochism.pdf:

解决这个问题的一种方法是对引理进行编码，由下式给出 参数化方程，如 Haskell 函数。一般来说，这样的引理 可以编码为类型的函数：

∀ x1 ... xn. Natty x1 → ... → Natty xn → ((l ~ r) ⇒ t) → t

我以为我明白了RankNTypes，但我无法理解这个命题的最后部分。我将其非正式地解读为“给定一个需要l ~ r，返回该术语”。我确信这种解释是错误的，因为它似乎会导致循环：我们不知道l ~ r直到证明本身得出结论，那么我怎么能期望提供一个需要这样做的术语作为证明的假设呢？

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

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

非正式地说，“给定一堆Nattys，返回命题的证明l and r是相等的”（使用 GHC数据.类型.相等 https://hackage.haskell.org/package/base-4.7.0.2/docs/Data-Type-Equality.html）。这对我来说更有意义，并且似乎与您在其他依赖类型系统中所说的一致。我猜它与论文中的版本相同，但我正在努力在心理上消除这两个版本。

简而言之，我很困惑。我觉得我错过了一个关键的见解。我应该如何读取类型((l ~ r) => t) -> t?

我把它读作“给定一个需要l ~ r，返回那个 学期”

它“给定一个术语，其类型包含l，返回该术语以及所有ls 被替换为rs 在类型中”（或在另一个方向r -> l）。这是一个非常巧妙的技巧，允许您委托所有cong, trans, subst以及与 GHS 类似的内容。

这是一个例子：

{-# LANGUAGE GADTs, DataKinds, PolyKinds, TypeFamilies, TypeOperators, RankNTypes #-}

data Nat = Z | S Nat

data Natty n where
    Zy :: Natty Z
    Sy :: Natty n -> Natty (S n)

data Vec a n where
    Nil  :: Vec a Z
    Cons :: a -> Vec a n -> Vec a (S n)

type family (n :: Nat) :+ (m :: Nat) :: Nat where
    Z     :+ m = m
    (S n) :+ m = S (n :+ m)

assoc :: Natty n -> Natty m -> Natty p -> (((n :+ m) :+ p) ~ (n :+ (m :+ p)) => t) -> t
assoc  Zy     my py t = t
assoc (Sy ny) my py t = assoc ny my py t

coerce :: Natty n -> Natty m -> Natty p -> Vec a ((n :+ m) :+ p) -> Vec a (n :+ (m :+ p))
coerce ny my py xs = assoc ny my py xs

UPDATE

专业化很有启发assoc:

assoc' :: Natty n -> Natty m -> Natty p ->
            (((n :+ m) :+ p) ~ (n :+ (m :+ p)) => Vec a (n :+ (m :+ p)))
                                               -> Vec a (n :+ (m :+ p))
assoc'  Zy     my py t = t
assoc' (Sy ny) my py t = assoc ny my py t

coerce' :: Natty n -> Natty m -> Natty p -> Vec a ((n :+ m) :+ p) -> Vec a (n :+ (m :+ p))
coerce' ny my py xs = assoc' ny my py xs

丹尼尔·瓦格纳解释了评论中发生的事情：

或者，换句话说，您可以将 ((l ~ r) => t) -> t 读作“给定 假设 l ~ r 的输入良好的术语，返回相同的术语 从我们已经证明 l ~ r 并排除了这一点的背景来看 假设”。

我们来详细说明一下证明部分。

In the assoc' Zy my py t = t case n等于Zy因此我们有

((Zy :+ m) :+ p) ~ (Zy :+ (m :+ p))

这减少到

(m :+ p) ~ (m :+ p)

这显然是恒等式，因此我们可以解除该假设并返回t.

在每个递归步骤中，我们维护

((n :+ m) :+ p) ~ (n :+ (m :+ p))

方程。所以当assoc' (Sy ny) my py t = assoc ny my py t方程变为

((Sy n :+ m) :+ p) ~ (Sy n :+ (m :+ p))

这减少到

 Sy ((n :+ m) :+ p) ~ Sy (n :+ (m :+ p))

由于定义(:+)。由于构造函数是单射的

constructors_are_injective :: S n ~ S m => Vec a n -> Vec a m
constructors_are_injective xs = xs

方程变为

((n :+ m) :+ p) ~ (n :+ (m :+ p))

我们可以打电话assoc'递归地。

终于在号召下coerce'这两个术语是统一的：

 1. ((n :+ m) :+ p) ~ (n :+ (m :+ p)) => Vec a (n :+ (m :+ p))
 2.                                      Vec a ((n :+ m) :+ p)

Clearly Vec a ((n :+ m) :+ p) is Vec a (n :+ (m :+ p))假设((n :+ m) :+ p) ~ (n :+ (m :+ p)).