16 Oct 23:06 2013

## liftN

Wvv <vitea3v <at> rambler.ru>

2013-10-16 21:06:11 GMT

2013-10-16 21:06:11 GMT

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(Continue reading)