Full type inference also lets you write beautiful, simple code -- without even needing to add types later, you get them now. And speeding up execution is just a bonus, the main benefit is catching errors early, and refactoring safely.

You cannot add "full-type inference" on top of a language with a dynamic type system. You also cannot add such type inference to an object-oriented language, like Scala (it may be possible, but very hard and nobody did it).

     the main benefit is catching errors early

Dynamic typing isn't about not specifying types. Dynamic typing is about creating types at runtime.

This enables certain techniques that are very productive, and totally different from what you would do in a language like Haskell, which does have full-type inference.

I also do not think a static language would work as a client-side in-browser language, simply because of the nature of browsers and the web. Such a language needs runtime introspection and even types created at runtime like air. For in-browser stuff I also prefer eval() over static-typing any day of the week.

There's an real conflict between static typing and eval() or reflection.

eval() is shown to be usable in a static typing environment by some of Don Stewart's papers, though it does take more effort on the language implementors' side.

Reflection is achieved in Haskell, for example, using reflective type-classes (such as Typeable and Data).

Doh, too late to edit.

Above should read: "There's no real conflict"

Unfortunately, there is no type inference system (that I know of) that can handle types that programmers use in dynamically typed languages on a daily basis. For example, consider the Django admin property 'list_filter' [1] or the Clojure metaprogramming functions 'proxy' [2] and 'defrecord' [3].

[1] https://docs.djangoproject.com/en/dev/ref/contrib/admin/#dja... [2] http://clojure.github.com/clojure/clojure.core-api.html#cloj... [3] http://clojure.github.com/clojure/clojure.core-api.html#cloj...

list_filter seems to be a closed sum type -- why do you think it's not simple to encode or infer as a static type?

I'm not sure what Proxy is used for -- but it sounds like Template Haskell can probably implement it?

defrecord seems like it refers to defining new types at runtime -- which is also possible via either late type-check or Template Haskell.

Actually, I didn't mean to type the whole function, but only the parameters... One would require something like union types, e.g. list_filter has type

  String | `a < SimpleListFilter | (String, `b < FieldListFilter)

Now, this type is certainly encodable in a modern advanced type system (although most statically typed languages utilize type erasure for compilation, so you would need tagged unions (Algebraic Data Types) for this), but I cannot imagine that any language is capable of inferring such a type. Maybe OCaml, but again, we would need polymorphic variants for that.

Instead of (a < SimpleListFilter) you can use a type-class constraint and an existential, or an explicit record of methods. In Haskell, anything you use will basically be inferred, and Haskell can encode that, though you would have to choose different primitives to encode that relationship than subtypes.

To a point, JavaScript already has type inference: https://mail.mozilla.org/pipermail/es-discuss/2011-September...