[Haskell-cafe] liftN

[Wvv]

I try to write a function "liftN", but I'm not satisfied with result.

lift :: (MonadTrans t) => Monad m => m a -> t m a

liftN n 
    | n < 1       = error "liftN: n<1"
    | n == 1     = lift
    | otherwise = lift . (liftN (n-1))

1) I know(?), that it is impossible to write liftN now: typechecker can't
decide which signature it is.
2) Main reason is finite recursive constraint

3) Let's think, it is possible to write
Main candidates: promoted data and data-kinds

For example,
lift . lift . lift
  :: (Monad (t1 (t2 m)), Monad (t2 m), Monad m, MonadTrans t,
      MonadTrans t1, MonadTrans t2) =>
     m a -> t (t1 (t2 m)) a

My best solution looks like:

data MT = M | T Int MT
liftN :: forall tm. ( forall x n.
		   Monad 'M, Monad (x :: MT),
		   MonadTrans ('T n),  
         ) => Int -> 'M a ->  ('T 0) (tm :: MT) a
liftN n
     | n < 1     = error "liftN:  n < 1"
     | n == 1    = lift
     | otherwise = lift . (liftN (n-1))


Am I miss something?
I think this function could look much prettier.
But I don't know how.



--
View this message in context: http://haskell.1045720.n5.nabble.com/liftN-tp5738612.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.