How to construct values of a higher-rank Coyoneda type in CPS?

user_5536315 0
Viewed 76
{-# 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)

I think Coyoneda should work by simulating existentials with a higher-rank type, but I fail to construct values of this type. The coyoneda auxiliary function doesn't type check, because with regard to the term k f tx the higher-rank type variable b would escape its scope.

However, I cannot come up with another way to implement coyoneda. Is it possible at all?

unification higher-rank-types haskell
2 Answers

A type T is isomorphic to

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

by the Yoneda isomorphism.

In your case,

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)

which is not what you wanted. To use coyoneda, you need to model an existential type instead:

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

So, let's turn this into a 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

Hence, this is the correct encoding you need to use in your Coyoneda definition.

user_32349590

The newtype is not quite correct. The following works:

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

coyoneda f g = Coyoneda (\k -> k f g)
user_10682320
Related