{-# 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?
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.