[Haskell-cafe] Generalizing "unlift" functions with monad-control

[Michael Snoyman]

Those are some impressive type gymnastics :) Unfortunately, I still don't
think I'm able to write the generic function the way I wanted to, so I'll
be stuck with a typeclass. However, I may be able to provide your helper
types/functions to make it easier for people to declare their own instances.

On Mon, Mar 30, 2015 at 10:42 PM Erik Hesselink <hesselink at gmail.com> wrote:

> Hi Michael,
>
> The problem seems to be that the constraint you want isn't (b ~ StT t
> b) for some specific b, you want (forall b. b ~ StT t b). It's not
> possible to say this directly, but after some trying I got something
> ugly that works. Perhaps it can be the inspiration for something
> nicer?
>
> {-# LANGUAGE RankNTypes #-}
> {-# LANGUAGE KindSignatures #-}
> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE ScopedTypeVariables #-}
>
> import Control.Monad.Trans.Control
> import Control.Monad.Trans.Reader
>
> newtype Unlift t = Unlift { unlift :: forall n b. Monad n => t n b -> n b }
>
> newtype ForallStId t = ForallStId (forall a. StTEq t a)
>
> data StTEq (t :: (* -> *) -> * -> *) a where
>   StTEq :: a ~ StT t a => StTEq t a
>
> askRun :: Monad m => ReaderT r m (Unlift (ReaderT r))
> askRun = liftWith (return . Unlift)
>
> askRunG :: forall t m.
>            ( MonadTransControl t
>            , Monad m
>            )
>         => ForallStId t -> t m (Unlift t)
> askRunG x = liftWith $ \runT ->
>   return $ Unlift ( (case x of ForallStId (StTEq :: StTEq t b) ->
> runT) :: forall b n. Monad n => t n b -> n b )
>
> askRun' :: Monad m => ReaderT r m (Unlift (ReaderT r))
> askRun' = askRunG (ForallStId StTEq)
>
> The constraints package allows you to define Forall constraints, but
> that needs something of kind (* -> Constraint) and I can't figure out
> how to get something like (b ~ StT t b) in that form: we don't have
> 'data constraints'.
>
> Hope this helps you along, and please let me know if you find a nicer
> way to do this.
>
> Regards,
>
> Erik
>
> On Mon, Mar 30, 2015 at 7:33 AM, Michael Snoyman <michael at snoyman.com>
> wrote:
> > I'm trying to extract an "unlift" function from monad-control, which
> would
> > allow stripping off a layer of a transformer stack in some cases. It's
> easy
> > to see that this works well for ReaderT, e.g.:
> >
> > {-# LANGUAGE RankNTypes #-}
> > {-# LANGUAGE TypeFamilies #-}
> > import Control.Monad.Trans.Control
> > import Control.Monad.Trans.Reader
> >
> > newtype Unlift t = Unlift { unlift :: forall n b. Monad n => t n b -> n
> b }
> >
> > askRun :: Monad m => ReaderT r m (Unlift (ReaderT r))
> > askRun = liftWith (return . Unlift)
> >
> > The reason this works is that the `StT` associated type for `ReaderT`
> just
> > returns the original type, i.e. `type instance StT (ReaderT r) m a = a`.
> In
> > theory, we should be able to generalize `askRun` to any transformer for
> > which that applies. However, I can't figure out any way to express that
> > generalized type signature in a way that GHC accepts it. It seems like
> the
> > following should do the trick:
> >
> > askRunG :: ( MonadTransControl t
> >            , Monad m
> >            , b ~ StT t b
> >            )
> >         => t m (Unlift t)
> > askRunG = liftWith (return . Unlift)
> >
> > However, I get the following error message when trying this:
> >
> > foo.hs:11:12:
> >     Occurs check: cannot construct the infinite type: b0 ~ StT t b0
> >     The type variable ‘b0’ is ambiguous
> >     In the ambiguity check for the type signature for ‘askRunG’:
> >       askRunG :: forall (t :: (* -> *) -> * -> *) (m :: * -> *) b.
> >                  (MonadTransControl t, Monad m, b ~ StT t b) =>
> >                  t m (Unlift t)
> >     To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
> >     In the type signature for ‘askRunG’:
> >       askRunG :: (MonadTransControl t, Monad m, b ~ StT t b) =>
> >                  t m (Unlift t)
> >
> > Adding AllowAmbiguousTypes to the mix provides:
> >
> > foo.hs:17:30:
> >     Could not deduce (b1 ~ StT t b1)
> >     from the context (MonadTransControl t, Monad m, b ~ StT t b)
> >       bound by the type signature for
> >                  askRunG :: (MonadTransControl t, Monad m, b ~ StT t b)
> =>
> >                             t m (Unlift t)
> >       at foo.hs:(12,12)-(16,25)
> >       ‘b1’ is a rigid type variable bound by
> >            the type forall (n1 :: * -> *) b2.
> >                     Monad n1 =>
> >                     t n1 b2 -> n1 (StT t b2)
> >            at foo.hs:1:1
> >     Expected type: Run t -> Unlift t
> >       Actual type: (forall (n :: * -> *) b. Monad n => t n b -> n b)
> >                    -> Unlift t
> >     Relevant bindings include
> >       askRunG :: t m (Unlift t) (bound at foo.hs:17:1)
> >     In the second argument of ‘(.)’, namely ‘Unlift’
> >     In the first argument of ‘liftWith’, namely ‘(return . Unlift)’
> >
> > I've tested with both GHC 7.8.4 and 7.10.1. Any suggestions?
> >
> > _______________________________________________
> > Haskell-Cafe mailing list
> > Haskell-Cafe at haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150331/3d19b090/attachment.html>