CODEWITHSUNDEEP
haskelltype-inferenceghcghci
scravy
scravy

Reputation: 12283

Type inference in GHCi vs. manual signature

when I type

:t map length . sum

into GHCi, it says that the type would be:

map length . sum :: Num [[a]] => [[[a]]] -> [Int]

However, if I create a file type-test.hs containing

x :: Num [[a]] => [[[a]]] -> [Int]
x = map length . sum

both ghc and ghci complain:

type-test.hs:1:1:
    Non type-variable argument in the constraint: Num [[a]]
    (Use -XFlexibleContexts to permit this)
    In the type signature for `x': x :: Num [[a]] => [[[a]]] -> [Int]

Why does ghci allow me to infer the type for this (using :t), when FlexibleContexts are not enabled?

Upvotes: 4

Views: 2835

Answers (5)

Ingo
Ingo

Reputation: 36339

Another way to look at it:

Haskell tells you that your expression had a valid type, namely [[[a]]] -> [Int] if only [[a]] would be an instance of Num.

This is like some girls telling you she will go out with you when hell freezes over. You wouldn't complain that she promised to go out with me despite the hell can freeze over possibility is not given in this world, would you? You would rather notice that she just said No in a more or less polite way.

Upvotes: 5

dflemstr
dflemstr

Reputation: 26167

(This doesn't answer your original question, but solves the problem with the code instead)

These errors hint at that your code as written probably isn't what you meant. This code:

map length . sum

means "Take my list of numbers, and sum it, then compute the length of each element(??) of the resulting number." That makes no sense.

You probably meant:

sum . map length

which means "Take my list of lists, compute the length of every element, and sum the lengths."

What the error message itself means is that since sum returns a number, aka the type of sum is Num n => [n] -> n, and you then try to use map length on that, which has type Num m => [[a]] -> [m], the compiler tries to say that n == [[a]] to make the types match, and everything goes downhill from there.

Upvotes: 7

C. A. McCann
C. A. McCann

Reputation: 77384

First, let's clarify one thing. What happens if we define the function in GHCi, rather than querying the type?

> let x = map length . sum :: (Num [[a]]) => [[[a]]] -> [Int]
<interactive>:0:9:
    Non type-variable argument in the constraint: Num [[a]]
    (Use -XFlexibleContexts to permit this)
    In an expression type signature: Num [[a]] => [[[a]]] -> [Int]

And so on. In other words, the same thing. What if we let GHCi infer the type of the definition?

> let x = map length . sum
<interactive>:0:22:
    No instance for (Num [[a0]])
      arising from a use of `sum'
    Possible fix: add an instance declaration for (Num [[a0]])
    In the second argument of `(.)', namely `sum'
    In the expression: map length . sum

This is roughly the same error that results from loading a file containing the definition without a type signature.

What's the upshot of all this? Well, think about the fact that it tells you what extension is needed. GHC is capable of recognizing what the type means, even if it rejects the type by default. I'd hardly expect GHC to use a completely different type checker depending on the combination of extensions used, so it seems easy to conclude that the offending type is being rejected for no reason other than the relevant extension being disabled.

The :t command in GHCi isn't part of the compilation process--it's a hotline to the type checking and inference system, letting you ask the type of hypothetical code. There's no obvious reason for it to restrict itself arbitrarily based on extensions, when a more general type could still be informative, for the same reason that the error messages above tell you use -XFlexibleContexts to permit this rather than merely syntax error in type constraint.

As a possibly more interesting aside, there are also cases where an inferred type will be accepted happily by the compiler, but the inferred type can't actually be written out explicitly for one of several reasons.

For instance, disabling the monomorphism restriction will allow your example to have its type inferred (matching what :t says), despite that type requiring an extension to write manually.

Another example are definitions in the where clause of a function definition which make use of polymorphic arguments to the parent function. Their own types are not polymorphic, being dictated by the arguments received in the outer scope, yet the type variables in the parent function's signature are not in scope for the where clause¹. There may be other examples as well.

¹ The type variables from the parent's signature can be brought into scope with the ScopedTypeVariables extension and an explicit forall, if that's needed.

Upvotes: 10

Daniel Fischer
Daniel Fischer

Reputation: 183888

The problem is that the function is perfectly acceptable, but its most general type is not allowed to be specified by the language grammar. What could ghci do in such circumstances? I can only think of two options, either give a type that can only be specified with some extension enabled, or giving an error. Giving an error without mentioning that it can be fixed by enabling an extension seems not very desirable to me. Just having :t report the inferred most general type is simpler, and quite possibly when the feature was implemented, nobody thought of situations like this.

Upvotes: 1

nponeccop
nponeccop

Reputation: 13677

See http://haskell.org/ghc/docs/6.12.1/html/users_guide/interactive-evaluation.html#extended-default-rules

Upvotes: 0

Related Questions