[Haskell-cafe] Generalizing "unlift" functions with monad-control
Hiromi ISHII
konn.jinro at gmail.com
Tue Mar 31 08:59:52 UTC 2015
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 <michael at snoyman.com> のメール：
>
> 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
> >
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
----- 石井 大海 ---------------------------
konn.jinro at gmail.com
筑波大学数理物質科学研究科
数学専攻 博士前期課程一年
----------------------------------------------
More information about the Haskell-Cafe
mailing list