Матч по равенству

Я как-то новичок в Идрисе. Раньше я использовал немного agda, и у меня тяжелый опыт работы в GHC Haskell. Я пытаюсь понять, почему что-то, что работает в GHC Haskell, не работает в Идрисе. Следующий код не компилируется (idris version 0.12.3, nobuiltins, noprelude):

data Nat = S Nat | Z

plus : Nat -> Nat -> Nat
plus Z right        = right
plus (S left) right = S (plus left right)

rightIdentityAlt : (n : Nat) -> n = (plus n Z)
rightIdentityAlt Z = Refl
rightIdentityAlt (S y) = case rightIdentityAlt y of
  Refl => Refl

Это не выполняется со следующей ошибкой:

idris_binary.idr: 21: 3-7: При проверке левой стороны блока IdrisBinary.case в rightIdentityAlt на idris_binary.idr: 20: 31: Объединение y и плюс y Z приведет к бесконечному значению

Примерный эквивалентный код GXC haskell делает typecheck. Я могу получить версию Idris для typecheck, если я вместо этого использую:

cong : (x : Nat) -> (y : Nat) -> (f : Nat -> Nat) -> x = y -> f x = f y
cong _ _ _ Refl = Refl

rightIdentity : (n : Nat) -> n = (plus n Z)
rightIdentity Z = Refl
rightIdentity (S x) = cong x (plus x Z) S (rightIdentity x)

Я думаю, что причина, по которой rightIdentityAlt работает в GHC Haskell, но не в Идрисе, имеет дело с различием в том, как унификация работает на двух языках. В GHC Haskell унификации, полученные из сопоставления шаблонов на GADT, просто распространяются повсюду, но в Idris кажется, что вам нужно уточнить исходные типы с помощью предложения with. Вот моя попытка сделать это:

rightIdentityAlt : (n : Nat) -> n = (plus n Z) 
rightIdentityAlt Z = Refl
rightIdentityAlt (S y) with (rightIdentityAlt y) 
  rightIdentityAlt (S y) | Refl {A = Nat} {x = y} = Refl

Blast. Еще ничего хорошего. Теперь мы потеряли равенство, которое мы изначально пытались доказать:

idris_binary.idr:26:20:When checking left hand side of with block in IdrisBinary.rightIdentityAlt:
Type mismatch between
    plus y Z (Inferred value)
and
    y (Given value)
Holes: IdrisBinary.rightIdentityAlt

Я понимаю, что прагматичный ответ заключается только в том, чтобы переписать это с помощью cong или для чего-то, связанного с тактикой, но я действительно хочу понять, почему способ, которым я хочу писать rightIdentityAlt, не работает. Согласование шаблонов на = не дает доказательств в объеме, как я ожидал бы. Есть ли способ заставить это сделать это, или есть что-то принципиально неправильное в этом подходе в Идрисе?

Ответы

Ответ 1

Я думаю, что это может быть связано с Hasochism.

Слово Хадохизм использовалось Линдли и Макбрайдом, чтобы ослабить боль и удовольствие от использования (псевдо) зависимых типов, таких как GADT в Haskell. В Haskell, как только мы сопоставим с Refl, GHC вызывает доказательство теоремы, которое будет распространять это равенство для нас. Это часть удовольствия.

"Боль" состоит в том, что она не имеет полностью зависимых типов. У нас действительно нет f : (x : T) -> ... в Haskell. Если x универсально квантифицирован, он должен быть типом в Haskell, и он будет удален во время выполнения, поэтому мы не можем напрямую сопоставить шаблон с ним. Мы должны использовать синглтоны и другие методы. Кроме того, в Haskell мы не можем написать g : (h : *->*) (x : *) -> h x -> ... и передать первые два аргумента, чтобы сделать h x = Int. Для этого h должна быть функцией уровня типа, например. g (\t:* -> t) Int 42, но у нас их нет. Однако отсутствие этой функции значительно упрощает "удовольствие", и стирание типа делает язык более эффективным (хотя мы должны иметь возможность избежать стирания с помощью типов pi), так что это не так уж плохо.

В любом случае, в Agda/Coq/Idris, если вы не хотите использовать некоторые автоматические вещи (например, тактику), вы должны написать свою собственную зависимую элиминацию и принести доказательства равенства, где они вам нужны, например. используя cong.

В качестве альтернативы это также компилируется:

rightIdentityAlt : (n : Nat) -> n = (plus n Z)
rightIdentityAlt Z = Refl
rightIdentityAlt (S y) = aux y (rightIdentityAlt y) 
  where
  aux : (m : Nat) -> m = plus n Z -> S m = plus (S n) Z
  aux _ Refl = Refl

Обратите внимание на самую внутреннюю функцию aux, которая включает в себя две переменные m и n. Это делается так, при сопоставлении с Refl это приводит к замене m на plus n Z, не затрагивая n. Чтобы сыграть этот "трюк", нам нужны две разные переменные.

Проблема с исходным кодом заключается в том, что m и n, там, являются множественными вхождениями одной и той же переменной n. Это заставляет зависимое соответствие заменять как на S y, так и проверять полученный тип, который вызывает ошибку.

Лично я могу лучше понять зависимое сопоставление шаблонов в Coq, где вы можете использовать match .. return ..., чтобы выразить полученный тип каждого совпадения. Кроме того, это выражение, которое может быть вложенным, не требуя отдельных определений. Вот он, аннотированный некоторыми комментариями, показывающими, как каждое соответствие влияет на требуемый тип.

Fixpoint rightIdentityAlt (n: nat): n = plus n O :=
   match n return n = plus n O with
   | O => (* required: n = plus n O with n := O
             hence   : O = plus O O *)
      eq_refl
   | S y =>  (* required: n = plus n O with n := S y
                hence   : S y = plus (S y) O *)
      match rightIdentityAlt y in _ = o return S y = S o with
      | eq_refl => (* required: S y = S o with o := y
                      hence   : S y = S y *)
         eq_refl
      end
   end
.