Yoneda
has a valid type as long as the higher-rank extension is set:
newtype Yoneda f a = Yoneda (forall b. (a -> b) -> f b)
which yields the type (forall b. (a -> b) -> f b) -> Yoneda f a
.
b
is picked by the consumer of Yoneda
and hence doesn't appear on the LHS of the newtype
declaration.
Coyoneda
, however, doesn't make sense to me:
data Coyoneda f a = forall b. Coyoneda (b -> a) (f b)
which yields (b -> a) -> f b -> Coyoneda f a
.
b
is explicitly quantified but the quantifier doesn't seem to be in the right position to render the type variable rank 2. Nonetheless b
isn't listed on the LHS of the data
declaration. So what is it? Almost existential? This is only an uneducated guess, because I don't quite understand existential quantifiers and assume Haskell doesn't support them.
data Coyoneda f a = forall b. Coyoneda (b -> a) (f b)
Can also be written with GADT syntax:
data Coyoneda f a where
Coyoneda :: forall b. (b -> a) -> f b -> Coyoneda f a
The explicit quantification is optional.
Coyoneda :: (b -> a) -> f b -> Coyoneda f a
Coyoneda :: forall f a b. (b -> a) -> f b -> Coyoneda f a
So you got it right: b
is existentially quantified here, since it doesn’t appear in the result type of the Coyoneda
data constructor.