Re: Type checker's expected and inferred types (reformatted)
On Wednesday 28 October 2009 08:14:46 John Lato wrote: Isaac Dupree m...@isaac.cedarswampstudios.org wrote: ghci: Prelude \x - (3+x) + (length x) interactive:1:15: Couldn't match expected type `[a]' against inferred type `Int' In the second argument of `(+)', namely `(length x)' In the expression: (3 + x) + (length x) In the expression: \ x - (3 + x) + (length x) This is how I understand this process 1. checker infers x :: [a] from 'length x' 2. checker infers (3 + x) :: [a] from (+) and step 1 3. checker infers the second (+) :: [a] - [a] - [a] from step 2 4. conflict - checker expects (length x) :: [a] from step 3 and infers (length x) :: Int from definition of 'length'. Even with this simple example the error message given doesn't directly point to the problem. I don't think it's uncommon for there to be more steps in practice. I frequently find myself adding explicit type signatures to let-bound functions to debug these. This is a pain because it also usually involves enabling ScopedTypeVariables. I'll second that. On Saturday 24 October 2009 15:21:51 Albert Y. C. Lai wrote: I find it unnecessary to decrypt the two words expected and inferred. They have their own definitions and they stand for themselves; On the contrary, this is a perfect example of why the error message's choice of words is bad. One type is expected and the other is inferred. In the example the contextual type [a] is inferred via steps 1-2-3, and the internal type Int is determined so trivially that the inferred designation is somewhere between confusing and misleading. I'd love to see expected kept, and inferred removed from the message. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type checker's expected and inferred types (reformatted)
Dear GHCers, On Wed, 2009-10-28 at 12:14 +, John Lato wrote: This had me confused for a while, but I think I've worked out what's happening. (+) is polymorphic, ... Oh darn, it sounds like you're right. And polymorphism is so common. I just came up with that example randomly as the first nontrivial type-error-with-a-lambda I could think of... I think this is a great example of why the current type errors are not as helpful as they could be. The code where the type checker determines 'x' has type [a] is several steps removed from where the error arises. This is how I understand this process (I've probably left out some details): I am a little ambiguous on this issue; I usually find GHC's type errors make me realize what I did wrong very quickly, i.e. until I start messing with combinations of GADTs, type classes and type families. When I've looked at an error for too long without understanding what's happening, I usually look for ways to express the same problem in simpler constructs. This case has me stumped, though. 1. checker infers x :: [a] from 'length x' 2. checker infers (3 + x) :: [a] from (+) and step 1 3. checker infers the second (+) :: [a] - [a] - [a] from step 2 Pardon? Judging from the error GHC gives, you must be right, but isn't *this* the point where things should go wrong? I'm not too intimately familiar with the type checker's internals, so this example leads me to speculate that normal types are inferred and checked *before* type class constraints are evaluated. However, I would have wanted this error: Prelude [1] + [2] interactive:1:0: No instance for (Num [t]) arising from a use of `+' at interactive:1:0-8 Possible fix: add an instance declaration for (Num [t]) In the expression: [1] + [2] In the definition of `it': it = [1] + [2] In other words: isn't the problem in this case that the type checker does not gather all information (no instance of type class Num) to give the proper error? Is gathering type class information after normal types have already conflicted even possible? Regards, Philip ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type checker's expected and inferred types (reformatted)
From: Isaac Dupree m...@isaac.cedarswampstudios.org David Menendez wrote: On Sun, Oct 25, 2009 at 1:37 PM, Isaac Dupree m...@isaac.cedarswampstudios.org wrote: David Menendez wrote: The expected type is what the context wants (it's *ex*ternal). The inferred type is what the expression itself has (it's *in*ternal). So inferring the type Maybe () for bar seems wrong. well, maybe GHC just gets it wrong enough of the time, that I got confused. Or maybe ... When there are bound variables interacting, on the inside and outside, it gets confusing. ghci: Prelude \x - (3+x) + (length x) interactive:1:15: Couldn't match expected type `[a]' against inferred type `Int' In the second argument of `(+)', namely `(length x)' In the expression: (3 + x) + (length x) In the expression: \ x - (3 + x) + (length x) Your explanation of expected and inferred could make sense to me if the error message followed the Couldn't match line with, instead, In the first argument of `length', namely `x' because 'length' gives the context of expected list-type, but we've found out from elsewhere (a vague word) that 'x' needs to have type Int. This had me confused for a while, but I think I've worked out what's happening. (+) is polymorphic, ... Oh darn, it sounds like you're right. And polymorphism is so common. I just came up with that example randomly as the first nontrivial type-error-with-a-lambda I could think of... I think this is a great example of why the current type errors are not as helpful as they could be. The code where the type checker determines 'x' has type [a] is several steps removed from where the error arises. This is how I understand this process (I've probably left out some details): 1. checker infers x :: [a] from 'length x' 2. checker infers (3 + x) :: [a] from (+) and step 1 3. checker infers the second (+) :: [a] - [a] - [a] from step 2 4. conflict - checker expects (length x) :: [a] from step 3 and infers (length x) :: Int from definition of 'length'. Even with this simple example the error message given doesn't directly point to the problem. I don't think it's uncommon for there to be more steps in practice. I frequently find myself adding explicit type signatures to let-bound functions to debug these. This is a pain because it also usually involves enabling ScopedTypeVariables. I personally would find it useful if error messages showed the sequence of how the type checker determined the given context. Especially if it would also do so for infinite type errors, which don't provide much useful information to me. Cheers, John ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type checker's expected and inferred types (reformatted)
David Menendez wrote: The expected type is what the context wants (it's *ex*ternal). The inferred type is what the expression itself has (it's *in*ternal). So inferring the type Maybe () for bar seems wrong. well, maybe GHC just gets it wrong enough of the time, that I got confused. Or maybe ... When there are bound variables interacting, on the inside and outside, it gets confusing. ghci: Prelude \x - (3+x) + (length x) interactive:1:15: Couldn't match expected type `[a]' against inferred type `Int' In the second argument of `(+)', namely `(length x)' In the expression: (3 + x) + (length x) In the expression: \ x - (3 + x) + (length x) Your explanation of expected and inferred could make sense to me if the error message followed the Couldn't match line with, instead, In the first argument of `length', namely `x' because 'length' gives the context of expected list-type, but we've found out from elsewhere (a vague word) that 'x' needs to have type Int. If we flip around the expression-order, we get Prelude \x - (length x) + (3+x) interactive:1:20: Couldn't match expected type `Int' against inferred type `[a]' In the second argument of `(+)', namely `(3 + x)' In the expression: (length x) + (3 + x) In the expression: \ x - (length x) + (3 + x) ...and yes, technically your explanation of expected/inferred works. But the location/parity depends on the evaluation-order that the type checker uses. The error messages don't seem to specify location precisely enough that I can easily use the information about which type is the 'expected' type and which type is the 'inferred' one. There are usually more chains of inference, let-clauses, etc. through which a contradiction is found, that muddy the issue. hmm. Yes, I think I would appreciate for error messages to tell me exactly which piece of the expression is expected/inferred to be those types. (Is this always a sensible question? or are there sometimes typing-conflicts that can't be / aren't reduced to the expected/inferred type of a particular expression in the code?) -Isaac ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type checker's expected and inferred types (reformatted)
On Sun, Oct 25, 2009 at 1:37 PM, Isaac Dupree m...@isaac.cedarswampstudios.org wrote: David Menendez wrote: The expected type is what the context wants (it's *ex*ternal). The inferred type is what the expression itself has (it's *in*ternal). So inferring the type Maybe () for bar seems wrong. well, maybe GHC just gets it wrong enough of the time, that I got confused. Or maybe ... When there are bound variables interacting, on the inside and outside, it gets confusing. ghci: Prelude \x - (3+x) + (length x) interactive:1:15: Couldn't match expected type `[a]' against inferred type `Int' In the second argument of `(+)', namely `(length x)' In the expression: (3 + x) + (length x) In the expression: \ x - (3 + x) + (length x) Your explanation of expected and inferred could make sense to me if the error message followed the Couldn't match line with, instead, In the first argument of `length', namely `x' because 'length' gives the context of expected list-type, but we've found out from elsewhere (a vague word) that 'x' needs to have type Int. This had me confused for a while, but I think I've worked out what's happening. (+) is polymorphic, and GHC is giving it the type [a] - [a] - [a]. So the context is expecting [a], but we infer length x :: Int from the definition of length. In the alternate case, \x - length x + (3+x), GHC gives the outer (+) the type Int - Int - Int, and the inner (+) the type [a] - [a] - [a], which is why we get the type mismatch complaint for 3+x instead of x. Note what happens if we use a monomorphic operator: Prelude let () = undefined :: Int - Int - Int Prelude \x - (3+x) length x interactive:1:22: Couldn't match expected type `[a]' against inferred type `Int' In the first argument of `length', namely `x' In the second argument of `()', namely `length x' In the expression: (3 + x) length x Prelude \x - (3+x) + length x Here, GHC has concluded that x must be an Int, and thus can't be passed to length. Prelude \x - length x (3+x) interactive:1:19: Couldn't match expected type `Int' against inferred type `[a]' In the second argument of `()', namely `(3 + x)' In the expression: length x (3 + x) In the expression: \ x - length x (3 + x) Here, GHC has concluded that x must be [a], and thus 3+x must be [a], which can't be used with . -- Dave Menendez d...@zednenem.com http://www.eyrie.org/~zednenem/ ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type checker's expected and inferred types (reformatted)
David Menendez wrote: On Sun, Oct 25, 2009 at 1:37 PM, Isaac Dupree m...@isaac.cedarswampstudios.org wrote: David Menendez wrote: The expected type is what the context wants (it's *ex*ternal). The inferred type is what the expression itself has (it's *in*ternal). So inferring the type Maybe () for bar seems wrong. well, maybe GHC just gets it wrong enough of the time, that I got confused. Or maybe ... When there are bound variables interacting, on the inside and outside, it gets confusing. ghci: Prelude \x - (3+x) + (length x) interactive:1:15: Couldn't match expected type `[a]' against inferred type `Int' In the second argument of `(+)', namely `(length x)' In the expression: (3 + x) + (length x) In the expression: \ x - (3 + x) + (length x) Your explanation of expected and inferred could make sense to me if the error message followed the Couldn't match line with, instead, In the first argument of `length', namely `x' because 'length' gives the context of expected list-type, but we've found out from elsewhere (a vague word) that 'x' needs to have type Int. This had me confused for a while, but I think I've worked out what's happening. (+) is polymorphic, ... Oh darn, it sounds like you're right. And polymorphism is so common. I just came up with that example randomly as the first nontrivial type-error-with-a-lambda I could think of... I wonder if it would help for the message to also output what it thinks the complete type of the function is (so far). I wonder if it could look something like this: Couldn't match expected type `[a]' against inferred type `Int' In the second argument of `(+) :: [a] - [a]', namely `(length x) :: Int' (always, at the risk/tradeoff of taking up space with lots of useless information. sadly. hmm.) Ideally I would like GHC to pick a location for the error that's more intuitive, but that sounds like an awfully vague desire :-) -Isaac ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type checker's expected and inferred types (reformatted)
For the record, and to speak up as part of a possible silent majority, I completely understand the type error messages. I find enough information in them. I like them. I find it unnecessary to decrypt the two words expected and inferred. They have their own definitions and they stand for themselves; external and internal are helpful mnemonics, useful approximation, but not decryption. I support work on ghc to prioritize professional use over pedagogical use, that is, if a proposed pedagogical improvement conflicts with professional use concerns, or even if simply no one has time to implement, I support sacrificing the pedagogical improvement. To mitigate the sacrifice, we users write tutorials for each other. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type checker's expected and inferred types (reformatted)
Am Samstag 24 Oktober 2009 21:21:51 schrieb Albert Y. C. Lai: For the record, and to speak up as part of a possible silent majority, I completely understand the type error messages. Mostly, I do, too. But I can't get why IO () is *expected* and Maybe () is *inferred* for bar in fun2. Can you explain? I find enough information in them. I like them. Generally, it's the same for me, though some are better than others. Even if one doesn't completely understand them, it's rare that one can't get enough out of them to start fixing the code. I find it unnecessary to decrypt the two words expected and inferred. They have their own definitions and they stand for themselves; external and internal are helpful mnemonics, useful approximation, but not decryption. I support work on ghc to prioritize professional use over pedagogical use, that is, if a proposed pedagogical improvement conflicts with professional use concerns, or even if simply no one has time to implement, I support sacrificing the pedagogical improvement. Seconded. To mitigate the sacrifice, we users write tutorials for each other. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Type checker's expected and inferred types (reformatted)
(Some formatting was apparently lost en route. Trying again with extra
newlines.)
I came across a type error that misled me for quite a while, because the
expected and inferred types were backwards (from my point of view). A
simplified example is below. Can someone explain how GHC's type checker
creates the error message?
In this example, fun1 and fun2 are basically the same. The type error is
because they try to run an IO () together with a Maybe ().
import Control.Monad
foo :: Maybe ()
foo = return ()
bar :: IO ()
bar = return ()
fun1 = let fooThen m = foo m
in fooThen (bar undefined)
fun2 = let fooThen m = foo m
in fooThen (do {bar; undefined})
With ghc 6.10.4, both functions attribute the error message to `bar'. However,
the expected and inferred monads are swapped.
fun1 produces the error message:
Couldn't match expected type `Maybe a' against inferred type `IO ()'
In the first argument of `(=)', namely `bar'
fun2 produces the error message:
Couldn't match expected type `IO ()' against inferred type `Maybe ()'
In a stmt of a 'do' expression: bar
It's confusing because 'bar' is inferred to have type Maybe (), even though
it's explicitly declared to be an IO ().
_
Windows 7: Simplify your PC. Learn more.
http://www.microsoft.com/Windows/windows-7/default.aspx?ocid=PID24727::T:WLMTAGL:ON:WL:en-US:WWL_WIN_evergreen1:102009___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type checker's expected and inferred types (reformatted)
C Rodrigues wrote: fun1 produces the error message: Couldn't match expected type `Maybe a' against inferred type `IO ()' In the first argument of `(=)', namely `bar' fun2 produces the error message: Couldn't match expected type `IO ()' against inferred type `Maybe ()' In a stmt of a 'do' expression: bar It's confusing because 'bar' is inferred to have type Maybe (), even though it's explicitly declared to be an IO (). Which message do you prefer? I couldn't tell which it was. For myself, I never understood the difference between expected and inferred: it works better for me to just think there were at least two different ways that determined the 'type' of this expression, and the results contradicted each other, and here are two of those results. Now, dear user, go and look at your code to intuit *what* those ways of determining the type might have been (or sometimes it's easier just to look for mistakes, ignoring the particular details of the error) -Isaac ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type checker's expected and inferred types (reformatted)
On Fri, Oct 23, 2009 at 9:46 PM, Isaac Dupree m...@isaac.cedarswampstudios.org wrote: C Rodrigues wrote: fun1 produces the error message: Couldn't match expected type `Maybe a' against inferred type `IO ()' In the first argument of `(=)', namely `bar' fun2 produces the error message: Couldn't match expected type `IO ()' against inferred type `Maybe ()' In a stmt of a 'do' expression: bar It's confusing because 'bar' is inferred to have type Maybe (), even though it's explicitly declared to be an IO (). Which message do you prefer? I couldn't tell which it was. For myself, I never understood the difference between expected and inferred: it works better for me to just think there were at least two different ways that determined the 'type' of this expression, and the results contradicted each other, and here are two of those results. Now, dear user, go and look at your code to intuit *what* those ways of determining the type might have been (or sometimes it's easier just to look for mistakes, ignoring the particular details of the error) The expected type is what the context wants (it's *ex*ternal). The inferred type is what the expression itself has (it's *in*ternal). So inferring the type Maybe () for bar seems wrong. I'm guessing it's a bug in the way do-expressions are handled. Note that this doesn't happen if the bar is last. Prelude :t let fooThen m = foo m in fooThen (do undefined; bar) interactive:1:51: Couldn't match expected type `Maybe b' against inferred type `IO ()' In the expression: bar In the first argument of `fooThen', namely `(do undefined bar)' In the expression: fooThen (do undefined bar) Prelude :t do foo; bar interactive:1:8: Couldn't match expected type `Maybe b' against inferred type `IO ()' In the expression: bar In the expression: do foo bar Prelude :t do foo; bar; foo interactive:1:8: Couldn't match expected type `IO ()' against inferred type `Maybe ()' In a stmt of a 'do' expression: bar In the expression: do foo bar foo -- Dave Menendez d...@zednenem.com http://www.eyrie.org/~zednenem/ ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Type checker's expected and inferred types (reformatted)
Which message do you prefer? I couldn't tell which it was. I prefer fun1. In my understanding, the 'inferred' type is gleaned by looking at theexpression itself, while the 'expected' type is implied by the context. _ Windows 7: It works the way you want. Learn more. http://www.microsoft.com/Windows/windows-7/default.aspx?ocid=PID24727::T:WLMTAGL:ON:WL:en-US:WWL_WIN_evergreen2:102009___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
