Arrow Notation - Command combinators don't work with higher rank types? (GHC 7.4)

[Ben Moseley]

Thanks for the explanation Ross.

> So the limitation is in the design rather than the implementation.
> Is this a major obstacle?  

I don't think so for my use case - I think I'll be able to work around it without too much trouble.

> I appreciate that this was cut down to provide
> a concise report; how important is this in the full application?


The real application is trying to process a structure containing GADTs - something more like this:

{-# LANGUAGE GADTs,Arrows,Rank2Types #-}
import Control.Arrow

data G a where
    G1 :: Int -> G Char
    G2 :: Int -> G Bool

-- mapcomb :: Arrow a => (a (env,G x) (G x)) -> a (env,(G b,G c)) (G b,G c)
-- mapcomb _aegg = proc (_env,bc) -> returnA -< bc

process :: Int -> G x -> G x
process i (G1 n) = G1 $ succ n
process i (G2 n) = G2 $ succ n

processA :: Arrow a => a (Int,G x) (G x)
processA = proc (i,gx) -> returnA -< process i gx

mapcomb :: Arrow a => (forall x . a (env,G x) (G x)) -> a (env,(G b,G c)) (G b,G c)
mapcomb aegg = proc (env,(g1,g2)) -> do
                 g1' <- aegg -< (env,g1)
                 g2' <- aegg -< (env,g2)
                 returnA -< (g1',g2')

myarr :: Arrow a => a Int Bool
myarr = proc i -> do
          (|mapcomb (\g -> processA -< (i,g)) |) (G1 3,G2 3)
          -- (| (mapcomb (processA <<^ (\(_,g)->(7,g)) )) |) (G1 3,G2 3)
          returnA -< False

I guess to do this it'll be necessary to plumb 'i' through manually (changing the type of 'mapcomb') ?

--Ben

On 15 Jan 2012, at 10:21, Ross Paterson wrote:

> On Sun, Jan 15, 2012 at 09:34:35AM +0000, Ben Moseley wrote:
>> Consider the code below:
>> 
>> ----
>> 
>> {-# LANGUAGE Arrows,Rank2Types #-}
>> 
>> import Control.Arrow
>> 
>> -- cmdcomb :: Arrow a => (a (env,x) x) -> a (env,x) x
>> -- cmdcomb aegg = aegg
>> 
>> cmdcomb :: Arrow a => (forall x . a (env,x) x) -> a (env,x) x
>> cmdcomb aegg = aegg
>> 
>> myarr :: Arrow a => a (Int,Bool) Bool
>> myarr = proc (i,b) -> do
>>          (|cmdcomb (\g -> returnA -< g) |) 'x'
>>          -- (| (cmdcomb (arr snd)) |) 'x'
>>          returnA -< False
>> 
>> ----
>> 
>> This code generates the error below (but using either of the commented sections instead gets it to typecheck):
>> 
>> ../MyDev/FPF3/saturday/dm.hs:13:13:
>>    Couldn't match expected type `t0 t1 t2'
>>                with actual type `forall x. a0 (env0, x) x'
>>    Expected type: t0 t1 t2 -> a (a1, t4) t3
>>      Actual type: (forall x. a0 (env0, x) x) -> a0 (env0, x0) x0
>>    In the expression: cmdcomb
>>    In the expression:
>>      proc (i, b) -> do { (|cmdcomb ((\ g -> returnA -< g))|) 'x';
>>                          returnA -< False }
>> Failed, modules loaded: none.
>> 
>> Is this a bug or a limitation in the current implementation?
> 
> It's performing as documented in the User's Guide: "the type of each
> argument of the operator (and its result) should have the form
> 
>    a (...(e,t1), ... tn)
> 
> t where e is a polymorphic variable".  In this case the operator is
> cmdcomb, and the commented-out type has the allowed form, but the given
> one doesn't.  With the second variant uncommented, the operator would be
> 
>    cmdcomb (arr snd) :: Arrow a => a (env,x) x
> 
> which also conforms.
> 
> So the limitation is in the design rather than the implementation.
> Is this a major obstacle?  I appreciate that this was cut down to provide
> a concise report; how important is this in the full application?
> 
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users