On Sun, Jun 27, 2010 at 7:43 AM, Sjoerd Visscher
Hi Max,
This is really interesting!
1. There exist total functions:
lift :: X d => d a -> D a lower :: X d => D a -> d a
2. And you can write a valid instance:
instance X D
With *no superclass constraints*.
All your examples have a more specific form:
lift :: X d => d a -> D d a lower :: X d => D d a -> d a instance X (D d)
This might help when looking for a matching categorical concept. With your original signatures I was thinking of initial/terminal objects, but that's not the case.
2. Is there a mother of all idioms? By analogy with the previous three examples, I tried this:
-- (<**>) :: forall a. i a -> (forall b. i (a -> b) -> i b) newtype Thingy i a = Thingy { runThingy :: forall b. i (a -> b) -> i b }
But I can't see how to write either pure or <*> with that data type. This version seems to work slightly better:
newtype Thingy i a = Thingy { runThingy :: forall b. Yoneda i (a -> b) -> i b }
Because you can write pure (pure x = Thingy (\k -> lowerYoneda (fmap ($ x) k))). But <*> still eludes me!
It's usually easier to switch to Monoidal functors when playing with Applicative. (See the original Functional Pearl "Applicative programming with effects".)
Then I got this:
newtype Thingy i a = Thingy { runThingy :: forall b. Yoneda i b -> Yoneda i (a, b) }
(&&&) :: Thingy i c -> Thingy i d -> Thingy i (c, d) mf &&& mx = Thingy $ fmap (\(d, (c, b)) -> ((c, d), b)) . runThingy mx . runThingy mf
instance Functor (Thingy i) where fmap f m = Thingy $ fmap (first f) . runThingy m
instance Applicative (Thingy i) where pure x = Thingy $ fmap (x,) mf <*> mx = fmap (\(f, x) -> f x) (mf &&& mx)
Note that Yoneda is only there to make it possible to use fmap without the Functor f constraint. So I'm not sure if requiring no class constraints at all is a good requirement. It only makes things more complicated, without providing more insights.
I'd say that if class X requires a superclass constraint Y, then the instance of X (D d) is allowed to have the constraint Y d. The above code then stays the same, only with Yoneda removed and constraints added.
This is an encoding of the fact that all Functors in Haskell are strong, and that Yoneda i is a Functor for any i :: * -> *. -Edward Kmett