adjunctions

adjunctions copied to clipboard

Any instance of Representable admits an automatically derivable left-adjoint in Haskell (That's how I'm reading this, at least). It is basically a generalization of the (,) r -| (->) r adjunction, as (,) (Rep u) -| (->) (Rep u), essentially.

instance Representable u => Adjunction ((,) (Rep u)) u where
    unit x = tabulate (,x)
    counit (i, x) = index x i

We can also convert to and from this representation with any "official" left-adjoint:

fromAuto :: Adjunction f u => (Rep u, a) -> f a
fromAuto (i, x) = index (unit x) i

-- this implementation i am a little less certain about
toAuto :: Adjunction f u => f a -> (Rep u, a)
toAuto x = (indexAdjunction (tabulate id) i, y)
  where
    (y, i) = splitL x

This patch adds a newtype wrapper and data type:

newtype RepAdjunction u a = RepAdjunction (u a)
data TaggedRep u a = TaggedRep (Rep u) a

instance Representable u => Adjunction (TaggedRep u) (RepAdjunction u)

allows people to utilize this automatically derived adjunction, as well as functions for converting between any Adjunction f u => f a and TaggedRep a, if it is useful for interop between the Adjunction and Representable instances.