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.
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.We can also convert to and from this representation with any "official" left-adjoint:
This patch adds a newtype wrapper and data type:
allows people to utilize this automatically derived adjunction, as well as functions for converting between any
Adjunction f u => f a
andTaggedRep a
, if it is useful for interop between theAdjunction
andRepresentable
instances.