Является ли наличие `(a -› b) - ›b` эквивалентом` a`?

Луки ответил превосходно, но я собираюсь предложить другое объяснение forall b. (a -> b) -> b === a по нескольким причинам: во-первых, потому что я думаю, что обобщение на Code density немного излишне восторженно. А во-вторых, потому что это возможность связать кучу интересного воедино. Вперед!

Волшебная шкатулка z5h

Представьте, что кто-то подбросил монету, а затем положил ее в волшебную шкатулку. Вы не можете видеть внутри коробки, но если вы выберете тип 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 и (.)?)

Идентичность, кодовая плотность и Йонеда, о боже!

Теперь, как мы можем обобщить Box? luqui использует плотность кода: оба bs обобщаются конструктором произвольного типа, который мы назовем f. Это преобразование 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 - это вложение Йонеды, а правильно абстрагированные _55 _ / _ 56_ законы для YonedaBox являются доказательством леммы Йонеды!

TL; DR:

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

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

Во-первых, обратите внимание, что в этом вопросе есть двусмысленность. Имеем ли мы в виду тип 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)

Здесь мы видим некоторый словарный запас. Первый тип - это _6 _ монада, вторая - _7 _ 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.

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

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

Есть некоторые термины типа forall b . (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. Это свойство является следствием forall b . (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.

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

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

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

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

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