[Haskell-cafe] Generalizing "unlift" functions with monad-control
Erik Hesselink
hesselink at gmail.com
Mon Mar 30 19:42:16 UTC 2015
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
>
More information about the Haskell-Cafe
mailing list