[Haskell-cafe] liftN
Wvv
vitea3v at rambler.ru
Wed Oct 16 21:06:11 UTC 2013
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.
More information about the Haskell-Cafe
mailing list