Yoneda

Yoneda.markdown

import Data.Functor.Yoneda
import Data.Char
import Data.Kind

infixr 5
  ·

type  List :: (Type -> Type) -> Constraint
class List f where
  nil :: f a
  (·) :: a -> f a -> f a

A type class that allows constructing lists

abc :: List f => f Char
abc = 'a'·'b'·'c'·nil

abc can be a String if we provide instance List []. But what happens if we want to map over abc as is?

You might think that this requies a Functor constraint

ordAbc :: Functor f => List f => f Int
ordAbc = fmap ord abc

But there is a way to get around that: Data.Functor.Yoneda

Think of Yoneda F as F in the process of being mapped over.

This means Yoneda F A has access to cont

--
--        vvvv
--   fmap cont (as :: F A)
--        ^^^^
--
instance List f => List (Yoneda f) where

  -- No need to map in the empty case
  --   fmap _cont [] = []
  nil :: Yoneda f a
  nil = Yoneda \_cont -> nil

  -- As we cons, we apply 'cont' to the head
  --   fmap cont (a:as) = cont(a) : fmap cont as
  (·) :: a -> Yoneda f a -> Yoneda f a
  a · Yoneda as = Yoneda \cont ->
    cont(a) · as cont

Now we have the ability to map over forall f. List f => f a without explicitly using fmap or assuming a Functor f instance at any point. The mapping is built into the List (Yoneda f) instance.

We map over abc :: forall f. List f => f Char by instantiating f as Yoneda g. Ignoring the newtype, this turns 'a'·'b'·'c'·nil into \cont -> cont 'a'·cont 'b'·cont 'c'·nil.

>> :t abc @(Yoneda _)
.. :: List g => Yoneda g Char

then using runYoneda

>> :t runYoneda abc
List g => (Char -> xx) -> g xx

Now we just pass ord as an argument and we have successfully mapped over abc

ordAbc' :: List g => g Int
ordAbc' = runYoneda abc ord

as if we had written abc already mapped, and then passed it ord

runYonedaAbc :: List f => (Char -> xx) -> f xx
runYonedaAbc f = f 'a'· f 'b'· f 'c'·nil

Let's talk about abc :: forall f. List f => f Char, and give its type a name.

newtype Build :: ((k -> Type) -> Constraint) -> (k -> Type) where
  MkBuild :: (forall zz. cls zz => zz a) -> Build cls a

abcBuild :: Build List Char
abcBuild = MkBuild abc

and now we can define Build List as a Functor

instance Functor (Build List) where
  fmap :: (a -> a') -> (Build List a -> Build List a')
  fmap f (MkBuild as) = MkBuild (if | Yoneda yo <- as -> yo f)

This means we can map ord over abcBuild while being polymorphic about the underlying structure zz

abcBuild :: Build List Char
abcBuild = MkBuild abc

abcOrdBuild :: Build List Int
abcOrdBuild = fmap ord abcBuild

Using the brand-new extension -XQuantifiedConstraints we can define a Functor for any type class that "lifts" over Yoneda (cls f => cls (Yoneda f))

-- Implies :: Constraint -> Constraint -> Constraint
class    (a => b) => Implies a b
instance (a => b) => Implies a b

-- Lifting :: (k -> Constraint) -> (k -> k) -> Constraint
class    (forall xx. p xx `Implies` p (f xx)) => Lifting p f
instance (forall xx. p xx `Implies` p (f xx)) => Lifting p f

instance Lifting @(Type -> Type) cls Yoneda => Functor (Build cls) where
  fmap :: (a -> a') -> (Build cls a -> Build cls a')
  fmap f (MkBuild as) = MkBuild (if | Yoneda yo <- as -> yo f)

The @(Type -> Type) uses the yet unreleased visible kind applications.

If you understand

fmap :: Functor f => (a -> x) -> (f a -> f x)

then flip fmap returns Yoneda f a

                                 vvvvvvvvvvvvvvvvvvvvvvvvv
flip fmap :: Functor f => f a -> forall x. (a -> x) -> f x
                                 ^^^^^^^^^^^^^^^^^^^^^^^^^

type Yo f a = (forall x. (a -> x) -> f x)

flip fmap :: Functor f => f a -> Yo f a

Reddit discussion https://www.reddit.com/r/haskell/comments/9ykkkc/code_yoneda_stuff/

This is also possible for Data.Functor.Contravariant.Coyoneda

instance Nil f => Nil (Co_Yoneda f) where
 nil :: Co_Yoneda f a
 nil = Co_Yoneda (\_ -> nil)

instance Cons f => Cons (Co_Yoneda f) where
 (·) :: a -> Co_Yoneda f a -> Co_Yoneda f a
 a · Co_Yoneda as = Co_Yoneda (\f -> f a · as f)

-- and CONTRAvariant Coyoneda

instance Nil f => Nil (Contra_Coyoneda f) where
 nil :: Contra_Coyoneda f a
 nil = Contra_Coyoneda id nil

instance Cons f => Cons (Contra_Coyoneda f) where
 (·) :: a -> Contra_Coyoneda f a -> Contra_Coyoneda f a
 (·) a = over (\f as -> f a · as)