Работа с типами до определенной эквивалентности

Question

Предположим, мы хотели бы представить (подписанные) целые числа как группу Гротендика над натуральными числами (или, другими словами, как пару (m, n), где понимаемое целое число - m - n):

data ZTy : Type where
  MkZ : (m, n : Nat) -> ZTy

Теперь (структурное) равенство, которое язык дает нам бесплатно, больше не является тем, что мы хотим: вместо этого мы заботимся только об определенном отношении эквивалентности (а именно, (m1, n1) ~ (m2, n2) тогда и только m1 + n2 = m2 + n1). Не важно, давайте запишем это!

data Equiv : ZTy -> ZTy -> Type where
  MkEquiv : (prf : m1 + n2  = m2 + n1) -> Equiv (MkZ m1 n1) (MkZ m2 n2)

Но работа с этим очень быстро запутывается. Любой аргумент типа prop Const (для prop : ZTy -> Type) заменяется на (k : ZTy) -> (k `EqZ` Const) -> prop k, если не сказать больше (в качестве более прикладного примера я пытаюсь записать двустороннее индукционное доказательство для этого типа, и я Я до сих пор не уверен, что я правильно понял даже подпись этого термина).

Более того, такой функции, как replaceZ : {P : ZTy -> Type} -> (k1 `Equiv` k2) -> P k1 -> P k2 (очевидно), не существует, но я не могу найти лучшего кандидата. В качестве интересного примечания / наблюдения, если мы не экспортируем определение из ZTy, ни один клиентский код P не сможет это заметить, и эта функция будет иметь смысл для любого определенного P в любом другом модуле, но похоже, что мы не можем усвоить это в языке.

Еще одна вещь, которую я имею в виду, - это ограничить набор предикатов теми, которые имеют отношения эквивалентности. То есть замена P : ZTy -> Type чем-то вроде P : ZTy -> Type, pAdmissible : ZPred P, где ZPred подтверждает доказательство своей инвариантности относительно отношения эквивалентности:

data ZPred : Type -> Type where
  MkZPred : {P : ZTy -> Type} ->
            (preservesEquiv : {k1, k2 : ZTy} -> (k1 `Equiv` k2) -> P k1 -> P k2) ->
            ZPred P

В любом случае, каков общий подход к работе с такими типами? Есть ли что-нибудь еще, что бы хорошо сработало?

Я также кое-что слышал о фактор-типах, но я мало что знаю.

Answer 1

Coq описывает эти ситуации с богатым языком «комбинаторов отношений», который является лучшей версией вашей последней идеи. Я переведу это. У вас есть

ZTy : Type -- as yours

А вы приступаете к определению отношений и функций по отношениям:

-- if r : Relation t and x, y : t, we say x and y are related by r iff r x y is inhabited
Relation : Type -> Type
Relation t = t -> t -> Type

-- if x, y : ZTy, we say x and y are (Equiv)alent iff Equiv x y is inhabited, etc.
Equiv : Relation ZTy  -- as yours
(=)   : Relation a    -- standard
Iso   : Relation Type -- standard

-- f and f' are related by a ==> r if arguments related by a end up related by r
(==>) : Relation a -> Relation b -> Relation (a -> b)
(==>) xr fxr = \f, f' => (x x' : a) -> xr x x' -> fxr (f x) (f' x')
infixr 10 ==>

Идея состоит в том, что Equiv, (=) и Iso - все отношения равенства. Equiv и (=) - два разных понятия равенства на ZTy, а (=) и Iso - два понятия равенства на Type. (==>) объединяет отношения в новые отношения.

Если у вас есть

P : ZTy -> Type

Вы хотели бы сказать, что Equiv аргументы alent отображаются на Iso морфических типов. То есть вам нужно

replaceP : (x x' : ZTy) -> Equiv x x' -> Iso (P x) (P x')

Как может помочь язык отношений? Ну, по сути, replaceP говорит о том, что P "равно" самому себе в соответствии с отношением Equiv ==> Iso (NB Equiv ==> Iso не является эквивалентностью, но единственное, чего ему не хватает, это рефлексивности.) Если функция не «равно» себе в Equiv ==> Iso, тогда это немного похоже на «противоречие», и эта функция «не существует» в вашей вселенной. Или, скорее, если вы хотите написать функцию

f : (ZTy -> Type) -> ?whatever

Вы можете ограничить себя правильным типом функций, требуя аргумент доказательства, например, так:

Proper : Relation a -> a -> Type
Proper r x = r x x

f : (P : ZTy -> Type) -> Proper (Equiv ==> Iso) P -> ?whatever

Обычно, однако, вы отбрасываете доказательства, если в этом нет крайней необходимости. На самом деле стандартная библиотека уже содержит множество функций на ZTy, например

concatMap : Monoid m => (ZTy -> m) -> List ZTy -> m

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

concatMapProper : Proper ((Equiv ==> (=)) ==> Pairwise Equiv ==> (=))
-- you'd really abstract over Equiv and (=), but then you need classes for Relations
Pairwise : Relation a -> Relation [a] -- as you may guess

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

proof : Property Constant

всегда необходимо заменить на

proof : (k : ZTy) -> Equiv k Constant -> Property k

является лишь частично обоснованным. Если у вас уже есть

PropertyProper : Proper (Equiv ==> Iso) Property

, что вы, скорее всего, должны, тогда вы можете написать proper : Property Constant и просто протолкнуть его через PropertyProper, чтобы обобщить его при необходимости. (Или напишите proper с общей подписью, используя простое определение с PropertyProper сверху). Вы не можете отказаться от написания доказательства где-то , потому что оно просто не так тривиально.

Стоит также отметить, что (==>) использует иное, чем в качестве аргумента Proper. Он служит универсальным расширением равенства:

abs1 : ZTy -> Nat
abs1 (MkZ l r) = go l r
  where go (S n) (S m) = go n m
        go Z     m     = m
        go n     Z     = n
abs2 : ZTy -> Nat
abs2 (MkZ l r) = max l r - min l r

absEq : (Equiv ==> (=)) abs1 abs2
--    : (x x' : ZTy) -> Equiv x x' -> abs1 x = abs2 x'