[Gankro]

Honestly parametric polymorphism is a big slippery slope feature. There's always Just One More Thing -- higher rank/order/kinded types, where clauses, dependent types, specialization... or else you force people to use dynamic checks/allocations/casts that reduce your type-safety and bog the code down relative to the "optimal" design.

Don't get me wrong, I love me some parametric polymorphism, but it's by no means a simple thing as far as I've seen. Especially if you care about the effeciency of things (you can fudge a lot more wih lots of indirection/allocation, like Java does).

[pcwalton]

> Don't get me wrong, I love me some parametric polymorphism, but it's by no means a simple thing as far as I've seen.

I disagree. You should look at OCaml (and Standard ML, though the eqtypes in SML are a botch): generics are dead simple there. Much simpler than Go interfaces, in fact.

Sure, there's always "one more thing" you could add, but that's always true for anything in any language. Slippery slope is a fallacy for this reason.

> or else you force people to use dynamic checks/allocations/casts that reduce your type-safety and bog the code down relative to the "optimal" design

Which is what happens even more if you don't have generics!

[catnaroek]

> eqtypes in SML are a botch

Standard ML's `eqtypes` aren't a bad idea at all:

(0) They ensure that `op=` can only be used on things that actually have decidable equality.

(1) If SML were to be equipped with dependent types in the future, it would make sense to only allow `eqtypes` as type indices. First-order unification can be used on syntactic values of `eqtypes`, so the basic architecture of a Damas-Milner type checker can be retained, in spite of having dependent types.

OTOH, equality and comparisons in OCaml are completely broken.

[catnaroek]

> higher rank

A language designer can provide let polymorphism, refuse to add more, and call it a day.

> (higher) order/kinded types,

This is orthogonal to parametric polymorphism. Higher-kinded types are problematic for inference, and the way Haskell has implemented them has unfortunate consequences for modularity.

> where clauses,

This is just syntactic sugar. (FWIW, what I think Rust needs is better inference, rather than ways to make type signatures less verbose.)

> dependent types,

This is unrelated to parametric polymorphism.

> specialization

This is antithetical to parametric polymorphism.

> or else you force people to use dynamic checks/allocations/casts that reduce your type-safety and bog the code down relative to the "optimal" design.

Standard ML doesn't have dynamic checks or unsafe casts, and I don't find myself longing for them.

[mafribe]

   This is orthogonal to 
   parametric polymorphism

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).

[catnaroek]

> 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.

[mafribe]

   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.

[catnaroek]

> 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.

[snaky]

There's 1ML where those languages are are unified into one language.

http://www.mpi-sws.org/~rossberg/1ml/

[tome]

> A more serious problem with higher-kinded types IMO is that they wouldn't interact very well with an ML-style module system

That's interesting. Why is that?

[catnaroek]

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.