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

Question

也许这是一个愚蠢的问题。以下是来自《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 Hodgson

---

有人点亮了 @pigworker 信号。 - Rein Henrichs

我认为你需要将一个 Π 投射到夜空中以引起他的注意。 - Benjamin Hodgson

@Gilles 让我们看看它是否会得到任何答案，如果没有的话就迁移吧 :) - Benjamin Hodgson

这是一个有趣的问题：对于给定的类型a，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

Answer 1

我将其翻译为“给定一个需要 l ~ r 的术语，返回该术语”。实际上，它的含义是“给定一个类型包含 l 的术语，返回在类型中所有 l 被替换为 r 的术语”（或者反过来是 r -> l）。这是一种非常巧妙的技巧，可以使您将所有 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

Daniel Wagner解释了以下情况：

或者换句话说，您可以将((l ~ r) => t) - > t理解为“假设l〜r是已经类型正确的术语，则从证明l〜r并且解除该假设的上下文中返回相同的术语”。

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

在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) 在假设 ((n :+ m) :+ p) ~ (n :+ (m :+ p)) 的情况下，等同于 Vec a (n :+ (m :+ p))。

- effectfully

---

我认为Chi的回答更好地解释了“它的意义”，但这是其强大功能的惊人演示。哇。 - dfeuer

你的例子帮助我建立了关于类型“使用”的“自上而下”的直觉（它似乎是一种安全地在等价类型之间进行转换的方式），但我仍然在努力理解它的“自下而上”的含义。您是否认为您可以提供一个示例，说明GHC如何对您的assoc和coerce函数进行类型检查？ - Benjamin Hodgson

Answer 2

I would have expected an equality proof to have a type more like this:

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

那是一个合理的替代方案。事实上，它在Hasochism论文中的逻辑等效。

{-# LANGUAGE GADTs, RankNTypes, TypeOperators, ScopedTypeVariables #-}
module Hasochism where

data l :~: r where
  Refl :: l :~: l

type Hasoc l r = forall t. (l ~ r => t) -> t

lemma1 :: forall l r. Hasoc l r -> l :~: r
lemma1 h = h Refl 

lemma2 :: forall l r. l :~: r -> Hasoc l r
lemma2 Refl t = t

从某种意义上来说，Hasoc l r 是约束条件 l ~ r 的不可预测编码。

相较于:~:，Hasochistic变体稍微容易使用一些。例如，一旦你有了...

type family A a
-- ...
proof1 :: Proxy a -> Hasoc a (A a)
proof1 _ = -- ...

您可以简单地按照以下方式使用它

use1 :: forall a. [a] -> [A a]
use1 t = proof1 (Proxy :: Proxy a) t

相反，使用

proof2 :: Proxy a -> a :~: A a
proof2 _ = -- ...

您需要：

use2 :: forall a. [a] -> [A a]
use2 t = case proof2 (Proxy :: Proxy a) of Refl -> t

- chi

---

谢谢，这证实了我的猜想，这两个证明版本是等价的。 - Benjamin Hodgson

Answer 3

我们已经得到了一些很好的答案，但作为罪犯，我想提供一些评论。

是的，这些引理有多个等效的表述方式。我使用的表述方式是其中之一，选择主要是出于实用考虑。现在（在一个更新的代码库中），我甚至定义了...

-- Holds :: Constraint -> *
type Holds c = forall t . (c => t) -> t

这是一个“消解器类型”的示例：它抽象了它的输出（消解的动机），并要求你构建零个或多个（这里是一个）更具体情况下实现动机的方法。阅读方法是反向的。它说：

如果你有一个问题（要占领任何动机类型 t），而没有人能帮助你，也许你可以通过在你的方法中假设约束 c 来取得进展。

鉴于约束语言支持与运算（又称元组），我们获得了编写引理的手段。

lemma :: forall x1 .. xn. (p1[x1 .. xn],.. pm[x1 .. xn])        -- premises
                       => t1[x1 .. xn] -> .. tl[x1 .. xn]       -- targets
                       -> Holds (c1[x1 .. xn],.. ck[x1 .. xn])  -- conclusions

而且可能会出现某些限制条件，比如前提条件p或结论c呈方程形式

l[x1 .. xn] ~ r[x1 .. cn]

现在，要部署这样一个引理，考虑填补空洞的问题。

_ :: Problem

通过消元引理来完善这个_，指定目标。动机来源于手头的问题。在Holds的情况下，方法（单数）仍然保持开放状态。

lemma target1 .. targetl $ _

这种方法的参数类型不会发生变化。

_ :: Problem

但是GHC将会知道更多的信息，因此更有可能相信您的解决方案。

有时候，在选择什么是（约束）前提条件和什么是（数据）目标之间存在一个约束与数据选择。我倾向于选择这些来避免歧义（Simon喜欢猜测x1 .. xn，但有时需要提示）并促进归纳证明，这对于目标（通常是类型级别数据的单例）比前提条件更容易。

至于部署，对于方程式，您可以切换到数据类型表示并进行情况分析。

case dataLemma target1 .. targetl of Refl -> method

事实上，如果您装备自己具备Dict存在主义

data Dict (c :: Constraint) :: * where
  Dict :: c => Dict c

你可以一次性处理很多事情

case multiLemma blah blah blah of (Refl, Dict, Dict, Refl) -> method

但是当只有一个方法时，消除器形式更加紧凑和易读。事实上，我们可以在不向右滑动的情况下链接多个引理。

lemma1 ..   $
...
lemmaj ..   $
method

如果您有一个包含两个或更多情况的消除器，我认为最好将其封装为GADT，以便使用场景可以使用构造函数标签有助于标记每个情况。

总之，是的，重点是选择事实的呈现方式，以最紧凑的方式扩展GHC的约束求解机制，以便更多的东西只需进行类型检查即可。如果您与Simon发生争执，向隔壁的Dimitrios解释自己通常是一个很好的策略。

- pigworker