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

В книге Thinkingwithtypes.com/" rel="noreferrer">Thinking with Types 6.4 Continuation Monad говорится, что типы a и forall r. (a -> r) -> r изоморфны, что подтверждается следующими функциями :

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

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

В этой книге говорится, что любые два типа, имеющие одинаковую мощность, всегда будут изоморфны друг другу. Поэтому я пытаюсь выяснить мощность типов 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|?

Я смущен. Спасибо за любые советы!


types haskell isomorphism
person Z-Y.L    schedule 15.02.2020    source источник
comment
Я не эксперт в этом и не могу полностью объяснить это, но я считаю, что основная часть, которую вы упускаете, это то, что forall r. a явно не изоморфен (a -> r) -> r для любого конкретного r, но это не то, что используют cont и unCont .   -  person Robin Zigmond    schedule 15.02.2020
comment
Вы, кажется, невнимательно прочитали книгу. Если A истинно, то B истинно, не обязательно означает, что если B истинно, то A истинно. Не все прямоугольники являются квадратами, но все квадраты являются прямоугольниками.   -  person 4castle    schedule 15.02.2020
comment
@4castle, хотя это, конечно, правда, здесь это не имеет значения, потому что, хотя это и не указано в ОП, совершенно очевидно, что типы, изоморфные друг другу, действительно будут иметь одинаковую мощность.   -  person Robin Zigmond    schedule 15.02.2020
comment
Что ж, тип t и тип forall x. t не обязательно имеют одинаковую кардинальность. Итак, вы рассчитали правильную кардинальность для (a -> r) -> r, но не для forall r. (a -> r) -> r.   -  person Daniel Wagner    schedule 15.02.2020

Ответы (2)


arrow_upward
7
arrow_downward

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

Но сам изоморфизм можно интуитивно объяснить так:

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

Единственный способ выполнить такое обещание — тайно держать в руке a.

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

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

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

И в вашем вопросе вы уже показываете две конверсии: cont конвертирует в одну сторону, unCont конвертирует в другую. И можно банально показать, что cont . unCont = unCont . cont = id. Поэтому типы изоморфны.

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

person Fyodor Soikin    schedule 15.02.2020
comment
вы можете тривиально показать, что cont . unCont = unCont . cont = id мне трудно показать cont . unCont = id из заданных определений. Я получаю cont . unCont $ g = \f -> f (g id), но как это тривиально id? Что мне не хватает? - person Will Ness; 22.02.2020
comment
Вы должны использовать тот факт, что единственная возможная реализация g — применение аргумента к некоторому значению типа a (игнорируя дно). Итак, g = \h -> h a. Затем cont . unCont $ g = \f -> f (g id) = \f -> f (id a) = \f -> f a = g - person Fyodor Soikin; 22.02.2020
comment
хорошо, так что это не тривиально и не строго без формальных экзистенциальных типов или чего-то еще (существует a такое, что ..., или предполагая g h = h a для некоторого a, мы доказываем это ...)? но я понял вашу мысль, спасибо. - person Will Ness; 22.02.2020

arrow_upward
9
arrow_downward

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

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

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

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

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

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

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

person chi    schedule 15.02.2020
comment
у вас есть какие-нибудь указатели/подсказки, почему forall a. (F a -> a) -> a совпадает с T = F T? (или я неправильно понял этот момент?) спасибо. - person Will Ness; 22.02.2020
comment
@WillNess homepages.inf.ed.ac. uk/wadler/papers/free-rectypes/ - person chi; 22.02.2020