Как построить значения типа Койонеды более высокого ранга в CPS?

#haskell #unification #higher-rank-types

Вопрос:

 {-# LANGUAGE RankNTypes #-}

newtype Coyoneda f a = Coyoneda {
  uncoyo :: forall b r. ((b -> a) -> f b -> r) -> r
}

coyoneda f tx = Coyoneda (k -> k f tx)

Я думаю Coyoneda , что должен работать, моделируя экзистенциалы с типом более высокого ранга, но мне не удается построить значения этого типа. coyoneda Вспомогательная функция не проверяет тип, потому что в отношении термина k f tx переменная типа более высокого ранга b выйдет за пределы ее области действия.

Однако я не могу придумать другого способа реализации coyoneda . Возможно ли это вообще?

Ответ №1:

Тип T изоморфен

 forall r . (T -> r) -> r

по изоморфизму Йонеды.

В вашем случае,

 forall b r. ((b -> a) -> f b -> r) -> r
~=  -- adding explicit parentheses
forall b . (forall r. ((b -> a) -> f b -> r) -> r)
~=  -- uncurrying
forall b . (forall r. ((b -> a, f b) -> r) -> r)
~=  -- Yoneda
forall b . (b -> a, f b)

а это не то, чего ты хотел. Чтобы использовать coyoneda, вместо этого вам нужно смоделировать экзистенциальный тип:

 exists b . (b -> a, f b)

Итак, давайте превратим это в forall

 exists b . (b -> a, f b)
~=  -- Yoneda
forall r . ((exists b . (b -> a, f b)) -> r) -> r
~=  -- exists on the left side of -> becomes a forall
forall r . (forall b . (b -> a, f b) -> r) -> r
~=  -- currying
forall r . (forall b . (b -> a) -> f b -> r) -> r

Следовательно, это правильная кодировка, которую вам нужно использовать в своем Coyoneda определении.

Ответ №2:

Это newtype не совсем правильно. Следующие работы:

 newtype Coyoneda f a = Coyoneda {
  uncoyo :: forall r. (forall b. (b -> a) -> f b -> r) -> r
}

coyoneda f g = Coyoneda (k -> k f g)