Dear all, in http://www.haskell.org/pipermail/glasgow-haskell-users/2006-January/009565.h... Simon Peyton-Jones asks for programs that are broken by the proposed change. Here is a nearly real world one: {-# OPTIONS_GHC -fglasgow-exts #-} import Control.Monad import Control.Monad.ST import Data.Array.MArray import Data.Array.ST import Data.STRef import Data.Set hiding (map,filter) -- a store that allows to mark keys class Mark m store key | store -> key m where new :: (key,key) -> m store mark :: store -> key -> m () markQ :: store -> key -> m Bool seen :: store -> m [ key ] -- implementation 1 instance Ord key => Mark (ST s) (STRef s (Set key)) key where new _ = newSTRef empty mark s k = modifySTRef s (insert k) markQ s k = liftM (member k) (readSTRef s) seen s = liftM elems (readSTRef s) -- implementation 2 instance Ix key => Mark (ST s) (STUArray s key Bool) key where new bnd = newArray bnd False mark s k = writeArray s k True markQ = readArray seen s = liftM (map fst . filter snd) (getAssocs s) -- traversing the hull suc^*(start) with loop detection trav suc start i = new i >>= \ c -> mapM_ (compo c) start >> return c where compo c x = markQ c x >>= flip unless (visit c x) visit c x = mark c x >> mapM_ (compo c) (suc x) -- sample graph f 1 = 1 : [] f n = n : f (if even n then div n 2 else 3*n+1) t1 = runST (trav f [1..10] (1,52) >>= \ (s::STRef s (Set Int)) -> seen s) t2 = runST (trav f [1..10] (1,52) >>= \ (s::STUArray s Int Bool) -> seen s) In ghc-6.4.2 this works as expected, but ghc-6.5.20061001 says B.hs:40:44: A pattern type signature cannot bind scoped type variables `s' unless the pattern has a rigid type context In the pattern: s :: STRef s (Set Int) In a lambda abstraction: \ (s :: STRef s (Set Int)) -> seen s In the second argument of `(>>=)', namely `\ (s :: STRef s (Set Int)) -> seen s' Unfortunately I cannot find an easy workaround but use similiar patterns somewhere deeply nested in my programs... Is there a simple workaround? Could we relax the rules for lexically scoped type variables a bit? Regards, Mirko Rahn -- -- Mirko Rahn -- Tel +49-721 608 7504 -- --- http://liinwww.ira.uka.de/~rahn/ ---
Mirko Rahn wrote:
In ghc-6.4.2 this works as expected, but ghc-6.5.20061001 says
B.hs:40:44: A pattern type signature cannot bind scoped type variables `s' unless the pattern has a rigid type context
Why are the rules for lexically scoped type variables so complicated? Could we not just have a very simple rule like the following: 1) Any type variable not explicitly introduced by a forall is implicitly scoped over the entire top level decl that contains the expression/pattern that contains the type variable By "entire top level decl" I mean the highest level decl that makes sense eg: foo :: MonadIO m => a -> m a foo x = let bar :: forall b. b -> m b -- 'm' bound by foo's sig bar y = return y in bar x zap :: a -> Int zap _ = let yup = sizeOf (undefined :: a) in yup Regards, Brian. -- Logic empowers us and Love gives us purpose. Yet still phantoms restless for eras long past, congealed in the present in unthought forms, strive mightily unseen to destroy us. http://www.metamilk.com
| Simon Peyton-Jones asks for programs that are broken by the proposed | change. Here is a nearly real world one: You may not like this but this should work: Instead of | t1 = runST (trav f [1..10] (1,52) >>= \ (s::STRef s (Set Int)) -> seen s) try t1 = runST ( (trav f [1..10] (1,52) >>= \ s -> seen s) :: forall s. ST s [Int] ) or, equivalently t1 = runST run_it where run_it :: forall s. ST s Int run_it = trav f [1..10] (1,52) >>= \s -> seen s What's interesting about this example is that you aren't trying to bind the type variable 's'. You'd be quite happy to write \ (s :: STRef _ (Set Int)) -> seen s Note the wildcard "_". Arguably, one could loosen the rules in this case. This is an avenue that I have seen suggested before, but which I have, for one, not yet explored. Maybe others have better ideas. Simon
Simon Peyton-Jones wrote:
| t1 = runST (trav f [1..10] (1,52) >>= \ (s::STRef s (Set Int)) -> seen s)
try
t1 = runST ( (trav f [1..10] (1,52) >>= \ s -> seen s) :: forall s. ST s [Int] )
No, the problem is that t1 should use another implementation than t2. This version cannot discriminate between different implementations anymore. (And logically it did not compile.) In 6.4.2 I can choose the implementation just by type annotation but that's now impossible...
What's interesting about this example is that you aren't trying to bind the type variable 's'. You'd be quite happy to write \ (s :: STRef _ (Set Int)) -> seen s
Note the wildcard "_". Arguably, one could loosen the rules in this case. This is an avenue that I have seen suggested before, but which I have, for one, not yet explored. Maybe others have better ideas.
For me it would exactly solve the problem. So maybe one could 'quick hack' it into ghc!? Regards, MR -- -- Mirko Rahn -- Tel +49-721 608 7504 -- --- http://liinwww.ira.uka.de/~rahn/ ---
| > | t1 = runST (trav f [1..10] (1,52) >>= \ (s::STRef s (Set Int)) -> seen | > s) | > | > try | > | > t1 = runST ( (trav f [1..10] (1,52) >>= \ s -> seen s) | > :: forall s. ST s [Int] ) | | No, the problem is that t1 should use another implementation than t2. | This version cannot discriminate between different implementations | anymore. (And logically it did not compile.) Oh I see. Well, you'd need to put the type annotation for s back in: t1 = runST ( (trav f [1..10] (1,52) >>= \ (s::STRef s (Set Int)) -> seen s) :: forall s. ST s [Int] ) Simon
Oh I see. Well, you'd need to put the type annotation for s back in:
t1 = runST ( (trav f [1..10] (1,52) >>= \ (s::STRef s (Set Int)) -> seen s) :: forall s. ST s [Int] )
...and reach the starting point again. This version gives the same error message as the original one. But what works is to give some more detailed hints to the type system: t1S = trav f [1..10] (1,52) :: ST s (STRef s (Set Int)) t2S = trav f [1..10] (1,52) :: ST s (STUArray s Int Bool) t1 = runST ( t1S >>= seen ) t2 = runST ( t2S >>= seen ) This compiles (and works). Thank's for advice, MR -- -- Mirko Rahn -- Tel +49-721 608 7504 -- --- http://liinwww.ira.uka.de/~rahn/ ---
Aha. That's a bug. The forall'd type variables of an expression type signature should scope over the expression. Thank you -- I'll fix it, though I don't know if it'll get into 6.6 now. Simon | -----Original Message----- | From: Mirko Rahn [mailto:rahn@ira.uka.de] | Sent: 02 October 2006 16:05 | To: Simon Peyton-Jones | Cc: glasgow-haskell-users@haskell.org | Subject: Re: Problem with lexically scoped type variables. | | | > Oh I see. Well, you'd need to put the type annotation for s back in: | > | > t1 = runST ( (trav f [1..10] (1,52) >>= \ (s::STRef s (Set Int)) -> seen | > s) | > :: forall s. ST s [Int] ) | | ...and reach the starting point again. This version gives the same error | message as the original one. | | But what works is to give some more detailed hints to the type system: | | t1S = trav f [1..10] (1,52) :: ST s (STRef s (Set Int)) | t2S = trav f [1..10] (1,52) :: ST s (STUArray s Int Bool) | | t1 = runST ( t1S >>= seen ) | t2 = runST ( t2S >>= seen ) | | This compiles (and works). | | Thank's for advice, MR | | -- | -- Mirko Rahn -- Tel +49-721 608 7504 -- | --- http://liinwww.ira.uka.de/~rahn/ ---
participants (3)
-
Brian Hulley -
Mirko Rahn -
Simon Peyton-Jones