Я не совсем уверен в следующем подходе к этому вопросу (вроде бы слишком хорошо, чтобы быть правдой), но это лучшее, что я могу предложить до сих пор, поэтому давайте положим его на стол.
ответ Чи решает проблему, предлагая кандидата изоморфизма между 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)
Удивительно, что свидетели "одинаковы", за исключением их типов. Интересно, если бы какой-то аргумент, начинающийся с этого наблюдения, позволил бы нам вернуться назад и доказать изоморфизм более прямым образом.