haskellgadtnewtypehigher-rank-types

Coyoneda hasn't a higher-rank type but what type has it actually?


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.


Solution

  • 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.