[Haskell-cafe] Type inference; always

[Luke Palmer]

2008/5/18 Peter Verswyvelen <bf3 at telenet.be>:
> In Haskell, I sometimes have to annotate code with type info because the
> type-inferer otherwise fails (even with -XNoMonomorphismRestriction).
> Surely, most of the time this is because I was writing buggy code, but
> sometimes, type annotation just seems needed to get a successful compilation
> (luckily not as often as in C# 3.0)

Then you must either be programming using extensions or you have found
a bug.  Haskell 98 should never require annotations (modulo
monomorphism).  In particular with either higher rank polymorphism or
GADTs, full inference is undecidable, so it is perfectly reasonable to
have to put a few annotations here and there.

> It seems some new papers appeared regarding this, e.g.
> http://research.microsoft.com/~simonpj/papers/boxy
>
> Is this work being incorporated into GHC?

IIRC that work is already in 6.8.  I can't be sure though.

> Unfortunately I'm not able to read those papers, so I'm not really sure what
> it means anyway and what implications (example code?) it would have ;-)

There are some type inference algorithms (Colored Local Type Inference
of Scala comes to mind) which can infer quite a lot, but it is pretty
difficult to tell when it won't be able to.  The main contribution of
the FPH is an algorithm which is predictable in that respect.  From
the paper:

"FPH ... has the following delightfully simple rule for when a type
annotation is required:  a type annotation may be required only for a
let-binding or lambda-abstraction that has a non-Damas-Milner type"

Here the paper is only referring to higher-rank polymorphism, so its
interaction with other extensions can still be tricky.  Essentially
non-Damas-Milner types are the ones that you wouldn't be able to write
down in Haskell without the 'forall' keyword; the ones whose
quantification is somewhere besides the top level.

Do you have an example of code that required an annotation to compile?

Luke