Как именно конг может быть хорошо напечатан? - PullRequest
Новая
       9

Как именно конг может быть хорошо напечатан?

0 голосов
/ 02 октября 2018

Я смотрел на определение 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)?Я что-то упустил?

1 Ответ

0 голосов
/ 02 октября 2018

Сопоставление зависимых шаблонов к вашим услугам.

Если мы сделаем отверстие в вашем 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, и весь контекст корректируется соответствующим образом.

Это та же логика, что и в GADT на Haskell: 

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 прекрасно объединяются, как мы знаем из контекста .

...