Dan Burton danburton.email at gmail.com
Wed Oct 16 21:32:24 UTC 2013

```My "solution" is a lot less interesting

lift1 = lift
lift2 = lift . lift1
lift3 = lift . lift2
lift4 = lift . lift3
lift5 = lift . lift4

What you want seemingly requires dependent types, because the result type
depends on the Int that you pass in. Haskell is not well equipped to handle
this, though you could probably whip up some Template Haskell to get the
job done for cases where the Int can be determined at compile time.

-- Dan Burton

On Wed, Oct 16, 2013 at 2:06 PM, Wvv <vitea3v at rambler.ru> wrote:

> 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
>      m a -> t (t1 (t2 m)) a
>
> My best solution looks like:
>
> data MT = M | T Int MT
> liftN :: forall tm. ( forall x 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: