<div dir="ltr">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.<br></div><br><div class="gmail_quote">On Tue, Mar 31, 2015 at 12:06 PM Erik Hesselink <<a href="mailto:hesselink@gmail.com">hesselink@gmail.com</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">This looks much better! I don't know why I didn't find it, I did<br>
experiment with type classes a bit...<br>
<br>
Regards,<br>
<br>
Erik<br>
<br>
On Tue, Mar 31, 2015 at 10:59 AM, Hiromi ISHII <<a href="mailto:konn.jinro@gmail.com" target="_blank">konn.jinro@gmail.com</a>> wrote:<br>
> Hi Michael, Erik,<br>
><br>
>> The constraints package allows you to define Forall constraints, but<br>
>> that needs something of kind (* -> Constraint) and I can't figure out<br>
>> how to get something like (b ~ StT t b) in that form: we don't have<br>
>> 'data constraints'.<br>
><br>
> I think we can do it with 'constraints' package using type class as below:<br>
><br>
> ```haskell<br>
> import Control.Monad.Trans.Control (MonadTransControl (liftWith), StT)<br>
> import Control.Monad.Trans.Reader (ReaderT)<br>
> import Data.Constraint ((:-), (\\))<br>
> import Data.Constraint.Forall (Forall, inst)<br>
><br>
> class (StT t a ~ a) => Identical t a<br>
> instance (StT t a ~ a) => Identical t a<br>
><br>
> type Unliftable t = Forall (Identical t)<br>
><br>
> newtype Unlift t = Unlift { unlift :: forall n b. Monad n => t n b -> n b }<br>
><br>
> mkUnlift :: forall t m a . (Forall (Identical t), Monad m)<br>
> => (forall n b. Monad n => t n b -> n (StT t b)) -> t m a -> m a<br>
> mkUnlift r act = r act \\ (inst :: Forall (Identical t) :- Identical t a)<br>
><br>
> askRunG :: forall t m. (MonadTransControl t, Unliftable t, Monad m) => t m (Unlift t)<br>
> askRunG = liftWith unlifter<br>
> where<br>
> unlifter :: (forall n b. Monad n => t n b -> n (StT t b)) -> m (Unlift t)<br>
> unlifter r = return $ Unlift (mkUnlift r)<br>
><br>
> askRun :: Monad m => ReaderT a m (Unlift (ReaderT a))<br>
> askRun = askRunG<br>
> ```<br>
><br>
> This compiles successfuly in my environment, and things seems to be done correctly,<br>
> because we can derive ReaderT version from `askRunG`.<br>
><br>
> In above, we defined `Unliftable t` constraint sysnonym for `Forall (Identical t)` just for convenience.<br>
> Using this constraint synonym needs `ConstraintKinds` even for library users, it might be<br>
> appropreate to define it as follows:<br>
><br>
> ```<br>
> class Forall (Identical t) => Unliftable t<br>
> instance Forall (Identical t) => Unliftable t<br>
> ```<br>
><br>
> This definiton is the same trick as `Identical` constraint.<br>
> We can choose which case to take for `Unliftable`, but `Identical` type class<br>
> should be defined in this way, to get `Forall` works correctly.<br>
> (This is due to 'constarints' package's current implementation;<br>
> don't ask me why :-))<br>
><br>
>> 2015/03/31 15:32、Michael Snoyman <<a href="mailto:michael@snoyman.com" target="_blank">michael@snoyman.com</a>> のメール：<br>
>><br>
>> 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.<br>
>><br>
>> On Mon, Mar 30, 2015 at 10:42 PM Erik Hesselink <<a href="mailto:hesselink@gmail.com" target="_blank">hesselink@gmail.com</a>> wrote:<br>
>> Hi Michael,<br>
>><br>
>> The problem seems to be that the constraint you want isn't (b ~ StT t<br>
>> b) for some specific b, you want (forall b. b ~ StT t b). It's not<br>
>> possible to say this directly, but after some trying I got something<br>
>> ugly that works. Perhaps it can be the inspiration for something<br>
>> nicer?<br>
>><br>
>> {-# LANGUAGE RankNTypes #-}<br>
>> {-# LANGUAGE KindSignatures #-}<br>
>> {-# LANGUAGE GADTs #-}<br>
>> {-# LANGUAGE ScopedTypeVariables #-}<br>
>><br>
>> import Control.Monad.Trans.Control<br>
>> import Control.Monad.Trans.Reader<br>
>><br>
>> newtype Unlift t = Unlift { unlift :: forall n b. Monad n => t n b -> n b }<br>
>><br>
>> newtype ForallStId t = ForallStId (forall a. StTEq t a)<br>
>><br>
>> data StTEq (t :: (* -> *) -> * -> *) a where<br>
>> StTEq :: a ~ StT t a => StTEq t a<br>
>><br>
>> askRun :: Monad m => ReaderT r m (Unlift (ReaderT r))<br>
>> askRun = liftWith (return . Unlift)<br>
>><br>
>> askRunG :: forall t m.<br>
>> ( MonadTransControl t<br>
>> , Monad m<br>
>> )<br>
>> => ForallStId t -> t m (Unlift t)<br>
>> askRunG x = liftWith $ \runT -><br>
>> return $ Unlift ( (case x of ForallStId (StTEq :: StTEq t b) -><br>
>> runT) :: forall b n. Monad n => t n b -> n b )<br>
>><br>
>> askRun' :: Monad m => ReaderT r m (Unlift (ReaderT r))<br>
>> askRun' = askRunG (ForallStId StTEq)<br>
>><br>
>> The constraints package allows you to define Forall constraints, but<br>
>> that needs something of kind (* -> Constraint) and I can't figure out<br>
>> how to get something like (b ~ StT t b) in that form: we don't have<br>
>> 'data constraints'.<br>
>><br>
>> Hope this helps you along, and please let me know if you find a nicer<br>
>> way to do this.<br>
>><br>
>> Regards,<br>
>><br>
>> Erik<br>
>><br>
>> On Mon, Mar 30, 2015 at 7:33 AM, Michael Snoyman <<a href="mailto:michael@snoyman.com" target="_blank">michael@snoyman.com</a>> wrote:<br>
>> > I'm trying to extract an "unlift" function from monad-control, which would<br>
>> > allow stripping off a layer of a transformer stack in some cases. It's easy<br>
>> > to see that this works well for ReaderT, e.g.:<br>
>> ><br>
>> > {-# LANGUAGE RankNTypes #-}<br>
>> > {-# LANGUAGE TypeFamilies #-}<br>
>> > import Control.Monad.Trans.Control<br>
>> > import Control.Monad.Trans.Reader<br>
>> ><br>
>> > newtype Unlift t = Unlift { unlift :: forall n b. Monad n => t n b -> n b }<br>
>> ><br>
>> > askRun :: Monad m => ReaderT r m (Unlift (ReaderT r))<br>
>> > askRun = liftWith (return . Unlift)<br>
>> ><br>
>> > The reason this works is that the `StT` associated type for `ReaderT` just<br>
>> > returns the original type, i.e. `type instance StT (ReaderT r) m a = a`. In<br>
>> > theory, we should be able to generalize `askRun` to any transformer for<br>
>> > which that applies. However, I can't figure out any way to express that<br>
>> > generalized type signature in a way that GHC accepts it. It seems like the<br>
>> > following should do the trick:<br>
>> ><br>
>> > askRunG :: ( MonadTransControl t<br>
>> > , Monad m<br>
>> > , b ~ StT t b<br>
>> > )<br>
>> > => t m (Unlift t)<br>
>> > askRunG = liftWith (return . Unlift)<br>
>> ><br>
>> > However, I get the following error message when trying this:<br>
>> ><br>
>> > foo.hs:11:12:<br>
>> > Occurs check: cannot construct the infinite type: b0 ~ StT t b0<br>
>> > The type variable ‘b0’ is ambiguous<br>
>> > In the ambiguity check for the type signature for ‘askRunG’:<br>
>> > askRunG :: forall (t :: (* -> *) -> * -> *) (m :: * -> *) b.<br>
>> > (MonadTransControl t, Monad m, b ~ StT t b) =><br>
>> > t m (Unlift t)<br>
>> > To defer the ambiguity check to use sites, enable AllowAmbiguousTypes<br>
>> > In the type signature for ‘askRunG’:<br>
>> > askRunG :: (MonadTransControl t, Monad m, b ~ StT t b) =><br>
>> > t m (Unlift t)<br>
>> ><br>
>> > Adding AllowAmbiguousTypes to the mix provides:<br>
>> ><br>
>> > foo.hs:17:30:<br>
>> > Could not deduce (b1 ~ StT t b1)<br>
>> > from the context (MonadTransControl t, Monad m, b ~ StT t b)<br>
>> > bound by the type signature for<br>
>> > askRunG :: (MonadTransControl t, Monad m, b ~ StT t b) =><br>
>> > t m (Unlift t)<br>
>> > at foo.hs:(12,12)-(16,25)<br>
>> > ‘b1’ is a rigid type variable bound by<br>
>> > the type forall (n1 :: * -> *) b2.<br>
>> > Monad n1 =><br>
>> > t n1 b2 -> n1 (StT t b2)<br>
>> > at foo.hs:1:1<br>
>> > Expected type: Run t -> Unlift t<br>
>> > Actual type: (forall (n :: * -> *) b. Monad n => t n b -> n b)<br>
>> > -> Unlift t<br>
>> > Relevant bindings include<br>
>> > askRunG :: t m (Unlift t) (bound at foo.hs:17:1)<br>
>> > In the second argument of ‘(.)’, namely ‘Unlift’<br>
>> > In the first argument of ‘liftWith’, namely ‘(return . Unlift)’<br>
>> ><br>
>> > I've tested with both GHC 7.8.4 and 7.10.1. Any suggestions?<br>
>> ><br>
>> > ______________________________<u></u>_________________<br>
>> > Haskell-Cafe mailing list<br>
>> > <a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
>> > <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank">http://mail.haskell.org/cgi-<u></u>bin/mailman/listinfo/haskell-<u></u>cafe</a><br>
>> ><br>
>> ______________________________<u></u>_________________<br>
>> Haskell-Cafe mailing list<br>
>> <a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
>> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank">http://mail.haskell.org/cgi-<u></u>bin/mailman/listinfo/haskell-<u></u>cafe</a><br>
><br>
> ----- 石井 大海 ---------------------------<br>
> <a href="mailto:konn.jinro@gmail.com" target="_blank">konn.jinro@gmail.com</a><br>
> 筑波大学数理物質科学研究科<br>
> 数学専攻 博士前期課程一年<br>
> ------------------------------<u></u>----------------<br>
><br>
> ______________________________<u></u>_________________<br>
> Haskell-Cafe mailing list<br>
> <a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank">http://mail.haskell.org/cgi-<u></u>bin/mailman/listinfo/haskell-<u></u>cafe</a><br>
______________________________<u></u>_________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank">http://mail.haskell.org/cgi-<u></u>bin/mailman/listinfo/haskell-<u></u>cafe</a><br>
</blockquote></div>