[Haskell-cafe] Generalizing "unlift" functions with monad-control
Michael Snoyman
michael at snoyman.com
Tue Mar 31 15:37:31 UTC 2015
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 <hesselink at gmail.com> 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
>
> On Tue, Mar 31, 2015 at 10:59 AM, Hiromi ISHII <konn.jinro at gmail.com>
> 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 <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
> > 筑波大学数理物質科学研究科
> > 数学専攻 博士前期課程一年
> > ----------------------------------------------
> >
> > _______________________________________________
> > 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150331/e6742d18/attachment-0001.html>
More information about the Haskell-Cafe
mailing list