О вложенных типах подвески CPS

(частичный ответ)

Я не удивлюсь, если a окажется изоморфным предложенному вами типу.

forall r. (((a -> r) -> r) -> r) -> r

До сих пор мне удалось только доказать, что первое встраивается во второе. Вложение также может быть изоморфизмом, но если это так, чтобы доказать, что нам, вероятно, потребуется использовать параметричность на страшном типе выше.

Вот вложение:

type YD a = forall r. (((a -> r) -> r) -> r) -> r

ydosi :: a -> YD a
ydosi x = \f -> f (\g -> g x)

ydiso :: YD a -> a
ydiso x = x (\a -> a id)

Доказать, что это вложение, легко, и для этого требуются только бета-шаги:

ydiso (ydosi x)
= ydiso (\f -> f (\g -> g x))
= (\f -> f (\g -> g x)) (\a -> a id)
= (\a -> a id) (\g -> g x)
= (\g -> g x) id
= id x
= x

Противоположное направление намного сложнее, и (если возможно) следует полагаться на параметричность x :: YD a. Завершение этого докажет желаемый изоморфизм.

ydosi (ydiso x)
= ydosi (x (\a -> a id))
= \f -> f (\g -> g (x (\a -> a id)))
= ????
= x

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

ответ Чи решает проблему, предлагая кандидата на изоморфизм между a и forall r. (((a -> r) -> r) -> r) -> r:

-- If you want to play with these in actual code, make YD a newtype.
type YD a = forall r. (((a -> r) -> r) -> r) -> r

ydosi :: a -> YD a
ydosi x = \kk -> kk (\k -> k x)

ydiso :: YD a -> a
ydiso mm = mm (\m -> m id)

Затем чи доказывает ydiso . ydosi = id, что оставляет направление ydosi . ydiso для рассмотрения.

Теперь, если у нас есть некоторое f и его левое обратное g (g . f = id), из этого легко следует, что f . g . f = f. Если f сюръективно, мы можем «отменить» его справа, что приведет нас к f . g = id (то есть к другому направлению изоморфизма). Если это так, то, учитывая, что у нас есть ydiso . ydosi = id, достаточно установить, что ydosi сюръективно, чтобы доказать изоморфизм. Один из способов разобраться в этом — порассуждать о жителях YD a.

(Хотя я не буду пытаться делать это здесь, я предполагаю, что следующие отрывки можно уточнить, выразив их в терминах правил ввода System F -- см. этот вопрос Math.SE.)

Значение YD A — это функция, которая принимает продолжение:

mm :: forall r. (((A -> r) -> r) -> r) -> r
mm = \kk -> _y
-- kk :: forall r. ((A -> r) -> r) -> r
-- _y :: r

Единственный способ получить здесь результат типа r — применить kk к чему-то:

mm :: forall r. (((A -> r) -> r) -> r) -> r
mm = \kk -> kk _m
-- kk :: forall r. ((A -> r) -> r) -> r
-- _m :: forall r. (A -> r) -> r

Поскольку тип kk полиморфен в r, таким же должен быть и тип _m. Это означает, что мы также знаем, каким должно быть _m, благодаря знакомому изоморфизму A/forall r. (A -> r) -> r:

mm :: forall r. (((A -> r) -> r) -> r) -> r
mm = \kk -> kk (\k -> k _x)
-- kk :: forall r. ((A -> r) -> r) -> r
-- k :: forall r. (A -> r) -> r
-- _x :: A

Однако правая часть выше — это именно ydosi:

mm :: forall r. (((A -> r) -> r) -> r) -> r
mm = ydosi _x
-- _x :: A

Мы только что выяснили, что любое значение forall r. (((A -> r) -> r) -> r) -> r равно ydosi x для некоторого x :: A. Отсюда немедленно следует, что ydosi сюръективно, чего достаточно для доказательства изоморфизма.

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

Как выглядят свидетели изоморфизма вложенной подвески? Если мы определим...

-- The familiar isomorphism.
type Susp a = forall r. (a -> r) -> r

suosi :: a -> Susp a
suosi x = \k -> k x

suiso :: Susp a -> a
suiso m = m id

...мы можем написать...

ydosi . suiso . suiso :: Susp (Susp a) -> YD a
suosi . suosi . ydiso :: YD a -> Susp (Susp a)

... что сводится к:

-- A few type annotations would be necessary to persuade GHC about the types here.
\mm -> \kk -> kk (\k -> k (mm id id)) -- Susp (Susp a) -> YD a
\mm -> \kk -> kk (\k -> k (mm (\m -> m id))) -- YD a -> Susp (Susp a)

Мы можем применить Susp a теорему о свободе к mm в первом свидетеле...

f (mm g) = mm (f . g) -- Free theorem
f (mm id) = mm f

mm id id
($ id) (mm id)
mm ($ id)
mm (\m -> m id)

... и так:

\mm -> \kk -> kk (\k -> k (mm (\m -> m id))) -- Susp (Susp a) -> YD a
\mm -> \kk -> kk (\k -> k (mm (\m -> m id))) -- YD a -> Susp (Susp a)

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