[Haskell-cafe] Generalizing "unlift" functions with monad-control
Erik Hesselink
hesselink at gmail.com
Tue Mar 31 09:05:37 UTC 2015
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
More information about the Haskell-Cafe
mailing list