Hello everybody, I'm trying to implement the type protection used by ST to prevent a monad from returning a certain type. There's my code: import Control.Monad.Identity newtype SomeMonad s a = SomeMonad { unSome :: Identity a } deriving (Monad) newtype SomeType s = SomeType Int runSomeMonad :: (forall s. SomeMonad s a) -> a runSomeMonad (SomeMonad x) = runIdentity x And when compiled, I got this error: phantom.hs:10:14: Couldn't match expected type `forall s. PwetMonad s a' against inferred type `PwetMonad s a1' In the pattern: PwetMonad x In the definition of `runPwetMonad': runPwetMonad (PwetMonad x) = runIdentity x But when I change line 10 to: runSomeMonad x = runIdentity . unSome $ x then it works, so obviously, the trouble is about pattern matching. What was I doing wrong?
On Sat, Jul 3, 2010 at 4:24 PM, Yves Parès
Hello everybody,
I'm trying to implement the type protection used by ST to prevent a monad from returning a certain type. There's my code:
import Control.Monad.Identity
newtype SomeMonad s a = SomeMonad { unSome :: Identity a } deriving (Monad)
newtype SomeType s = SomeType Int
runSomeMonad :: (forall s. SomeMonad s a) -> a runSomeMonad (SomeMonad x) = runIdentity x
And when compiled, I got this error: phantom.hs:10:14: Couldn't match expected type `forall s. PwetMonad s a' against inferred type `PwetMonad s a1' In the pattern: PwetMonad x In the definition of `runPwetMonad': runPwetMonad (PwetMonad x) = runIdentity x
But when I change line 10 to: runSomeMonad x = runIdentity . unSome $ x
then it works, so obviously, the trouble is about pattern matching. What was I doing wrong?
I think it has to do with the order that the foralls are instantiated, but when that comes up it always surprises me and I find it very confusing as well. The error message is saying that the constructor (SomeMonad) has type forall s1 a1. SomeMonad s1 a1 but that the function signature requires it to have have type forall a. (forall s. SomeMonad s a). If you introduce a case expression the error goes away: runSomeMonad :: (forall s. SomeMonad s a) -> a runSomeMonad m = case m of SomeMonad x -> runIdentity x My, vague and likely incorrect, understanding is that the order that the type checker/inferencer picks the types for s and a can make examples like this fail and changing the expression so that it must pick them later/differently fixes it. Perhaps someone can correct my understanding. In the case where you use unSome, I suspect the reason it works is because unSome works for any s and a so the difference in order of choice doesn't matter to applications of unSome. At least, that's my vague understanding. I hope that helps, Jason
On Saturday 03 July 2010 7:24:17 pm Yves Parès wrote:
I'm trying to implement the type protection used by ST to prevent a monad from returning a certain type. There's my code:
import Control.Monad.Identity
newtype SomeMonad s a = SomeMonad { unSome :: Identity a } deriving (Monad)
newtype SomeType s = SomeType Int
runSomeMonad :: (forall s. SomeMonad s a) -> a runSomeMonad (SomeMonad x) = runIdentity x
And when compiled, I got this error: phantom.hs:10:14: Couldn't match expected type `forall s. PwetMonad s a' against inferred type `PwetMonad s a1' In the pattern: PwetMonad x In the definition of `runPwetMonad': runPwetMonad (PwetMonad x) = runIdentity x
But when I change line 10 to: runSomeMonad x = runIdentity . unSome $ x
then it works, so obviously, the trouble is about pattern matching. What was I doing wrong?
The problem is instantiation. SomeMonad is a constructor for the type SomeMonad s a for any *particular* s and a. But the type: forall s. SomeMonad s a is not that type. That type doesn't have constructors (proper) at all, and hence you cannot match against it. If types were passed explicitly, then values of the second type would look like: /\s -> ... Where the big lambda is type abstraction. But you can't match against this, of course (just as you can't match against functions as lambda expressions), you can only apply values of this type. In the second case, when you write: runIdentity . unSome $ x you are implicitly instantiating x to some particular s (which? I can't say; I suppose it doesn't matter), which allows you to to match against it, or use unSome as you are. If type passing were explicit, it'd look like: runIdentity . unSome $ x@() picking s = (), for example. You could also do a case like: case x@() of SomeMonad m -> ... which in GHC would just look like: case x of SomeMonad m -> ... which can be confusing, because one would expect to be able to collapse that into a direct match in the function definition, but you cannot, because you have to apply x to a type before you match on it. -- Dan
Hello!
On Sat, Jul 3, 2010 at 9:12 PM, Dan Doel
The problem is instantiation. SomeMonad is a constructor for the type
SomeMonad s a
for any *particular* s and a. But the type:
forall s. SomeMonad s a
is not that type. That type doesn't have constructors (proper) at all, and hence you cannot match against it. If types were passed explicitly, then values of the second type would look like:
/\s -> ...
Where the big lambda is type abstraction. But you can't match against this, of course (just as you can't match against functions as lambda expressions), you can only apply values of this type.
I understood your explanation. However, is this an implementation detail/bug or is it an intended feature? Cheers, -- Felipe.
On Saturday 03 July 2010 10:52:31 pm Felipe Lessa wrote:
I understood your explanation. However, is this an implementation detail/bug or is it an intended feature?
Well, I wouldn't call it a bug. Perhaps it could be called a lack of a feature, because one can imagine such pattern matches being desugared into case statements where instantiation is allowed to happen.... But, the example here is very simple, and I can raise some issues that might convince you that this isn't a simple issue in general, and the GHC devs are somewhat justified in not bothering to sort it out, at your expense. :) First, what if we write: runSomeMonad m@(SomeMonad x) = ... What type does m have? We need to instantiate the argument to do the match on the right, so is m bound to the instantiated value, or the polymorphic value? I guess this comes down to whether the above desugars to: runSomeMonad m = case m of SomeMonad x -> ... or: runSomeMonad v = case v of m@(SomeMonad x) -> ... Second, the original example is uniform regardless of how 's' is instantiated, but that might not be true in general. If we use data families for instance: data family T a :: * data instance T Int = I1 Int | I2 Char data instance T () = U1 Int | U2 data instance T Char = C1 | C2 Int f :: (forall a. T a) -> Int ... Now, how are we going to be allowed to match in this function? f (I1 i) = ... f (I2 c) = ... This, so far, desugars fine into something like: f t = case t :: T Int of I1 i -> ... I2 c -> ... but adding a third case makes the situation trickier: f (U1 i) = ... because that'd require instantiating t to a different type. Of course, you could still desugar that to: f t = case t :: T Int of I1 i -> ... I2 c -> ... _ -> case t :: T () of U1 i -> ... but that third case is dead code. Or, should we allow mixing and matching, and instantiate separately even at the same type: f (I1 i) = ... f (C2 i) = ... f (U1 i) = ... f (I2 i) = ... becomes: f t = case t :: T Int of I1 i -> ... _ -> case t :: T Char of C2 i -> ... _ -> case t :: T () of U1 i -> ... _ -> case t :: T Int of I2 i -> ... although that could be consolidated a bit. That's off the top of my head. There may be other issues. Treating values with polymorphic type as if they were some particular instantiation isn't a simple matter, though. -- Dan
Okay, I understand better, now. But I could never have guessed it just from the GHC error message. Another question on the same code: import Control.Monad.Identity newtype SomeMonad s a = SomeMonad { unSome :: Identity a } deriving (Monad) newtype SomeType s = SomeType Int runSomeMonad :: (forall s. SomeMonad s a) -> a runSomeMonad x = runIdentity . unSome $ x foo :: SomeType s foo = runSomeMonad (return $ SomeType 42) According to what I read about ST, it should not compile because of 'foo' (hence the protection), well it does. What have I forgotten in my code?
On Sunday 04 July 2010 5:41:07 am Yves Parès wrote:
Okay, I understand better, now. But I could never have guessed it just from the GHC error message.
Another question on the same code:
import Control.Monad.Identity
newtype SomeMonad s a = SomeMonad { unSome :: Identity a } deriving (Monad)
newtype SomeType s = SomeType Int
runSomeMonad :: (forall s. SomeMonad s a) -> a runSomeMonad x = runIdentity . unSome $ x
foo :: SomeType s foo = runSomeMonad (return $ SomeType 42)
According to what I read about ST, it should not compile because of 'foo' (hence the protection), well it does. What have I forgotten in my code?
The s in your SomeType isn't linked in any way to the variable quantified in the SomeMonad. You're producing: return $ SomeType 42 :: forall t. SomeMonad t (SomeType s) and running it to get the SomeType s. You need something to tie them together, like: mkSomeType :: Int -> SomeMonad s (SomeType s) mkSomeType i = return (SomeType i) and then hide the SomeType constructor, perhaps. -- Dan
That's it !
Indeed, you do not create a STRef yourself using a STRef data constructor,
you use the function:
newSTRef :: a -> GHC.ST.ST s (STRef s a)
Thanks.
2010/7/4 Dan Doel
On Sunday 04 July 2010 5:41:07 am Yves Parès wrote:
Okay, I understand better, now. But I could never have guessed it just from the GHC error message.
Another question on the same code:
import Control.Monad.Identity
newtype SomeMonad s a = SomeMonad { unSome :: Identity a } deriving (Monad)
newtype SomeType s = SomeType Int
runSomeMonad :: (forall s. SomeMonad s a) -> a runSomeMonad x = runIdentity . unSome $ x
foo :: SomeType s foo = runSomeMonad (return $ SomeType 42)
According to what I read about ST, it should not compile because of 'foo' (hence the protection), well it does. What have I forgotten in my code?
The s in your SomeType isn't linked in any way to the variable quantified in the SomeMonad. You're producing:
return $ SomeType 42 :: forall t. SomeMonad t (SomeType s)
and running it to get the SomeType s. You need something to tie them together, like:
mkSomeType :: Int -> SomeMonad s (SomeType s) mkSomeType i = return (SomeType i)
and then hide the SomeType constructor, perhaps.
-- Dan
On 4 July 2010 00:24, Yves Parès
then it works, so obviously, the trouble is about pattern matching. What was I doing wrong?
This seems to be in violation of the Haskell Report. See e.g. section 3.3 (http://www.haskell.org/onlinereport/exps.html): """ The following identity holds: \ p1 ... pn -> e = \ x1 ... xn -> case (x1, ..., xn) of (p1, ..., pn) -> e where the xi are new identifiers. """ But: runSomeMonad4, runSomeMonad5 :: (forall s. SomeMonad s a) -> a runSomeMonad4 = \x -> case x of SomeMonad x -> runIdentity x runSomeMonad5 = \(SomeMonad x) -> runIdentity x runSomeMonad4 is accepted and runSomeMonad5 is rejected. Of course, the Report doesn't make provision for rank-N types, so this is not *strictly* speaking a violation. But it does seem against the *spirit* of the report, if nothing else! Cheers, Max
participants (5)
-
Dan Doel -
Felipe Lessa -
Jason Dagit -
Max Bolingbroke -
Yves Parès