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并得到i类型时Int,你也会揭示出a等于Int并将这些知识添加到上下文中(通过一个等式约束),这在以后会产生a并且是Int统一的.这就是我们能够返回i的结果:因为a从类型签名和Int完全统一,正如我们从上下文中知道的那样.