search

ekmett / adjunctions

Simple adjunctions
http://hackage.haskell.org/package/adjunctions
Other
44 stars 27 forks source link

Isomorphism `f (Rep r)` and `r ~> f` #75

Open Icelandjack opened 1 year ago

Icelandjack commented 1 year ago

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)
ekmett commented 1 year ago

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.