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

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 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

...

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

On Mon, Mar 30, 2015 at 7:33 AM, Michael Snoyman wrote: 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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe