Как понять, что типы a и forall r. (a -> r) -> r изоморфны

Question

В книге Мышление с типами , 6.4 Continuation Monad говорит, что типы a и forall r. (a -> r) -> r изоморфны c, что может быть засвидетельствовано следующими функциями:

cont :: a -> (forall r. (a -> r) -> r)
cont x = \f -> f x

unCont :: (forall r. (a -> r) -> r) -> a
unCont f = f id

В этой книге говорится, что любые два типа, имеющие одинаковую мощность, всегда будут изоморфны c друг другу. Поэтому я пытаюсь выяснить мощность типов a и forall r. (a -> r) -> r.

Предположим, что тип a равен |a|. Тогда для типа forall r. (a -> r) -> r как определить его мощность равна |a|? Тип функции a -> b имеет мощность |b|^|a|, т. Е. |b| в степени |a|, поэтому forall r. (a -> r) -> r имеет мощность |r|^(|r|^|a|). Как это может быть равно |a|?

Я в замешательстве. Спасибо за любые советы!

Answer 1

Кардинальность на самом деле не может быть определена при наличии полиморфных c типов. В настоящее время понятно, что полиморфные типы c «не являются множествами», как может показаться на первый взгляд. Известный новаторский аргумент Рейнольдса был приведен в его статье «Полиморфизм не является теорией множеств c», доказывая, что мы не можем просто интерпретировать типы с множествами «тривиальным» способом и получить осмысленное представление.

Действительно, в наборах 2^K и K - разные кардиналы, первый из которых больше. Точно так же 2^(2^K) больше K. Тем не менее, F X = 2^(2^X) (напоминающий F a = (a -> Bool) -> Bool) образует (ковариантный) функтор, для которого мы можем найти фиксированную точку

newtype T = T ((T -> Bool) -> Bool)

, получая T, являющуюся изоморфным c к 2^(2^T), что не имеет смысла в наборах, именно потому, что они не могут иметь одинаковую мощность.

(Приведенный выше тип T может быть получен даже без рекурсивных типов при наличии полиморфизма посредством кодировки как forall a. (F a -> a) -> a.)

В любом случае, для выхода из этого тупика нам нужно интерпретировать a -> Bool как нечто иное, чем набор функций 2^a. Возможным решением является использование непрерывных по Скотту функций , как это сделано Скоттом. Аналогичным решением является использование стабильных функций (см. Книгу Жирара «Доказательства и типы»), в которых (если я правильно помню) интерпретации T и T -> Bool имеют одинаковые 1029 * кардинальность (если оба не являются конечными).

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

Answer 2

Аргумент кардинальности на самом деле не работает с полиморфными c типами (см. Ответ @ chi).

Но сам изоморфизм можно интуитивно объяснить следующим образом:

Тип forall r. (a -> r) -> r означает ", если вы дадите мне функцию, которая преобразует a в r, я могу вернуть вам r. О, и я могу сделать это для любого возможного r"

Единственный способ выполнить такое обещание - тайно иметь a в моей руке ,

Поскольку я обещаю сделать это для любого возможного r, это означает, что я ничего не могу знать о самом r, в том числе о том, как построить его значение. И единственное, что у меня есть, это функция a -> r, которую вы мне даете. И единственный способ вызвать такую ​​функцию - дать ей a.

Это означает, что если я даю такое обещание, у меня уже в тайне должно быть a за моей спиной.

---

Для более формального объяснения напомним, что «isomorphi c» в простых терминах означает «может быть однозначно преобразован туда и обратно без потерь». Вот к чему приводит аргумент кардинальности: если у вас одинаковое количество вещей, вы всегда можете организовать пару между ними.

И в своем вопросе вы уже показываете две конверсии: cont конвертирует одну Кстати, unCont преобразует другой. И вы можете тривиально показать, что cont . unCont = unCont . cont = id. Следовательно, типы изоморфны c.

Хотя показание существования двух преобразований является более формальным, я считаю, что не всегда достаточно получить интуицию о том, что два типа действительно "своего рода одно и то же" отсюда и интуитивное объяснение, которое я дал выше.