A parameter type is existential, a return type is universal, part 4

We saw an adjunction of SomeF and Const in the part 1, and an adjunction of Const and AnyF in the part 2. They’re called an adjoint triple and denoted as SomeF -| Const -| AnyF. Let’s express them as code in Haskell.

We’ll use two categories. First category is Hask where objects are types and morphisms are functions. The second category is Hask^Hask where objects are endofunctors in Hask and morphisms are natural transformations.

First, let’s define some types to express endofunctors in Hask and natural transformations.

type FunctorType :: Type
type FunctorType = Type -> Type

type (~>) :: FunctorType -> FunctorType -> Type
type f ~> g = forall a. f a -> g a

Then, we’ll define two functors. The first functor is a functor from Hask to Hask^Hask. We’ll call it FunctorFromHaskToHask2.

type FunctorFromHaskToHask2Type :: Type
type FunctorFromHaskToHask2Type = Type -> FunctorType

type FunctorFromHaskToHask2 :: FunctorFromHaskToHask2Type -> Constraint
class FunctorFromHaskToHask2 t where
  mapFromHaskToHask2 :: (Functor (t a), Functor (t b)) => (a -> b) -> (t a ~> t b)

This functor maps an object in Hask (Type) to an object in Hask^Hask (FunctorType), and maps a morphism in Hask (Type -> Type) to a morphism in Hask^Hask (FunctorType ~> FunctorType).

The second functor is the opposite; Hask^Hask to Hask. We’ll call it FunctorFromHask2ToHask.

type FunctorFromHask2ToHaskType :: Type
type FunctorFromHask2ToHaskType = FunctorType -> Type

type FunctorFromHask2ToHask :: FunctorFromHask2ToHaskType -> Constraint
class FunctorFromHask2ToHask t where
  mapFromHask2ToHask :: (Functor f, Functor g) => (f ~> g) -> (t f -> t g)

This functor maps an object in Hask^Hask (FunctorType) to an object in Hask (Type), and maps a morphism in Hask^Hask (FunctorType ~> FunctorType) to a morphism in Hask (Type -> Type).

When you have Const,

type Const :: Type -> Type -> Type
newtype Const a b = MkConst a

you can make Const a an instance of Functor.

instance Functor (Const a) where
  fmap :: (b -> c) -> Const a b -> Const a c
  fmap _ (MkConst a) = MkConst a

When you look at the kind of Const, you’ll find its type is Type -> Type -> Type, but it’s identical to Type -> FunctorType. So you can think Const is a functor from Hask to Hask^Hask. Let’s make it an instance of FunctorFromHaskToHask2.

instance FunctorFromHaskToHask2 Const where
  mapFromHaskToHask2 :: (a -> b) -> (Const a ~> Const b)
  mapFromHaskToHask2 a2b = \(MkConst a) -> MkConst (a2b a)

Next, let’s take a look at SomeF.

type SomeF :: FunctorType -> Type
data SomeF f = forall a. MkSomeF (f a)

SomeF is a type that takes a FunctorType. So you can think it’s a functor from Hask^Hask to Hask. Let’s make it an instance of FunctorFromHask2ToHask.

instance FunctorFromHask2ToHask SomeF where
  mapFromHask2ToHask :: (f ~> g) -> (SomeF f -> SomeF g)
  mapFromHask2ToHask f2g = \(MkSomeF fa) -> MkSomeF (f2g fa)

You can do the same with AnyF.

type AnyF :: FunctorType -> Type
newtype AnyF f = MkAnyF (forall a. f a)

instance FunctorFromHask2ToHask AnyF where
  mapFromHask2ToHask :: (f ~> g) -> (AnyF f -> AnyF g)
  mapFromHask2ToHask f2g = \(MkAnyF fa) -> MkAnyF (f2g fa)

Now, we’ve had necessary functors; Const from Hask to Hask^Hask, and SomeF and AnyF from Hask^Hask to Hask. We’ll define two type classes expressing adjunctions. The first one has Hask^Hask to Hask on the left, and Hask to Hask^Hask on the right.

class (FunctorFromHask2ToHask f, FunctorFromHaskToHask2 g) => LeftAdjunction f g | f -> g, g -> f where
  liftLeftAdjunct :: (Functor h) => (f h -> a) -> (h ~> g a)
  leftRightAdjunct :: (Functor h) => (h ~> g a) -> (f h -> a)

The second one has the opposite.

class (FunctorFromHaskToHask2 f, FunctorFromHask2ToHask g) => RightAdjunction f g | f -> g, g -> f where
  liftRightAdjunct :: (Functor h) => (f a ~> h) -> (a -> g h)
  rightLeftAdjunct :: (Functor h) => (a -> g h) -> (f a ~> h)

We can make a pair of SomeF and Const an instance of LeftAdjunction, and a pair of Const and AnyF an instance of RightAdjunction.

instance LeftAdjunction SomeF Const where
  liftLeftAdjunct :: (Functor h) => (SomeF h -> a) -> (h ~> Const a)
  liftLeftAdjunct someH2a = \h -> MkConst (someH2a (MkSomeF h))

  leftRightAdjunct :: (Functor h) => (h ~> Const a) -> (SomeF h -> a)
  leftRightAdjunct h2const = \(MkSomeF h) -> let MkConst a = h2const h in a

instance RightAdjunction Const AnyF where
  liftRightAdjunct :: (Functor h) => (Const a ~> h) -> (a -> AnyF h)
  liftRightAdjunct const2h = \a -> MkAnyF (const2h (MkConst a))

  rightLeftAdjunct :: (Functor h) => (a -> AnyF h) -> (Const a ~> h)
  rightLeftAdjunct a2anyH = \(MkConst a) -> let MkAnyF ha = a2anyH a in ha

In an adjoint triple, there is a forgetful functor in the middle, and a free functor on the left and a cofree functor on the right. A forgetful functor forgets a structure, a free functor creates a minimum structure, and a cofree functor creates a maximum structure.

In this adjoint triple SomeF -| Const -| AnyF, you can think that Const forgets a functor f, SomeF creates a minimum functor that works with some given a, and AnyF creates a maximum functor that works with any given a.