Имеет ли `(a → b) → b` эквивалент наличия` a`?

Ответ 1

Ответ luqui превосходный, но я собираюсь предложить другое объяснение forall b. (a -> b) -> b === a по нескольким причинам: во-первых, потому что я думаю, что обобщение на Codensity немного чрезмерно велико. И второе, потому что это возможность связать кучу интересных вещей вместе. Onwards!

z5h Magic Box

Представьте, что кто-то щелкнул монеткой, а затем положил ее в волшебную коробку. Вы не можете видеть внутри поля, но если вы выберете тип b и передадите в поле функцию с типом Bool -> b, поле выплюнет b. Что мы можем узнать об этой коробке, не заглядывая в нее? Можем ли мы узнать, что такое состояние монеты? Можем ли мы узнать, какой механизм использует ящик для создания b? Как оказалось, мы можем сделать и то, и другое.

Мы можем определить поле как функцию ранга 2 типа Box Bool, где

type Box a = forall b. (a -> b) -> b

(Здесь тип ранга 2 означает, что производитель ящиков выбирает a, и пользователь поля выбирает b.)

Мы помещаем a в поле, а затем закрываем окно, создавая... закрытие.

-- Put the a in the box.
box :: a -> Box a
box a f = f a

Например, box True. Частичное приложение - это просто умный способ создания закрытий!

Теперь, это монеты голов или хвосты? Поскольку я, ящик пользователя, разрешено выбирать b, я могу выбрать Bool и передать функцию Bool -> Bool. Если я выберу id :: Bool -> Bool, тогда возникает вопрос: будет ли поле выплюнуть значение, которое оно содержит? Ответ заключается в том, что ящик будет либо выплюнуть значение, которое он содержит, либо выплюнет глупость (нижнее значение, например undefined). Другими словами, если вы получите ответ, то ответ должен быть правильным.

-- Get the a out of the box.
unbox :: Box a -> a
unbox f = f id

Поскольку мы не можем генерировать произвольные значения в Haskell, единственная чувствительная вещь, которую может сделать ящик, - применить данную функцию к тому, что она скрывает. Это является следствием параметрического полиморфизма, также известного как параметричность.

Теперь, чтобы показать, что Box a изоморфен a, нам нужно доказать две вещи о боксе и распаковке. Нам нужно доказать, что вы выбрали то, что вы вложили, и что вы можете положить то, что вы выбрали.

unbox . box = id
box . unbox = id

Я сделаю первый и оставлю второй как упражнение для читателя.

  unbox . box
= {- definition of (.) -}
  \b -> unbox (box b)
= {- definition of unbox and (f a) b = f a b -}
  \b -> box b id
= {- definition of box -}
  \b -> id b
= {- definition of id -}
  \b -> b
= {- definition of id, backwards -}
  id

(Если эти доказательства кажутся довольно тривиальными, потому что все (полные) полиморфные функции в Haskell являются естественными преобразованиями и то, что мы доказываем здесь - естественность. Параметричность в очередной раз дает нам теоремы для низких, низкие цены!)

В качестве стороннего и другого упражнения для читателя, почему я не могу определить rebox с помощью (.)?

rebox = box . unbox

Почему мне нужно встроить определение (.) в себя как своего рода пещерного человека?

rebox :: Box a -> Box a
rebox f = box (unbox f)

(Подсказка: каковы типы box, unbox и (.)?)

Идентичность и кодовость и Yoneda, Oh My!

Теперь, как мы можем обобщить box? luqui использует Codensity: оба b обобщаются произвольным конструктором типа, который мы будем называть f. Это Codensity transform f a.

type CodenseBox f a = forall b. (a -> f b) -> f b

Если мы зафиксируем f ~ Identity, вернемся назад box. Однако есть еще один вариант: мы можем нажать только тип возврата с помощью f:

type YonedaBox f a = forall b. (a -> b) -> f b

(Я как бы отдал игру здесь с этим именем, но мы вернемся к этому.) Мы также можем исправить f ~ Identity здесь, чтобы восстановить box, но мы разрешаем пользователю окна пропускать нормальная функция, а не стрелка Клейсли. Чтобы понять то, что мы обобщаем, рассмотрим еще раз определение box:

box a f = f a

Ну, это просто flip ($), не так ли? И получается, что наши два других блока построены путем обобщения ($): CodenseBox - частично примененное, перевернутое монадическое связывание, а YonedaBox - частично примененное flip fmap. (Это также объясняет, почему Codensity f является Monad и Yoneda f является Functor для любого выбора f. Единственный способ создать его - это закрыть транзакцию или fmap, соответственно.) Кроме того, обе эти концепции теории эзотерических категорий - это действительно обобщения понятия, знакомого многим рабочим программистам: преобразование CPS!

Другими словами, YonedaBox является вложением Yoneda, а правильно абстрагированные законы box/unbox для YonedaBox являются доказательством леммы Йонеды!

TL; ДР:

forall b. (a -> b) -> b === a является экземпляром леммы Йонеды.

Ответ 2

Этот вопрос представляет собой окно в ряд более глубоких понятий.

Во-первых, обратите внимание, что в этом вопросе есть двусмысленность. Имеем ли мы тип forall b. (a -> b) -> b, так что мы можем создать экземпляр b с любым типом, который нам нравится, или мы имеем в виду (a -> b) -> b для некоторого определенного b, который мы не можем выбрать.

Таким образом, мы можем формализовать это различие в Haskell:

newtype Cont b a = Cont ((a -> b) -> b)
newtype Cod a    = Cod (forall b. (a -> b) -> b)

