[Haskell-cafe] Generalizing "unlift" functions with monad-control
Michael Snoyman
michael at snoyman.com
Sun Apr 5 12:29:33 UTC 2015
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 <michael at snoyman.com> 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 <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/20150405/7f5d22d7/attachment.html>
More information about the Haskell-Cafe
mailing list