Lambda the Ultimate

And this is both good and bad. Many people (rightly, I believe) claim that extensive use of type inference can harm readability. This is particularly important in a language with ad-hoc polymorphism.

All well and good, of course. But can you have the good without the bad? Clearly, local inference does not give the same benefits as global type inference, so they are not comparable. If we are thinking of the advantages of global inferencing, can we have those without the dangers you mention?

Global inference with an IDE adding the appropriate annotations to the display (but not the source per se unless asked) seems a good way to go. Failing that, I'd like a way to separate out annotations that are there to directly express the programmer's intent from ones that're there for ease of understanding - that way, if I want to carry out transformations that preserve well-typedness but not types then I can just regenerate the latter afterwards and only worry about the former. This might also help in tracking type errors on occasion - if it trips a "documentation" annotation but would be well-typed without, that might be suggestive.

...save a lot of typing, and it sure makes refactoring easier.

Of course, if that's ALL you want, you can just use type aliases (typedef or similar).

Since I am in a sarcastic mood: People who type slowly, perhaps should not be programmers.

Alternatively: By the time you have enough practice to be a good programmer, the amount of typing (on the keyboard) is less of an issue than the amount of typing (in the code).

not much typing of either sort there... :)

Modern IDEs handle "the typing" aspect of it. It's the reading aspect that is the problem - too much clutter, too much boilerplate, etc..

This is a double edged sword: I want the addiotnal stuff when I am reading code, provide of course that it is readable and not line noise...

Why couldn't a tool derive a good read mode from a piece of source code, including (inferred) type annotations, documentation, comments, reordering the declarations to follow some narrative hints, unit tests, referenced papers? The more I think about reading vs writing code the less I like this WYSIWYG nature of editors today, the linear structure used today is just one path in the possible narratives that would be interesting to read. Actually it makes me sad that the Smalltalk browser was created so long ago and it still is the state of art for this (don't get me wrong I love the browser, but we could do so much more).

The idea of tools for producing different representations for reading code is not new. Eiffel is a prominent language that advocated exactly that (though not for type annotation, naturally).

Does this refer to module local type inference? Or is does it refer to the restricted flow of type information through the parse tree (at all levels)?

My definition of local type inference is type inference within a local scope which is not dependent on anything other than the explicit types of local symbols. Practically, it means the types of arguments and return types of functions or methods must have type annotatons, as well as any non-local symbols such as global variables.

Here is an example of a function written in GScript, our internal language that uses local type inference:

  function calculateTotalSalaries( emps : List<Employee> ) : double {
    var salaries = emps.map( \ e -> e.Salary )
    return salaries.sum()
  }

You have to annotate the parameter and return type, but everything else is inferred:

• the "e" paramter in the closure (we use the haskell syntax for closures) is inferred to be of type "Employee"
• the "salaries" variable is inferred to be List<double>

All of this inference depends only on the declared types of the parameters and the map and sum functions in a very straight-forward way, with no complicated multi-pass inference algorithm necessary. So you get a lot of bang for your buck.

Cheers,
Carson

the type parameter instantiations were drowning out the content.

Totally, 100% agreed. Tuples above 3 parameters are unusable in C#, sometimes forcing me to resort to arrays, and all the dynamic checking that involves.

Right, and this is what I meant by "needing better tool support". So the burden of supporting type inference shifts to the IDE, similarly to how Lisp is unusable without editor support. This is fine, I think, but must be acknowledged.

Fine? We had this debate so many time I am reluctant to start it again (really - those interested should read the archives, this is flame war territory around here). As a personal choice, I think tool support is nice but semantics are nicer. I want code I can read printed. I don't care how many characters are needed. Motto: If that's your bottleneck you are doing something wrong.

My bottleneck won't be the physical process of typing, but the process of going from "enough to be happy it'll be well-typed" to "I know the precise type and can serialise it into source code" can be slow and gets slower as the amount of detail in our types gets greater and greater. I'd far rather have a semantically-aware pretty-printer add inferred type annotations in appropriate places than have to hand-maintain them.

That said, most of our languages are appallingly spartan at type level compared to term level. Where are our local bindings, that we may wrap up a chunk of type behind a descriptive name and be done with it? Why doesn't the inferrer propagate all this stuff for us? Could we exploit techniques for common subexpression elimination to suggest where we might want to do so?

Over time this is likely to suggest a separation between a core type language and a metalanguage used to work with the inferrer/elaborator. It doesn't seem uncommon for proof assistants and the like to have a separation in this vein, either.

Is this the sort of semantic support (if any) you have in mind?

