The more powerful a type system, the easier it is to manipulate terms but the harder it is to reason about types. That's the fundamental tradeoff.
Being able to specify your own type language is like having an untyped language governing your term language.
There are promising directions though. In 20 years they might even have matured.
That's the fundamental tradeoff.
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.
what terms have this type?
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.
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.
int n = 2 + 3;
cut elimination / normalization,
https://arxiv.org/abs/1607.04156
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?
I haven't either, but I think that's the case.
share some references
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.
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.
less conflation of