Why do GHC and GHCI differ on type inference?

Question

I noticed, when doing a codegolf challenge, that by default, GHC doesn't infer the most general type for variables, leading to type errors when you try to use it with two different types.

For example:

(!) = elem
x = 'l' ! "hello" -- From its use here, GHC assumes (!) :: Char -> [Char] -> Bool
y = 5 ! [3..8] -- Fails because GHC expects these numbers to be of type Char, too

This can be changed using the pragma NoMonomorphismRestriction.

However, typing this into GHCI produces no type error, and :t (!) reveals that here, it assumes (Foldable t, Eq a) => a -> t a -> Bool, even when explicitly run with -XMonomorphismRestriction.

Why do GHC and GHCI differ on assuming the most general type for functions?

(Also, why have it enabled by default anyway? What does it help?)

Answer 1

I can't replicate your result that GHCi infers the type (Foldable t, Eq a) => a -> t a -> Bool even with -XMonomorphismRestriction (GHC 8.0.2).

What I see is that when I enter the line (!) = elem it infers the type (!) :: () -> [()] -> Bool, which is actually a perfect illustration of why you would want GHCi to behave "differently" from GHC, given that GHC is using the monomorphism restriction.

The problem described in @Davislor's answer that the monomorphism restriction was intended to address is that you could write code that syntactically looks like it's computing a value once, binding it to a name, and then using it several times, where actually the thing bound to a name is a reference to a closure awaiting a type class dictionary before it can really compute the value. All the use sites would separately work out what dictionary they need to pass and compute the value again, even if all the use sites actually pick the same dictionary (exactly as if you write a function of a number and then invoke it from several different places with the same parameter, you'd get the same result computed multiple times). But if the user was thinking of that binding as a simple value then this would be unexpected, and it's extremely likely that all the use-sites will want a single dictionary (because the user expected a reference to a single value computed from a single dictionary).

The monomorphism restriction forces GHC not to infer types that still need a dictionary (for bindings that have no syntactic parameters). So now the dictionary is chosen once at the binding site, instead of separately at each use of the binding, and the value really is only computed once. But that only works if the dictionary chosen at the binding site is the correct one that all the use sites would have chosen. If GHC picked the wrong one at the binding site, then all the use-sites would be type errors, even if they all agree on what type (and thus dictionary) they were expecting.

GHC compiles entire modules at once. So it can see the use sites and the binding site at the same time. Thus if any use of the binding requires a specific concrete type, the binding will use that type's dictionary, and everything will be well so long as all of the other use sites are compatible with that type (even if they were actually polymorphic and would also have worked with other types). This works even if the code that pins down the correct type is widely separated from the binding by many other calls; all the constraints on the types of things are effectively connected by unification during the type checking/inference phase, so when the compiler is choosing a type at the binding site it can "see" the requirements from all of the use-sites (within the same module).

But if the use sites are not all consistent with a single concrete type, then you get a type error, as in your example. One use-site of (!) requires the a type variable to be instantiated as Char, the other requires a type that also has a Num instance (which Char doesn't).

This wasn't consistent with our hopeful assumption that all the use-sites would want a single dictionary, and so the monomorphism restriction has resulted in an error that could have been avoided by inferring a more general type for (!). It's certainly debatable that the monomorphism restriction prevents more problems than it solves, but given that it is there, surely we'd want GHCi to behave the same way, right?

However GHCi is an interpreter. You enter code one statement at a time, not one module at a time. So when you type (!) = elem and hit enter, GHCi has to understand that statement and produce a value to bind to (!) with some specific type right now (it can be an unevaluated thunk, but we have to know what its type is). With the monomorphism restriction we can't infer (Foldable t, Eq a) => a -> t a -> Bool, we have to pick a type for those type variables now, with no information from use-sites to help us pick something sensible. The extended default rules that are on in GHCi (another difference from GHC) default those to [] and (), so you get (!) :: () -> [()] -> Bool¹. Pretty useless, and you get a type error trying either of the uses from your example.

The problem that the monomorphism restriction addresses is particularly egregious in the case of numeric calculations when you're not writing explicit type signatures. Since Haskell's numeric literals are overloaded you could easily write an entire complex calculation, complete with starting data, whose most general type is polymorphic with a Num or Floating or etc constraint. Most of the builtin numeric types are very small, so you're very likely to have values that you'd much rather store than compute multiple times. The scenario is more likely to happen, and more likely to be a problem.

But it's also exactly with numeric types that the whole-module type-inference process is essential to defaulting type variables to a concrete type in a way that is at all usable (and small examples with numbers are exactly what people new to Haskell are likely to be trying out in the interpreter). Before the monomorphism restriction was off by default in GHCi, there was a constant stream of Haskell question here on Stack Overflow from people confused why they couldn't divide numbers in GHCi that they could in compiled code, or something similar (basically the reverse of your question here). In compiled code you can mostly just write code the way you want with no explicit types and the full-module type inference figures out whether it should default your integer literals to Integer, or Int if they need to be added to something returned by length, or Double if they need to be added to something and multiplied by something else which is elsewhere divided by something, etc etc. In GHCi a simple x = 2 very often does the wrong under the monomorphism restriction turned on (because it'll pick Integer regardless of what you wanted to do with x later), with the result that you need to add far more type annotations in a quick-and-easy interactive interpreter than even the most ardent explicit-typist would use in production compiled code.

So it's certainly debateable whether GHC should use the monomorphism restriction or not; it's intended to address a real problem, it just also causes some other ones². But the monomorphism restriction is a terrible idea for the interpreter. The fundamental difference between line-at-a-time and module-at-a-time type inference means that even when they both did default to using it they behaved quite differently in practice anyway. GHCi without the monomorphism restriction is at least significantly more usable.

---

¹ Without the extended default rules you instead get an error about an ambiguous type variable, because it doesn't have anything to pin down a choice, not even the somewhat silly defaulting rules.

² I find it only a mild irritation in actual development because I write type signatures for top-level bindings. I find that's enough to make the monomorphism restriction apply only rarely, so it doesn't help or hinder me much. Thus I'd probably rather it was scrapped so that everything works consistently, especially as it seems to bite learners far more often than it bites me as a practitioner. On the other hand, debugging a rare performance problem on the occasion that it matters is much harder than rarely having to add a correct type signature that GHC annoyingly won't infer.

Answer 2

The background of why the committee made this decision is given, in the designers’ own words, in the article “A History of Haskell: Being Lazy with Class” by Paul Hudak et al.

A major source of controversy in the early stages was the so-called “monomorphism restriction.” Suppose that genericLength has this overloaded type:

genericLength :: Num a => [b] -> a

Now consider this definition:

f xs = (len, len)`
  where
    len = genericLength xs

It looks as if len should be computed only once, but it can actually be computed twice. Why? Because we can infer the type len :: (Num a) => a; when desugared with the dictionary-passing translation, len becomes a function that is called once for each occurrence of len, each of which might used at a different type.

[John] Hughes argued strongly that it was unacceptable to silently duplicate computation in this way. His argument was motivated by a program he had written that ran exponentially slower than he expected. (This was admittedly with a very simple compiler, but we were reluctant to make performance differences as big as this dependent on compiler optimisations.)

Following much debate, the committee adopted the now-notorious monomorphism restriction. Stated briefly, it says that a definition that does not look like a function (i.e. has no arguments on the left-hand side) should be monomorphic in any overloaded type variables. In this example, the rule forces len to be used at the same type at both its occurrences, which solves the performance problem. The programmer can supply an explicit type signature for len if polymorphic behaviour is required.

The monomorphism restriction is manifestly a wart on the language. It seems to bite every new Haskell programmer by giving rise to an unexpected or obscure error message. There has been much discussion of alternatives.

(18, Emphasis added.) Note that John Hughes is a co-author of the article.

Answer 3

NoMonomorphismRestriction is a useful default in GHCI because you don't have to write out so many pesky type signatures in the repl. GHCI will try to infer the most general types it can.

MonomorphismRestriction is a useful default otherwise for efficiency / performance reasons. Specifically, the issue boils down to the fact that:

typeclasses essentially introduce additional function parameters -- specifically, the dictionary of code implementing the instances in question. In the case of typeclass polymorphic pattern bindings, you end up turning something that looked like a pattern binding -- a constant that would only ever be evaluated once, into what is really a function binding, something which will not be memoised.

Link