On Sun, Jan 27, 2013 at 12:20:25AM +0000, Roman Cheplyaka wrote:
Very nice! This can be generalized to arbitrary arrows:
{-# LANGUAGE ExistentialQuantification #-}
import Prelude hiding (id) import Control.Arrow import Control.Applicative import Control.Category
data F from to b c = forall d . F (from b d) (to d c)
instance (Arrow from, Arrow to) => Functor (F from to b) where fmap f x = pure f <*> x
instance (Arrow from, Arrow to) => Applicative (F from to b) where pure x = F (arr $ const x) id F from1 to1 <*> F from2 to2 = F (from1 &&& from2) (to1 *** to2 >>> arr (uncurry id))
You only require that from b is Applicative, so that in turn can be generalized: data F g to c = forall d . F (g d) (to d c) instance (Applicative g, Arrow to) => Functor (F g to) where fmap f x = pure f <*> x instance (Applicative g, Arrow to) => Applicative (F g to) where pure x = F (pure x) id F from1 to1 <*> F from2 to2 = F ((,) <$> from1 <*> from2) (to1 *** to2 >>> arr (uncurry id))
I wonder what's a categorical interpretation of F itself.
It's a variety of left Kan extension (cf section 5 of "Constructing Applicative Functors" at MPC'2012).