Now I hear some saying that (in the presence of subtypes), type inference doesn't work that well, or always give you what you want.

Which comment says that?

It just feels safer :-).

Sticking with the inferred type will always be "safe". What measure of "safety" are you using to make that judgment?

Now I hear some saying that (in the presence of subtypes), type inference doesn't work that well, or always give you what you want.

The problem isn't subtyping but the particular subtyping choose by these languages (which weren't designed with good type systems in mind). I'm pretty happy typing p :: a -> Parser (a, Int, Int) in Haskell but the equivalent expression in Java<E> F<E, Parser<Tuple<E,Int,Int>>> p() is harder to read and write in Java, mostly because of bad syntax choices for the type language. Beyond that we have problems with inference because there's a poor man's unification for inferred types, so if I write use(build(new SubBar())) where <E> Foo<E> build(E e) and void use(Foo<Bar> foo) the compiler fails to infer the appropriate type for build given the constraints and the expression doesn't type check. Even worse as a programmer I have two ways to "fix" this: add an upcast to the build parameter (i.e. (Bar) new SubBar()) or mess with wildcards to change the use definition (i.e. void use(Foo<? extends Bar> foo)). If the type systems were designed from the ground up with inference in mind they would be significantly different and there wouldn't be more inference problems than we have in SML or Haskell.

The type inference problem in the presence of parametric polymorphism and subtyping like in Java and C# is significantly harder than in Haskell (98) or SML. You're very unlikely to ever get anything like those FP languages' type inference. Scala is a good language to look at in this regard. It too uses (only) local type inference which is more or less as much as one can reasonably expect. That said, you can do way, way more with local type inference than C# is doing (as Scala demonstrates.)

This also has the significant benefit that you can tell by looking at a function what the type is, which is often not the case in ML.

It is not much of a benefit, because, after (global) inference, the compiler knows the types and they can be easily written out and then you can just look at the minibuffer to see the types of variables.

Addition: One thing worth pointing out is that the term "global" can be misleading when interpreted informally. H-M infers principal types and the context for the inference of the type of a particular expression is not the whole program. Also, in ML, definitions are strictly ordered and mutually recursive definitions are explicitly grouped. So, after the principal type of a function (or any binding) has been inferred, it remains invariant no matter what definitions subsequently follow.

There's a practical problem with this when the code fails to compile for any reason, and the compiler can't tell you what the type of a function is supposed to be. This can be particularly problematic if you're working on someone else's code which you aren't already intimately familiar with.

Explicitly annotating types, at least at the top-level function definition level, has real benefits for just about anything more ambitious than code that only one person is going to read.

There's a practical problem with this when the code fails to compile for any reason, and the compiler can't tell you what the type of a function is supposed to be.

Actually, compilers usually report, in case of a type conflict, the expected and actual types. In most cases one of them is usually a good approximation of what the type is supposed to be.

Explicitly annotating types, at least at the top-level function definition level, has real benefits for just about anything more ambitious than code that only one person is going to read.

Which happens quite naturally in ML via module signatures. (And let's not forget that ML also allows type annotations on any expression and pattern.) However, given that one can see the inferred types, I rarely find it useful to have type annotations on the implementation side of a module boundary. The main exception is when I'm puzzled by a type-error (which happens rarely to me while programming in SML --- almost all type errors are immediately clear to me after I look at the offending expression(s)) and insert type annotations to test my assumptions. I almost always remove such annotations after I understand the problem.

Actually, compilers usually report, in case of a type conflict, the expected and actual types. In most cases one of them is usually a good approximation of what the type is supposed to be.

Yes, but when major changes are being made, just getting the types at the places where errors are occurring may not be enough.

I agree that module signatures address this, though. But this brings us back to an approach comparable to the "significant benefit" claimed for Typed Scheme - that you can tell by looking at a function (or the associated module signature) what the type is.

But this brings us back to an approach comparable to the "significant benefit" claimed for Typed Scheme - that you can tell by looking at a function (or the associated module signature) what the type is.

I'm puzzled. How is requiring annotations a benefit of Typed Scheme in this context? The alternative being compared to is ML, which allows annotations to be selectively used by the programmer and the tool support that makes it painless for the programmer to see the inferred types is already available. I really don't see this as a particular benefit (or advantage compared to the alternative being discussed) of Typed Scheme at all.

It would be more reasonable to claim that requiring some type annotations is not much of a hindrance compared to not requiring them, because type annotations can arguably improve readability in the absence of tool support.

Sorry, I was trying to say that when module signatures are used, that the approaches are comparable, i.e. I consider module signatures to also be a "significant benefit" over no type signatures at all.