Why is F#'s type inference so fickle?

Question

The F# compiler appears to perform type inference in a (fairly) strict top-to-bottom, left-to-right fashion. This means you must do things like put all definitions before their use, order of file compilation is significant, and you tend to need to rearrange stuff (via |> or what have you) to avoid having explicit type annotations.

How hard is it to make this more flexible, and is that planned for a future version of F#? Obviously it can be done, since Haskell (for example) has no such limitations with equally powerful inference. Is there anything inherently different about the design or ideology of F# that is causing this?

Answer 1

F# uses one pass compilation such that you can only reference types or functions which have been defined either earlier in the file you're currently in or appear in a file which is specified earlier in the compilation order.

I recently asked Don Syme about making multiple source passes to improve the type inference process. His reply was "Yes, it’s possible to do multi-pass type inference. There are also single-pass variations that generate a finite set of constraints.

However these approaches tend to give bad error messages and poor intellisense results in a visual editor."

http://www.markhneedham.com/blog/2009/05/02/f-stuff-i-get-confused-about/#comment-16153

Answer 2

I think that the algorithm used by F# has the benefit that it is easy to (at least roughly) explain how it works, so once you understand it, you can have some expectations about the result.

The algorithm will always have some limitations. Currently, it is quite easy to understand them. For a more complicated algorithms, this could be difficult. For example, I think you could run into situations where you think that the algorithm should be able to deduce something - but if it was general enough to cover the case, it would be non-decidable (e.g. could keep looping forewer).

Another thought on this is that checking the code from the top to the bottom corresponds to how we read code (at least sometimes..). So, maybe the fact that we tend to write the code in a way that enables type-inference also makes the code more readable for people...

Answer 3

Regarding "Haskell's equally powerful inference", I don't think Haskell has to deal with

• OO-style dynamic subtyping (type classes can do some similar stuff, but type classes are easier to type/infer)
• method overloading (type classes can do some similar stuff, but type classes are easier to type/infer)

That is, I think F# has to deal with some hard stuff that Haskell does not. (Almost certainly, Haskell has to deal with some hard stuff that F# does not.)

As is mentioned by other answers, most of the major .NET languages have the Visual Studio tooling as a major language design influence (see e.g. how LINQ has "from ... select" rather than the SQL-y "select... from", motivated by getting intellisense from a program prefix). Intellisense, error squiggles, and error-message comprehensibility are all tooling factors that inform the F# design.

It may well be possible to do better and infer more (without sacrificing on other experiences), but I don't think it's among our high priorities for future versions of the language. (The Haskellers may see F# type inference as somewhat weak, but they are probably outnumbered by the C#ers who see F# type inference as very strong. :) )

It might also be hard to extend the type inference in a non-breaking fashion; it is ok to change illegal programs into legal ones in a future version, but you have to be very careful to ensure previously-legal programs do not change semantics under new inference rules, and name resolution (an awful nightmare in every language) is likely to interact with type-inference-changes in surprising ways.

Answer 4

Is there anything inherently different about the design or ideology of F# that is causing this?

Yes. F# uses nominal rather than structural typing because it is simpler and, therefore, easier for mere mortals to use.

Consider this F# example:

let lengths (xss: _ [] []) = Array.map (fun xs -> xs.Length) xss

let lengths (xss: _ [] []) = xss |> Array.map (fun xs -> xs.Length)

The former does not compile because the type of xs inside the anonymous function cannot be inferred because F# cannot express the type "some class with a Length member".

In contrast, OCaml can express the direct equivalent:

let lengths xss = Array.map (fun xs -> xs#length) xss

because OCaml can express that type (it is written <length: 'a ..>). Note that this requires more powerful type inference than either F# or Haskell currently have, e.g. OCaml can infer sum types.

However, this feature is known to be a usability issue. For example, if you screw up elsewhere in the code then the compiler has not yet inferred that the type of xs was supposed to be an array so any error message it can give can only provide information like "some type with a Length member" and not "an array". With only slightly more complicated code, this quickly gets out of control as you have massive types with many structurally inferred members that don't quite unify, leading to incomprehensible (C++/STL-like) error messages.

Answer 5

The short answer is that F# is based on the tradition of SML and OCaml, whereas Haskell comes from a slightly different world of Miranda, Gofer, and the like. The differences in historical tradition are subtle, but pervasive. This distinction is paralleled in other modern languages too, such as the ML-like Coq which has the same ordering restrictions vs the Haskell-like Agda which doesn't.

This difference is related to lazy vs strict evaluation. The Haskell side of the universe believes in laziness, and once you already believe in laziness the idea of adding laziness to things like type inference is a no-brainer. Whereas in the ML side of the universe whenever laziness or mutual recursion is necessary it must be explicitly noted by the use of keywords like with, and, rec, etc. I prefer the Haskell approach because it results in less boilerplate code, but there are a lot of folks who think it's better to make these things explicit.