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

This looks much better! I don't know why I didn't find it, I did experiment with type classes a bit... Regards, Erik On Tue, Mar 31, 2015 at 10:59 AM, Hiromi ISHII wrote:

Hi Michael, Erik,

...

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

I think we can do it with 'constraints' package using type class as below:

```haskell import Control.Monad.Trans.Control (MonadTransControl (liftWith), StT) import Control.Monad.Trans.Reader (ReaderT) import Data.Constraint ((:-), (\\)) import Data.Constraint.Forall (Forall, inst)

class (StT t a ~ a) => Identical t a instance (StT t a ~ a) => Identical t a

type Unliftable t = Forall (Identical t)

newtype Unlift t = Unlift { unlift :: forall n b. Monad n => t n b -> n b }

mkUnlift :: forall t m a . (Forall (Identical t), Monad m) => (forall n b. Monad n => t n b -> n (StT t b)) -> t m a -> m a mkUnlift r act = r act \\ (inst :: Forall (Identical t) :- Identical t a)

askRunG :: forall t m. (MonadTransControl t, Unliftable t, Monad m) => t m (Unlift t) askRunG = liftWith unlifter where unlifter :: (forall n b. Monad n => t n b -> n (StT t b)) -> m (Unlift t) unlifter r = return $ Unlift (mkUnlift r)

askRun :: Monad m => ReaderT a m (Unlift (ReaderT a)) askRun = askRunG ```

This compiles successfuly in my environment, and things seems to be done correctly, because we can derive ReaderT version from `askRunG`.

In above, we defined `Unliftable t` constraint sysnonym for `Forall (Identical t)` just for convenience. Using this constraint synonym needs `ConstraintKinds` even for library users, it might be appropreate to define it as follows:

``` class Forall (Identical t) => Unliftable t instance Forall (Identical t) => Unliftable t ```

This definiton is the same trick as `Identical` constraint. We can choose which case to take for `Unliftable`, but `Identical` type class should be defined in this way, to get `Forall` works correctly. (This is due to 'constarints' package's current implementation; don't ask me why :-))

...

2015/03/31 15:32、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 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 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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

----- 石井 大海 --------------------------- konn.jinro@gmail.com 筑波大学数理物質科学研究科 数学専攻 博士前期課程一年 ----------------------------------------------

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe