Generalizing "unlift" functions with monad-control

older
Is it possible for cabal sandboxes...

Michael Snoyman

30 Mar 2015 30 Mar '15

1:33 a.m.

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?

Attachments:

attachment.html (text/html — 3.5 KB)

Show replies by date

Erik Hesselink

30 Mar 30 Mar

3:42 p.m.

New subject: Generalizing "unlift" functions with monad-control

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

Michael Snoyman

31 Mar 31 Mar

2:32 a.m.

New subject: 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

Hiromi ISHII

4:59 a.m.

New subject: Generalizing "unlift" functions with monad-control

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 筑波大学数理物質科学研究科数学専攻博士前期課程一年 ----------------------------------------------

Erik Hesselink

5:05 a.m.

New subject: 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

Michael Snoyman

11:37 a.m.

New subject: Generalizing "unlift" functions with monad-control

Wow, this looks great, thank you! I have to play around with this a bit more to see how it fits in with everything, I'll ping back this thread when I have something worth sharing. On Tue, Mar 31, 2015 at 12:06 PM Erik Hesselink wrote:

...

This looks much better! I don't know why I didn't find it, I did experiment with type classes a bit...

Regards,

Erik

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

...
...
...
generalized type signature in a way that GHC accepts it. It seems

On Tue, Mar 31, 2015 at 10:59 AM, Hiromi ISHII wrote: that 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

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

Michael Snoyman

5 Apr 5 Apr

8:29 a.m.

New subject: Generalizing "unlift" functions with monad-control

Finally got around to this, and it worked like a charm. Just cleaning up this package, will probably be on Hackage in a few days. On Tue, Mar 31, 2015 at 6:37 PM Michael Snoyman wrote:

...

Wow, this looks great, thank you! I have to play around with this a bit more to see how it fits in with everything, I'll ping back this thread when I have something worth sharing.

On Tue, Mar 31, 2015 at 12:06 PM Erik Hesselink wrote:

...
This looks much better! I don't know why I didn't find it, I did experiment with type classes a bit...

Regards,

Erik

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

...
...
...
generalized type signature in a way that GHC accepts it. It seems

On Tue, Mar 31, 2015 at 10:59 AM, Hiromi ISHII wrote: that 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

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

Hiromi ISHII

31 Mar 31 Mar

5:03 a.m.

New subject: Generalizing "unlift" functions with monad-control

P.S. oops, I missed to attach the appropreate language extensions. You have to specify following exntensions to get my example works: ```haskell {-# LANGUAGE ConstraintKinds, FlexibleContexts, FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses, RankNTypes, ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies, TypeOperators #-} ``` -- Hiromi ISHII konn.jinro@gmail.com

3710

Age (days ago)

3716

Last active (days ago)

List overview

Download

7 comments

3 participants

participants (3)

Erik Hesselink
Hiromi ISHII
Michael Snoyman

Generalizing "unlift" functions with monad-control

tags

participants (3)