ok, someone check me on this (type unification from the (>>=)/fmap thread)
I can't tell where I'm making the mistake here. In the thread where (>>=) and fmap were being confused, the error cited a type (Maybe a) which was supposed to be in typeclass Num. As far as I can tell, if the typechecker gets to the point where Num and Maybe are both present and (m) is Maybe, it has to (1) be focused on the (m b) part of (a -> m b), and therefore (2) must have already unified (a) and (b). But that means (m b) must unify with (Num a => a), which is unified with (b), resulting in the attempt to unify (Num a => a) with (Maybe a); since we get the error about (Maybe a) not being a Num, it must not have gotten there. But that means it can't have related Num to (m a) with (m) bound to Maybe, which is why I assumed it had unified (m) with ((->) r) instead. Can the typechecker really get the Num to the other end of (a -> m b) without also getting the (a) there? Or is it checking for the Num constraint before it has fully evaluated the type of (m b)? I thought typeclass constraints happened later than basic type unification. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH
On 10 May 2009, at 09:24, Brandon S. Allbery KF8NH wrote:
I can't tell where I'm making the mistake here.
Frankly, I can't do it either, because I don't understand what you're talking about. It seems that you have some idea of how the typechecker works, which is very different from that of mine. I've explained my view on this subject in my response to Michael, and it doesn't involve the ((->) r) monad at all.
In the thread where (>>=) and fmap were being confused, the error cited a type (Maybe a) which was supposed to be in typeclass Num. As far as I can tell, if the typechecker gets to the point where Num and Maybe are both present and (m) is Maybe, it has to (1) be focused on the (m b) part of (a -> m b), and therefore (2) must have already unified (a) and (b). But that means (m b) must unify with (Num a => a), which is unified with (b), resulting in the attempt to unify (Num a => a) with (Maybe a); since we get the error about (Maybe a) not being a Num, it must not have gotten there. But that means it can't have related Num to (m a) with (m) bound to Maybe, which is why I assumed it had unified (m) with ((->) r) instead.
Can the typechecker really get the Num to the other end of (a -> m b) without also getting the (a) there? Or is it checking for the Num constraint before it has fully evaluated the type of (m b)? I thought typeclass constraints happened later than basic type unification.
-- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Am Sonntag 10 Mai 2009 07:24:43 schrieb Brandon S. Allbery KF8NH:
I can't tell where I'm making the mistake here.
In the thread where (>>=) and fmap were being confused, the error cited a type (Maybe a) which was supposed to be in typeclass Num. As far as I can tell, if the typechecker gets to the point where Num and Maybe are both present and (m) is Maybe, it has to (1) be focused on the (m b) part of (a -> m b), and therefore (2) must have already unified (a) and (b). But that means (m b) must unify with (Num a => a), which is unified with (b), resulting in the attempt to unify (Num a => a) with (Maybe a); since we get the error about (Maybe a) not being a Num, it must not have gotten there. But that means it can't have related Num to (m a) with (m) bound to Maybe, which is why I assumed it had unified (m) with ((->) r) instead.
Can the typechecker really get the Num to the other end of (a -> m b) without also getting the (a) there? Or is it checking for the Num constraint before it has fully evaluated the type of (m b)? I thought typeclass constraints happened later than basic type unification.
Just in case it hasn't been answered yet: Just 3 >>= (1+) Just 3 :: (Num n1) => Maybe n1 (>>=) :: (Monad m) => m a -> (a -> m b) -> m b (1+) :: (Num n2) => n2 -> n2 (Just 3 >>=) :: (Num n1) => (n1 -> Maybe b) -> Maybe b Now we must unify the type of (1+) with (Just 3 >>=)'s argument's type, that is (Num n2) => n2 -> n2 with (Num n1) => n1 -> Maybe b n2 = n1 n2 = Maybe b giving (Just 3 >>=) :: (Num (Maybe b)) => (Maybe b -> Maybe b) -> Maybe b Just 3 >>= (1+) :: Num (Maybe b) => Maybe b ================================================= module MaybeNum where import Control.Monad instance Num a => Num (Maybe a) where (+) = liftM2 (+) (-) = liftM2 (-) (*) = liftM2 (*) signum = fmap signum abs = fmap abs negate = fmap negate fromInteger = Just . fromInteger ================================================= *MaybeNum> Just 3 >>= (1+) Just 4 or, weirder: ================================================= instance Num (Maybe Bool) where (+) = liftM2 (/=) (-) = (+) (*) = liftM2 (&&) signum = (`mplus` Just False) abs = signum negate = id fromInteger = Just . odd ================================================= *MaybeNum> Just 3 >>= (1+) :: Maybe Bool Just False
Hi, Brandon S. Allbery KF8NH wrote:
I can't tell where I'm making the mistake here.
I'm not sure, but I guess you are mixing up some names. Did you make sure that all type variables are distinct before starting to unify?
... must have already unified (a) and (b) ...
Why should it unify a and b?
Can the typechecker really get the Num to the other end of (a -> m b) without also getting the (a) there? Or is it checking for the Num constraint before it has fully evaluated the type of (m b)? I thought typeclass constraints happened later than basic type unification.
I think you can unify without looking at typeclass constraints at all, then apply the resulting substitutions to the original constraints. (As long as there are not functional dependencies involved, at least). Tillmann
Brandon S. Allbery KF8NH wrote:
I can't tell where I'm making the mistake here.
In Just 3 >>= (+1), we have, with some alpha conversions to make the unification easier to follow: Just 3 :: Num i => Maybe i -- (1) (>>=) :: m a -> (a -> m b) -> m b -- (2) (+1) :: Num n => n -> n -- (3) Unify (1) with the first argument in (2): Maybe i ~ m a m ~ Maybe -- (4) i ~ a -- (5) Unify the second argument in (2) with (3): (n -> n) ~ (a -> m b) n ~ a -- (6) n ~ m b -- (7) Substitute (4) in (7): n ~ Maybe b -- (8) But we have (Num n), so from (8), we need (Num (Maybe b)). Since there is no such instance, we get the error. Your question seems to be whether some other error should have come up first.
From (5) and (6), we get:
n ~ i -- (9) And from (8): i ~ Maybe b -- (10) Again, we have (Num i), so from (10), we need (Num (Maybe b)). Same error, different route. Perhaps you are assuming that i defaults to Integer before the type-checking completes, and are therefore expecting that (10) should produce a unification error before contexts are checked? Regards, Matthew
participants (5)
-
Brandon S. Allbery KF8NH -
Daniel Fischer -
Matthew Brecknell -
Miguel Mitrofanov -
Tillmann Rendel