Лучший способ написать конструкторы как функции в Agda

Question

У меня есть список

data List (X : Set) : Set where
  <>   : List X
  _,_  : X -> List X -> List X

определение равенства

data _==_ {l}{X : Set l}(x : X) : X -> Set l where
  refl : x == x

и конгруэнтность

cong : forall {k l}{X : Set k}{Y : Set l}(f : X -> Y){x y} -> x == y -> f x == f y
cong f refl = refl

Я пытаюсь доказать

propFlatten2 : {X : Set } ( xs0 : List X ) (x : X)  (xs1 : List X) (xs2 : List X)
              -> ( xs0 ++ x , xs1 ) ++ xs2  ==  xs0 ++ (x , xs1 ++ xs2 )
propFlatten2 <> x xs1 xs2 = refl
propFlatten2 (x , xs0) x₁ xs1 xs2 =   cong (λ l -> x , l) {!!}

Есть ли лучший способ использовать непосредственно конструктор _,_ кроме как через лямбду в последней строке?

Answer 1

У Agda нет специального синтаксиса для частичного применения операторов. Однако вы можете использовать операторы в их обычной префиксной версии:

x + y = _+_ x y

Это удобно, когда вам нужно частично применить крайний левый аргумент (ы):

_+_ 1 = λ x → 1 + x

Когда вам нужно частично применить аргументы, идущие справа, ваши возможности более ограничены. Как упоминалось в комментариях, вы можете использовать одну из удобных функций, таких как flip (нашел в Function):

flip f x y = f y x  -- Type omitted for brevity.

А потом просто flip аргументы _+_:

flip _+_ 1 = λ x → x + 1

---

Иногда вы найдете операторов, единственной целью которых является сделать код немного лучше. Лучший пример, который я могу придумать, это, вероятно, Data.Product.,_, Когда вы пишете зависимую пару (Data.Product.Σ), иногда первая часть пары может быть заполнена автоматически. Вместо того чтобы писать:

_ , x

Вы можете просто написать:

, x

Трудно сказать, когда написание специализированного оператора, такого как приведенный выше, действительно того стоит; если ваш единственный вариант использования использует его с конгруэнтностью, я бы просто придерживался лямбда-выражения, поскольку он очень ясно дает понять, что происходит.