haskell - "lemma"函数的一般类型应该如何理解？

Question

也许这是一个愚蠢的问题。这是来自 the Hasochism paper 的引用:

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

非正式地说，“给定一堆 Natty，返回 l 和 r 相等的命题证明”(使用 GHC 的Data.Type.Equality)。这对我来说更有意义，并且似乎与您在其他依赖类型系统中所说的一致。我猜它与论文中的版本相同，但我正在努力在心理上平衡这两个版本。

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

Answer 1

I'm reading it as "given a term which requires l ~ r, return that term"

它是“给定一个类型包含 l 的术语，返回该术语，并将所有 l 替换为类型中的 r ”(或在另一个方向 r -> l )。这是一个非常巧妙的技巧，允许您委托(delegate)所有 cong , trans , subst以及与 GHC 类似的东西。

这是一个例子:

{-# 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

更新

特化是有启发性的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

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

Or, to say it another way, you can read ((l ~ r) => t) -> t as, "given a term that is well typed assuming that l ~ r, return that same term from a context where we have proven l ~ r and discharged that assumption".

让我们详细说明证明部分。

在 assoc' Zy my py t = t案例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)

显然Vec a ((n :+ m) :+ p)是 Vec a (n :+ (m :+ p))假设((n :+ m) :+ p) ~ (n :+ (m :+ p)) .