У Hask или Agda есть эквалайзеры?

Я несколько не определился относительно того, является ли это вопросом математики .SE или SO, но я подозреваю, что математики в целом вряд ли знают или особенно заботятся об этой категории, в то время как программисты Haskell вполне могут это сделать.

Итак, мы знаем, что Hask имеет продукты, более или менее (я, конечно, работаю с идеализированным-Хаском). Меня интересует, есть ли у него эквалайзеры (в этом случае он будет иметь все конечные пределы).

Интуитивно это кажется не так, поскольку вы не можете делать разделение, как вы можете на множестве, и поэтому подобъекты кажутся сложными в целом. Но для любого конкретного случая, который вы хотели бы придумать, кажется, что вы сможете взломать его, выработав эквалайзер в Установить и подсчитав его (поскольку в конце концов каждый тип Haskell счетно, и каждое счетное множество изоморфно либо конечному типу, либо натуральным, оба из которых имеют Haskell). Поэтому я не вижу, как бы я нашел контрпример.

Теперь Агда кажется более многообещающим: там довольно легко создавать подобъекты. Является ли очевидный сигма тип Σ A (λ x → f x == g x) эквалайзером? Если детали не работают, это морально эквалайзер?

Ответ 1

tl; dr предложенный кандидат не совсем эквалайзер, но его нерелевантная копия

Кандидат на эквалайзер в Агде выглядит неплохо. Так что пусть попробует. Нам понадобится базовый комплект. Вот мой тип паразитных зависимостей Auslus refusenik и однородное равномерное равенство.

record Sg (S : Set)(T : S -> Set) : Set where
  constructor _,_
  field
    fst : S
    snd : T fst
open Sg

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

Здесь ваш кандидат на эквалайзер для двух функций

Q : {S T : Set}(f g : S -> T) -> Set
Q {S}{T} f g = Sg S \ s -> f s == g s

с проекцией fst, отправляющей Q f g в S.

Что он говорит: элемент Q f g - это элемент S типа источника, а также доказательство того, что f s == g s. Но это эквалайзер? Попробуем сделать так.

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

_o_ : {R S T : Set} -> (S -> T) -> (R -> S) -> R -> T
(f o g) x = f (g x)

Итак, теперь мне нужно показать, что любой h : R -> S, который идентифицирует f o h и g o h, должен влиять на кандидата fst : Q f g -> S. Мне нужно доставить и другой компонент u : R -> Q f g, и доказательство того, что действительно h факторы как fst o u. Здесь изображение: (Q f g , fst) является эквалайзером, если всякий раз, когда диаграмма коммутирует без u, существует единственный способ добавить u с диаграммой, все еще коммутирующей.

Здесь существует существование опосредованного u.

mediator : {R S T : Set}(f g : S -> T)(h : R -> S) ->
           (q : (f o h) == (g o h)) ->
           Sg (R -> Q f g) \ u -> h == (fst o u)

Ясно, что я должен выбрать тот же элемент S, который выбирает h.

mediator f g h q = (\ r -> (h r , ?0)) , ?1

оставляя меня с двумя доказательными обязательствами

?0 : f (h r) == g (h r)
?1 : h == (\ r -> h r)

Теперь ?1 может быть просто refl, поскольку для определения функции Агда для определения определено равенство eta. Для ?0 мы благословлены q. Равные функции, относящиеся к применению

funq : {S T : Set}{f g : S -> T} -> f == g -> (s : S) -> f s == g s
funq refl s = refl

поэтому мы можем взять ?0 = funq q r.

Но давайте не будем отмечать преждевременно, поскольку существование посреднического морфизма недостаточно. Мы требуем также его уникальности. И здесь колесо, скорее всего, пойдет на уступчивость, потому что == является интенсиональным, поэтому уникальность означает, что существует только один способ реализации посреднической карты. Но тогда наши предположения также интенсивно...

Здесь наше доказательство. Мы должны показать, что любой другой посредничающий морфизм равен тому, который выбирается mediator.

mediatorUnique :
  {R S T : Set}(f g : S -> T)(h : R -> S) ->
  (qh : (f o h) == (g o h)) ->
  (m : R -> Q f g) ->
  (qm : h == (fst o m)) ->
  m == fst (mediator f g h qh)

Мы можем немедленно заменить через qm и получить

mediatorUnique f g .(fst o m) qh m refl = ?

? :  m == (\ r -> (fst (m r) , funq qh r))

который выглядит хорошо, потому что у Agda есть законы для записей, поэтому мы знаем, что

