ekmett / kan-extensions

Kan extensions, Kan lifts, the Yoneda lemma, and (co)monads generated by a functor
Other
79 stars 33 forks source link

`lift` for `Codensity` can probably be done with coercions #18

Open treeowl opened 9 years ago

treeowl commented 9 years ago

Prelude: I don't know if it's worth trying to do this, or if the more precise arity analysis is better than theoretical allocation improvements.

We can legally define

instance MonadTrans Codensity where
  lift = frob
frob :: forall m a . Monad m => m a -> Codensity m a
frob = coerce (blah (Mag (>>=)) :: m a -> Mag2 m a)
newtype Mag m a = Mag (forall b . m a -> (a -> m b) -> m b)
newtype Mag2 m a = Mag2 (forall b . (a -> m b) -> m b)
blah :: Mag m a -> m a -> Mag2 m a
blah (Mag p) q = Mag2 (p q)

blah is obviously the identity (up to arity), because all it does is remove a newtype constructor and put a different one on. The effect is to shift the forall b to the right of an arrow; this does not change the run-time representation because type lambdas compile away. Unfortunately, I don't see a way to convince GHC that blah is just a cast. I believe, however, that it should be safe to define blah = unsafeCoerce id.