I'd like to refine this to: the fundamental tradeoff is between expressivity of the typing system and computational complexity of type-inference. Hindley-Milner's polymorphic typing system "has hit a sweetspot" (B. Pierce) between expressivity, type-inference. Almost every extension to Hindley-Milner makes full type inference undecidable.
Type inference is just one part of it. That's taking a term and asking "what type could this have?" Another thing you can do is turn it around and ask "what terms have this type?". That question also gets complicated easily.
And that's principled type systems. If you put ad hoc garbage into the types it might be inferrable and whatnot but still be ridiculous to reason about.
This is a very interesting question, but one that is rarely asked by compilers or by programmers, or indeed by theoreticians.
I conjecture that the complexity of both questions is related, although I admit that I'd be hard-pressed even to define properly what the complexity of "what type could this have?" might be.
Oh, it's more common a question than you suggest. If I am writing a block of code and I come to some hole in context, for example `foo (bar _) baz`, and I know what type of thing has to go in that hole, then the very next thing I ask is "What term do I need there?".
This is a big question for theoreticians working on new languages. The problem is called canonicity in that context. Here is an example of such a proof of "What terms have this type [in this context]?": https://arxiv.org/abs/1607.04156
And finally, compilers will ask this question if they're nice to you :) Here is GHC recently gaining the ability to ask this: https://phabricator.haskell.org/D3361
The questions are related by proofs of cut elimination / normalization, which is the compatibility between a term and its context. Complex types describe more complex interactions between terms and contexts. Higher rank polymorphism has undecidable inference because a higher rank type can be used in very complex contexts.
I know that this question is being asked and reseached -- indeed I do research in this direction. But it's not well understood, and it's not nearly as widely asked a question as the type-inference question which the java compiler asks every time you type something like
int n = 2 + 3;
Note that 2+3 needs to be type-inferred.
cut elimination / normalization,
I'm not sure this can be reduced to cut-elimination, because the question "What terms have this type?" can be asked for non-terminating programs as well -- indeed it becomes much
more interesting.
https://arxiv.org/abs/1607.04156
Aside: I'm not following HoTT closely, I guess the problem whether canonicity of the natural number type holds in HoTT in general (= can be derived from the axioms of HoTT alone) is still open?
> I'm not sure this can be reduced to cut-elimination, because the question "What terms have this type?" can be asked for non-terminating programs as well -- indeed it becomes much more interesting.
Oh please share some references :) I think in that context what matters is the progress and preservation parts of cut elimination.
> Aside: I'm not following HoTT closely, I guess the problem whether canonicity of the natural number type holds in HoTT in general (= can be derived from the axioms of HoTT alone) is still open?
The PBE / IPS (= programming-by-example / inductive program synthesis)
literature cares about this a great deal. The approach to PBE / IPS in
the tradition of [1], essentially seeks a unique representative of
each equivalence class of programs w.r.t. to the usual typed notion of
program equivalence.
Since most interesting examples of PBE / IPS use recursion, [1] goes
through a hierarchy of recursion principles, e.g. map, filter, fold,
full recursion. The order of choosing recursion principles matters a
great deal for controlling overfitting, the bête noire of machine
learning.
The basic problem is this: the answer to the question "What terms have this type?" is almost always an infinite set with a great deal of redundancy. E.g. 2+3 and 3+2 are both an answer to "What terms have type Int?". But both answers are contextually indistinguishable, so in practise we only one to see one of them. Since contexual equivalence is typically undecidable there are limits to how clever you can be in a computer program to avoid redundancies. Moreover, in PBE / IPS you typically don't want to have just values, you are interested essentially in short programs inhabiting a type. So cut-eliminiation, at least as conventionally understood, doesn't quite do the job.
[1] J. K. Feser, S. Chaudhuri, I. Dillig, Synthesizing Data Structure
Transformations from Input-Output Examples.
Thanks! This looks like a really interesting part of PL theory that I haven't looked at before. The problem you describe immediately reminds me of Equality Saturation; I wonder if it's been applied in this space: http://www.cs.cornell.edu/~ross/publications/eqsat/
Well the common technical problem is that of representing program fragments along with their equalities so that they can be utilized in the case I linked, and pruned in the case you suggested. It's just a musing though. I look forward to reading up on PBE in depth.
That's why you go with bidirectional type checking instead. This scales much better to more interesting language constructs like rank-n polymorphism, and dependent types, gives better localised error messages, and the downside of having to have some top level annotations is worth it, because that's best practice anyway.
Bidirectional is a nice, pragmatic compromise, but it is a reaction to the difficulty with taking full type inference beyond let-polymorphism. We wouldn't be using bidirectional, if Damas-Hindley-Milner would scale.
I dunno, I do prefer having type directed editing (eg. auto case splitting, and autocomplete), so full type inference is less of a holy grail to me.
Damas-Hindley-Milner inference is also hyper-optimised to a specific point on the design space, and does an excellent job there, but (to echo Conor McBride) I would love to see less conflation of the ideas of execution phase, parametericity, and implicitness going forward.