m == (\ r -> (fst (m r) , snd (m r)))

но когда мы пытаемся сделать ? = refl, мы получаем жалобу

snd (m _) != funq qh _ of type f (fst (m _)) == g (fst (m _))

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

postulate ext : {S T : Set}{f g : S -> T} -> ((s : S) -> f s == g s) -> f == g

sndq : {S : Set}{T : S -> Set}{s : S}{t t' : T s} ->
       t == t' -> _==_ {Sg S T} (s , t) (s , t')
sndq refl = refl

uip : {X : Set}{x y : X}{q q' : x == y} -> q == q'
uip {q = refl}{q' = refl} = refl

? = ext (\ s -> sndq uip)

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

record Ex (S : Set)(T : S -> Set) : Set where
  constructor _,_
  field
    fst : S
    .snd : T fst
open Ex

и новый эквалайзер-кандидат

Q : {S T : Set}(f g : S -> T) -> Set
Q {S}{T} f g = Ex S \ s -> f s == g s

Вся конструкция проходит по-прежнему, за исключением того, что в последнем обязательстве

? = refl

принимается!

Итак, да, даже в настройках интенции, законы eta и способность отмечать поля как несущественные, дают нам эквалайзеры.

В этой конструкции не было неразрешимой проверки типов.

Ответ 2

Hask

В Hask нет эквалайзеров. Важно помнить, что мышление о типе (или объектах в любой категории) и их классах изоморфизма действительно требует думать о стрелках. То, что вы говорите о базовых множествах, верно, но типы с изоморфными лежащими в основе множествами, конечно, не обязательно изоморфны. Одно отличие между Hask и Set как стрелками Hask должно быть вычислимым, а на самом деле для идеализированного Hask они должны быть тотальными.

Я потратил некоторое время, пытаясь придумать настоящий защитный контрпример, и нашел некоторые рекомендации, предлагающие, что это невозможно, но без доказательств. Однако у меня есть некоторые "моральные" контрпримеры, если вы это сделаете; Я не могу доказать, что в Haskell нет эквалайзера, но это, безусловно, кажется невозможным!

Пример 1

f, g: ([Int], Int) -> Int

f (p,v) = treat p as a polynomial with given coefficients, and evaluate p(v).
g _ = 0

Эквалайзер "должен" быть типом всех пар (p, n), где p (n) = 0, вместе с функцией, вставляющей эти пары в ([Int], Int). Задача Гильберта 10-го эта проблема неразрешима. Мне кажется, что это должно исключать возможность того, что это тип Haskell, но я не могу это доказать (возможно ли, что существует какой-то причудливый способ построить этот тип, который никто не обнаружил?). Возможно, я не подключил точку или два - возможно, доказать это невозможно, не сложно?

Пример 2

Скажем, у вас есть язык программирования. У вас есть компилятор, который берет исходный код и ввод и создает функцию, для которой фиксированной точкой функции является выход. (Хотя у нас нет компиляторов, подобных этому, определение семантики вроде этого не неслыханно). Итак, у вас есть

compiler : String -> Int -> (Int -> Int)

(Un) запишет это в функцию

compiler' : (String, Int, Int) -> Int

и добавьте функцию

id' : (String, Int, Int) -> Int
id' (_,_,x) = x

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

Дополнительные примеры

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

Agda

Я не так хорошо знаком с Агдой. Моя интуиция заключается в том, что ваш сигма-тип должен быть уравнителем: вы можете записать тип вниз вместе с необходимой функцией впрыска, и похоже, что он полностью удовлетворяет определению. Однако, как человек, который не использует Agda, я не думаю, что я действительно способен проверить детали.

Реальная практическая проблема заключается в том, что typechecking, что тип sigma не всегда может быть вычислимым, поэтому не всегда полезно это делать. Во всех приведенных выше примерах вы можете записать тип Sigma, который вы указали, но вы не сможете легко проверить, является ли что-то членом этого типа без доказательства.

Кстати, вот почему Haskell не должен иметь эквалайзеры: если бы это было так, то проверка типов была бы неразрешимой! Зависимые типы - это то, что делает все тик. Они должны иметь возможность выражать интересные математические структуры в своих типах, в то время как Haskell не может, поскольку его система типов может быть определена. Поэтому я, естественно, ожидал, что идеализированная Агда будет иметь все конечные пределы (в противном случае я буду разочарован). То же самое касается и других зависимых языков; Coq, например, должен обязательно иметь все ограничения.