adjunctions
adjunctions copied to clipboard
Isomorphism `f (Rep r)` and `r ~> f`
There is an isomorphism between f (Rep r)
and natural transformations r ~> f
:
one :: RepresentableOf rep r => Functor f => f rep -> r ~> f
one fins as = index as <$> fins
two :: RepresentableOf rep r => (r ~> f) -> f rep
two make = make positions
positions :: RepresentableOf rep r => r rep
positions = tabulate id
I don't know that it's useful, but there could be some Iso' (f rep) (r ~> f)
.
I got the idea of this isomorphism from Cofree Traversable Functors, where it is instantiated at RepresentableOf (Fin n) (Vec n)
. I'm curious if there is deeper history.
forall x. x -> .. (n-times) .. x -> f x
= Vec n ~> f
= f (Fin n)
I use something like this f (Rep f)
a lot, just to represent endomorphisms Rep f -> Rep f
in a way that can be tabulated. https://www.schoolofhaskell.com/user/edwardk/moore/for-less#running-a-tab in general the f rep form can be "better" simply because it has the option to memoize results. Here to match closer to your phrasing, this is really f (Rep g) ~ (g ~> f)
I just only needed the Endo-like case.