cong 到底怎样才能好类型呢？

Question

我在看cong的定义：

cong : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

而且我不明白为什么它的类型很好。特别是，refl 的隐式参数似乎必须是 f x 和 f y。为了让事情更清楚，我写了一个非隐式版本的相等性，并试图复制证明：

data Eq : (A : Set) -> A -> A -> Set where
  refl : (A : Set) -> (x : A) -> Eq A x x

cong : (A : Set) -> (B : Set) -> (f : A -> B) -> 
       (x : A) -> (y : A) -> (e : Eq A x y) -> Eq B (f x) (f y)
cong A B f x y e = refl B (f x)

这会导致类型错误：

x != y of type A when checking that the expression refl B (f x) has type Eq B (f x) (f y)

不出所料。除了 (f x)，我还能有什么？我错过了什么吗？

Answer 1

依赖模式匹配为您服务。

如果我们在您的 cong

上打个洞

cong : (A : Set) -> (B : Set) -> (f : A -> B) ->
       (x : A) -> (y : A) -> (e : Eq A x y) -> Eq B (f x) (f y)
cong A B f x y e = {!refl B (f x)!}

看看它，我们会看到

Goal: Eq B (f x) (f y)
Have: Eq B (f x) (f x)

所以值确实不同。但是一旦你在 e:

上进行模式匹配

cong : (A : Set) -> (B : Set) -> (f : A -> B) ->
       (x : A) -> (y : A) -> (e : Eq A x y) -> Eq B (f x) (f y)
cong A B f x y (refl .A .x) = {!refl B (f x)!}

x 与 y 相同的事实被揭露，上下文被悄悄重写：y 的每个出现都被 x 替换，所以往洞里看，我们现在看到了

Goal: Eq B (f x) (f x)
Have: Eq B (f x) (f x)

注意我们可以这样写

cong A B f x .x (refl .A .x) = refl B (f x)

即根本不要绑定 y，只是通过点模式说它与 x 相同。我们通过 e : Eq A x y 上的模式匹配获得了这些信息，因为一旦执行了匹配，我们就知道它实际上是 e : Eq A x x，因为这就是 refl 的类型签名所说的。 Eq A x y 和 Eq A x x 的统一导致一个微不足道的结论：y 等于 x 并且整个上下文相应地调整。

这与 Haskell GADT 的逻辑相同：

data Value a where
  ValueInt  :: Int  -> Value Int
  ValueBool :: Bool -> Value Bool

eval :: Value a -> a
eval (ValueInt  i) = i
eval (ValueBool b) = b

当您在 ValueInt 上匹配并获得类型 Int 的 i 时，您还揭示了 a 等于 Int 并将此知识添加到上下文（通过等式约束）使得 a 和 Int 稍后可以统一。这就是我们能够 return i 结果的原因：因为 a 从类型签名和 Int 完美统一，正如我们从 上下文.

cong 到底怎样才能好类型呢？

How exactly can cong be well-typed?

agda