Hi all, I'm trying to write a monad transformer class called MonadPCont, for partial continuations, which fits in with the Control.Monad libraries. I'm having a typing problem. What I have so far looks like this: -------------------- module MonadPCont where import Control.Monad import Control.Monad.Cont import Control.Monad.Trans import Control.Monad.Reader import Control.Monad.Writer import Control.Monad.State import Control.Monad.RWS class (Monad (mc a), Monad (mc r)) => MonadPCont mc a r where shift :: ((forall b. Monad (mc b) => a -> mc b r) -> mc r r) -> mc r a reset :: mc a a -> mc r a instance MonadPCont Cont a r where shift f = Cont (\c -> runCont (f (\x -> Cont (\c' -> c' (c x)))) id) reset m = Cont (\c -> c (runCont m id)) type ContT' m r a = ContT r m a instance Monad m => MonadPCont (ContT' m) a r where shift f = ContT (\c -> runContT (f (\x -> ContT (\c' -> c x >>= c'))) return) reset m = ContT (\c -> runContT m return >>= c) -------------------- The error I get is: MonadPCont.hs:21: Type synonym `ContT'' should have 3 arguments, but has been given 1 In the instance declaration for `MonadPCont (ContT' m) i o' Failed, modules loaded: none. I guess it's not possible to partially apply a synonym for a type constructor. Essentially, I'm trying to do a 'flip', but at the type level. The underlying problem is that ContT is written to take the final result type (call it 'r') as the first parameter, and the underlying monad (call it 'm') as the second parameter, e.g. 'ContT r m a'. This is done so that 'ContT r' can be made an instance of the MonadTrans class. Unfortunately, I need 'PI r -> ContT r m', along with a and r, to be a member of the MonadPCont class (PI is the type binding operator). So I thought I'd define ContT' to take the arguments the other way around. Unfortunately, it can't be partially applied. Any ideas, or is it just not feasible to work this class into the library? Thanks, Lyle Kopnicky
On 2004-08-30T17:09:39-0700, Lyle Kopnicky wrote:
Unfortunately, I need 'PI r -> ContT r m', along with a and r, to be a member of the MonadPCont class (PI is the type binding operator). So I thought I'd define ContT' to take the arguments the other way around. Unfortunately, it can't be partially applied.
What's your definition of PI? I suspect you simply need to define a newtype that wraps around 'PI r -> ContT r m'. See also: Wadler, Philip L. 1994. Monads and composable continuations. Lisp and Symbolic Computation 7(1): 39-56. http://homepages.inf.ed.ac.uk/wadler/topics/monads.html#composable -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig Green-Rainbow Party of Massachusetts http://www.green-rainbow.org/ Rich Zitola for Massachusetts State Senate (Worcester and Middlesex District) http://www.vote-zitola.org/
Sorry, I don't think I made myself clear. I'm not defining PI, it's the standard type binding operator, like lambda is the variable binding operator. Maybe I could write it as 'II' so it looks more like a capital pi. It's not a feature of Haskell, but part of type theory (dependent types). I was mixing and matching and making it look like Haskell. So instead of 'PI r -> ContT r m', I could write 'flip ContT', except that 'flip' needs to work on a type level instead of a value level. Or I could write '(`ContT` m)', or 'ContT _ m', where the '_' is a hole. Does this make sense now? Regards, Lyle Kopnicky Chung-chieh Shan wrote:
On 2004-08-30T17:09:39-0700, Lyle Kopnicky wrote:
Unfortunately, I need 'PI r -> ContT r m', along with a and r, to be a member of the MonadPCont class (PI is the type binding operator). So I thought I'd define ContT' to take the arguments the other way around. Unfortunately, it can't be partially applied.
What's your definition of PI? I suspect you simply need to define a newtype that wraps around 'PI r -> ContT r m'.
See also:
Wadler, Philip L. 1994. Monads and composable continuations. Lisp and Symbolic Computation 7(1): 39-56. http://homepages.inf.ed.ac.uk/wadler/topics/monads.html#composable
------------------------------------------------------------------------
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
On 2004-08-31T09:55:10-0700, Lyle Kopnicky wrote:
Sorry, I don't think I made myself clear. I'm not defining PI, it's the standard type binding operator, like lambda is the variable binding operator. Maybe I could write it as 'II' so it looks more like a capital pi. It's not a feature of Haskell, but part of type theory (dependent types). I was mixing and matching and making it look like Haskell. So instead of 'PI r -> ContT r m', I could write 'flip ContT', except that 'flip' needs to work on a type level instead of a value level. Or I could write '(`ContT` m)', or 'ContT _ m', where the '_' is a hole. Does this make sense now?
Yes, it makes sense now. You need to define newtype FlipContT m r a = FlipContT (ContT r m a) or more generally, newtype Flip c (m :: * -> *) r a = Flip (c r m a) The rationale for disallowing matching partially-applied type synonyms is that higher-order unification is undecidable. See also: Neubauer, Matthias, and Peter Thiemann. 2002. Type classes with more higher-order polymorphism. In ICFP '02: Proceedings of the ACM international conference on functional programming. New York: ACM Press. http://www.informatik.uni-freiburg.de/~neubauer/papers/icfp02.pdf http://www.informatik.uni-freiburg.de/~neubauer/papers/icfp02.ps.gz -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig Haskell: lazy, yet functional. http://haskell.org/ Aqsis: RenderMan for free. http://aqsis.com/
On Tue, 2004-08-31 at 10:00, Chung-chieh Shan wrote:
The rationale for disallowing matching partially-applied type synonyms is that higher-order unification is undecidable.
Higher-order unification is worse than just undecidable (after all, GHC's extended Haskell already includes constructs which are undecidable, which means that sometimes the compiler will loop forever); it's ambiguous. There can be multiple unifiers, none of which is the most general. See my earlier Haskell-cafe message for the trouble this can cause (search for "<technical note>"): http://www.haskell.org/pipermail/haskell-cafe/2004-March/005965.html Carl Witty
Yeah, here's a program which causes GHC to hang on compilation, but causes no problem for hugs. Does this qualify as higher-order unification? newtype X a = X (X a -> a) selfapp :: X a -> a selfapp self@(X f) = f self omega :: a omega = selfapp (X selfapp) loop = omega :: () y f = (f . selfapp) (X (f . selfapp)) fact0 f n = if n==0 then 1 else n * f (n-1) fact = y fact0 -- Lyle Kopnicky Carl Witty wrote:
On Tue, 2004-08-31 at 10:00, Chung-chieh Shan wrote:
The rationale for disallowing matching partially-applied type synonyms is that higher-order unification is undecidable.
Higher-order unification is worse than just undecidable (after all, GHC's extended Haskell already includes constructs which are undecidable, which means that sometimes the compiler will loop forever); it's ambiguous. There can be multiple unifiers, none of which is the most general. See my earlier Haskell-cafe message for the trouble this can cause (search for "<technical note>"):
http://www.haskell.org/pipermail/haskell-cafe/2004-March/005965.html
Carl Witty
Chung-chieh, Well, I tried what you suggested, and it seems to work. Unfortunately, it's not very useful. The point of creating MonadPCont, was, like MonadCont or MonadState, to automatically provide features to a monad built from a transformer, without having to redefine them. Since ContT is the monad transformer, I want any monad created from it to automatically support the MonadPCont operations. But they can't, because I can't make ContT an instance of MonadPCont. I can make FlipContT an instance of MonadPCont, but I can't make FlipContT a monad transformer. So what you have to do is create your layered monadwith ContT on top, and then apply the FlipCont constructor to get a monad with the methods of MonadPCont. Now since FlipContT isn't a monad transformer, you can't lift things into it. You can lift them into ContT and then write a wrapper around that. My point is that, unfortunately, I don't think it's very practical to create this type class. I think the problem is that, although MonadCont attempts to describe a monad as having certain operations, MonadPCont attempts to describe a group of related monads as having certain operations. They are related by being formed from the same type constructor. Here's the modified code: module MonadPCont where import Control.Monad import Control.Monad.Cont import Control.Monad.Trans import Control.Monad.Reader import Control.Monad.Writer import Control.Monad.State import Control.Monad.RWS class (Monad (mc a), Monad (mc r)) => MonadPCont mc a r where shift :: ((forall b. Monad (mc b) => a -> mc b r) -> mc r r) -> mc r a reset :: mc a a -> mc r a instance MonadPCont Cont a r where shift f = Cont (\c -> runCont (f (\x -> Cont (\c' -> c' (c x)))) id) reset m = Cont (\c -> c (runCont m id)) data FlipContT m r a = FlipContT { unFlipContT :: (ContT r m a)} instance Monad m => Monad (FlipContT m r) where return x = FlipContT $ return x (FlipContT m') >>= f = FlipContT $ m' >>= (unFlipContT . f) runFlipContT :: FlipContT m r a -> (a -> m r) -> m r runFlipContT (FlipContT m) = runContT m instance Monad m => MonadPCont (FlipContT m) a r where shift f = FlipContT $ ContT $ \c -> runFlipContT (f (\x -> FlipContT $ ContT $ \c' -> c x
= c')) return reset m = FlipContT $ ContT $ \c -> runFlipContT m return >>= c
- Lyle Chung-chieh Shan wrote:
On 2004-08-31T09:55:10-0700, Lyle Kopnicky wrote:
Sorry, I don't think I made myself clear. I'm not defining PI, it's the standard type binding operator, like lambda is the variable binding operator. Maybe I could write it as 'II' so it looks more like a capital pi. It's not a feature of Haskell, but part of type theory (dependent types). I was mixing and matching and making it look like Haskell. So instead of 'PI r -> ContT r m', I could write 'flip ContT', except that 'flip' needs to work on a type level instead of a value level. Or I could write '(`ContT` m)', or 'ContT _ m', where the '_' is a hole. Does this make sense now?
Yes, it makes sense now. You need to define
newtype FlipContT m r a = FlipContT (ContT r m a)
or more generally,
newtype Flip c (m :: * -> *) r a = Flip (c r m a)
The rationale for disallowing matching partially-applied type synonyms is that higher-order unification is undecidable.
See also:
Neubauer, Matthias, and Peter Thiemann. 2002. Type classes with more higher-order polymorphism. In ICFP '02: Proceedings of the ACM international conference on functional programming. New York: ACM Press. http://www.informatik.uni-freiburg.de/~neubauer/papers/icfp02.pdf http://www.informatik.uni-freiburg.de/~neubauer/papers/icfp02.ps.gz
participants (3)
-
Carl Witty -
Chung-chieh Shan -
Lyle Kopnicky