Higher-rank types are not orthogonal to parametric polymorphism, instead they are a special case. You can see this when you realise that rank-k polymorphism is a subsystem of System F (the paradigmatic typing system for parametric polymorphism) for any k. The let-polymorphism of the ML-family is just rank-1. See Chapters 22 and 23 of Pierce's great "Types and Programming Languages".
Higher-kinded types are
problematic for inference
That is true, but already type inference for rank-3 polymorphism is undeciable, and the same is true for System F polymorphism.
In practise, Haskell needs only few kind-annotations to make kind inference possible. This is helped by unannotated kind variables having kind * in Haskell (IIRC).
> Higher-rank types are not orthogonal to parametric polymorphism, instead it's a special case.
Errr, sorry, I only saw “higher-kinded”, not “higher-ranked”. But, of course, you are right.
> That is true, but already type inference for rank-3 polymorphism is undeciable, hence also System F polymorphism.
Let polymorphism covers 95% of what most programmers need. So if a language designer feels particularly risk-averse (a perfectly legitimate position), they can provide just let polymorphism and ML-style type inference, and then call it a day.
Of course, higher-ranked polymorphism is a nice thing to have, and you can require type annotations when you use more (as Haskell does).
> In practise, Haskell needs only few kind-annotations to make kind inference possible.
A more serious problem with higher-kinded types IMO is that they wouldn't interact very well with an ML-style module system, where you can define an abstract type whose internal implementation is a synonym. `newtype` is an ugly hack.
provide just let polymorphism
and ML-style type inference
I mostly agree with this, and this should be the default starting point for any new programming language. If B. Eich had built Javascript on this basis, the world would have been a better place.
My main caveat would be that even a basic language needs a mechanism to glue related code together, objects, modules, structs with row-typing, existentials, not sure. But something.
> My main caveat would be that even a basic language needs a mechanism to glue related code together, objects, modules, structs with row-typing, existentials, not sure. But something.
While not perfect, I think ML's solution is pretty reasonable: a separate module language, whose complexity doesn't infect the core language.
I'm aware of it. But my previous suggestions were in part shaped by the stated goals of Go's designers: to keep the language simple and easy to learn for non-language geeks. 1ML is really cool, but its type system can be intimidating: small vs. large types, incomplete inference, type-checking as elaboration into System F-omega, etc. OTOH, plain Damas-Milner is dead simple.
Another problem with 1ML is that it's only a research prototype for now, so we can't take it "for a spin". Given the 1ML inventor's main job, this is unlikely to change any time soon, unless some kind soul takes on the 1ML project lead.
Because, in ML, a type-level function that one module views as an abstract type constructor might be viewed by another module as a type synonym. Haskell's type language allows type constructors to appear partially applied, but requires type synonyms to appear fully applied, so it can't deal with this discrepancy.
In practise, Haskell needs only few kind-annotations to make kind inference possible. This is helped by unannotated kind variables having kind * in Haskell (IIRC).