Здесь мы видим некоторый словарь. Первый тип - это Cont монада, вторая Codensity Identity, хотя мое знакомство с последним термином недостаточно сильное, чтобы сказать, что вы должны назвать этим на английском языке.

Cont b a не может быть эквивалентен a, если a -> b не может содержать как минимум столько же информации, сколько a (см. комментарий Дэн Робертсон ниже). Так, например, обратите внимание, что вы никогда не сможете получить что-либо из Cont Void a.

Cod a эквивалентен a. Чтобы убедиться в этом, достаточно убедиться в изоморфизме:

toCod :: a -> Cod a
fromCod :: Cod a -> a

реализация которого я оставлю как упражнение. Если вы действительно хотите это сделать, вы можете попытаться доказать, что эта пара действительно является изоморфизмом. fromCod . toCod = id легко, но toCod . fromCod = id требует бесплатную теорему для Cod.

Ответ 3

Другие ответы проделали большую работу, описывая взаимосвязь между типами (a -> b) -> b и a, но я хотел бы указать на одно предостережение, потому что это приводит к некоторым интересным открытым вопросам, над которыми я работал.

Технически, (a -> b) -> b и a не изоморфны в langauge, таком как Haskell, который (1) позволяет вам написать выражение, которое не завершается, и (2) является либо позывным (строгим), либо содержит seq. Моя точка здесь не, чтобы быть nitpicky или показать, что параметричность ослаблена в Haskell (как хорошо известно), но что могут быть опрятные способы укрепить ее и в некотором смысле восстановить изоморфизмы, подобные этой.

Существуют некоторые термины типа (a -> b) -> b, которые не могут быть выражены как a. Чтобы понять, почему, начнем с рассмотрения доказательства, которое Рейн оставил в качестве упражнения, box . unbox = id. Оказывается, это доказательство на самом деле более интересно, чем в его ответе, поскольку он в решающей степени полагается на параметричность.

box . unbox
= {- definition of (.) -}
  \m -> box (unbox m)
= {- definition of box -}
  \m f -> f (unbox m)
= {- definition of unbox -}
  \m f -> f (m id)
= {- free theorem: f (m id) = m f -}
  \m f -> m f
= {- eta: (\f -> m f) = m -}
  \m -> m
= {- definition of id, backwards -}
  id

Интересный шаг, когда параме- ричность входит в игру, применяет свободную теорему f (m id) = m f. Это свойство является следствием (a -> b) -> b, типа m. Если мы рассматриваем m как поле с базовым значением типа a внутри, то единственное, что m может сделать с его аргументом, - применить его к этому базовому значению и вернуть результат. С левой стороны это означает, что f (m id) извлекает базовое значение из поля и передает его на f. Справа это означает, что m применяет f непосредственно к базовому значению.

К сожалению, это рассуждение не совсем выполняется, если у нас есть такие термины, как m и f ниже.

m :: (Bool -> b) -> b
m k = seq (k true) (k false)

f :: Bool -> Int
f x = if x then ⊥ else 2`

Вспомним, что мы хотели показать f (m id) = m f

f (m id)
= {- definition f -}
  if (m id) then ⊥ else 2
= {- definition of m -}
  if (seq (id true) (id false)) then ⊥ else 2
= {- definition of id -}
  if (seq true (id false)) then ⊥ else 2
= {- definition of seq -}
  if (id false) then ⊥ else 2
= {- definition of id -}
  if false then ⊥ else 2
= {- definition of if -}
  2

m f
= {- definition of m -}
  seq (f true) (f false)
= {- definition of f -}
  seq (if true then ⊥ else 2) (f false)
= {- definition of if -}
  seq ⊥ (f false)
= {- definition of seq -}
  ⊥

Ясно, что 2 не равно ⊥, поэтому мы потеряли нашу свободную теорему и изоморфизм между a и (a -> b) -> b с ней. Но что случилось, точно? По существу, m - это не только поле с красивым поведением, потому что оно применяет свой аргумент к двум различным базовым значениям (и использует seq для обеспечения того, чтобы оба этих приложения были фактически оценены), что мы можем наблюдать, передавая в продолжение, что заканчивается на одном из этих базовых значений, но не на другом. Другими словами, m id = false на самом деле не является точным представлением m как Bool, потому что он "забывает" о том, что m вызывает свой ввод как true, так и false.

Проблема связана с взаимодействием между тремя вещами:

• Наличие прерывания.
• Наличие seq.
• Тот факт, что термины типа (a -> b) -> b могут применять их вход несколько раз.

Нет надежды на то, чтобы обойти точки 1 или 2. Линейные типы могут дать нам возможность бороться с третьей проблемой, хотя, Линейная функция типа a ⊸ b - это функция от типа a до типа b, которая должна использовать свой вход ровно один раз. Если нам понадобится m иметь тип (a -> b) ⊸ b, то это исключает наш контрпример для свободной теоремы и должно показать изоморфизм между a и (a -> b) ⊸ b даже при отсутствии итерации и seq.

Это действительно здорово! Это показывает, что линейность обладает способностью "спасать" интересные свойства, приручая эффекты, которые могут затруднить истинное экваториальное мышление.

Однако остается одна большая проблема. У нас пока нет методов доказательства свободной теоремы, необходимой для типа (a -> b) ⊸ b. Оказывается, текущие логические отношения (инструменты, которые мы обычно используем для выполнения таких доказательств) не были разработаны, чтобы учесть линейность так, как это необходимо. Эта проблема имеет последствия для установления правильности для компиляторов, выполняющих переводы CPS.