haskell - What's the difference between parametric polymorphism and higher-kinded types?

Question

I am pretty sure they are not the same. However, I am bogged down by the common notion that "Rust does not support" higher-kinded types (HKT), but instead offers parametric polymorphism. I tried to get my head around that and understand the difference between these, but got just more and more entangled.

To my understanding, there are higher-kinded types in Rust, at least the basics. Using the "*"-notation, a HKT does have a kind of e.g. * -> *. For example, Maybe is of kind * -> * and could be implemented like this in Haskell.

data Maybe a = Just a | Nothing

Here,

• Maybe is a type constructor and needs to be applied to a concrete type to become a concrete type of kind "*".
• Just a and Nothing are data constructors.

In textbooks about Haskell, this is often used as an example for a higher-kinded type. However, in Rust it can simply be implemented as an enum, which after all is a sum type:

enum Maybe<T> {
    Just(T),
    Nothing,
}

Where is the difference? To my understanding this is a perfectly fine example of a higher-kinded type.

1. If in Haskell this is used as a textbook example of HKTs, why is it said that Rust doesn't have HKT? Doesn't the Maybe enum qualify as a HKT?
2. Should it rather be said that Rust doesn't fully support HKT?
3. What's the fundamental difference between HKT and parametric polymorphism?

This confusion continues when looking at functions, I can write a parametric function that takes a Maybe, and to my understanding a HKT as a function argument.

fn do_something<T>(input: Maybe<T>) {
    // implementation
}

again, in Haskell that would be something like

do_something :: Maybe a -> ()
do_something :: Maybe a -> ()
do_something _ = ()

which leads to the fourth question.

4. Where exactly does the support for higher-kinded types end? Whats the minimal example to make Rust's type system fail to express HKT?

Related Questions:

I went through a lot of questions related to the topic (including links they have to blogposts, etc.) but I could not find an answer to my main questions (1 and 2).

1. In Haskell, are "higher-kinded types" *really* types? Or do they merely denote collections of *concrete* types and nothing more?
2. Generic struct over a generic type without type parameter
3. Higher Kinded Types in Scala
4. What types of problems helps "higher-kinded polymorphism" solve better?
5. Abstract Data Types vs. Parametric Polymorphism in Haskell

Update

Thank you for the many good answers which are all very detailed and helped a lot. I decided to accept Andreas Rossberg's answer since his explanation helped me the most to get on the right track. Especially the part about terminology.

I was really locked in the cycle of thinking that everything of kind * -> * ... -> * is higher-kinded. The explanation that stressed the difference between * -> * -> * and (* -> *) -> * was crucial for me.

question from:https://stackoverflow.com/questions/48523571/whats-the-difference-between-parametric-polymorphism-and-higher-kinded-types

Answer 1

Some terminology:

• The kind * is sometimes called ground. You can think of it as 0th order.
• Any kind of the form * -> * -> ... -> * with at least one arrow is first-order.
• A higher-order kind is one that has a "nested arrow on the left", e.g., (* -> *) -> *.

The order essentially is the depth of left-side nesting of arrows, e.g., (* -> *) -> * is second-order, ((* -> *) -> *) -> * is third-order, etc. (FWIW, the same notion applies to types themselves: a second-order function is one whose type has e.g. the form (A -> B) -> C.)

Types of non-ground kind (order > 0) are also called type constructors (and some literature only refers to types of ground kind as "types"). A higher-kinded type (constructor) is one whose kind is higher-order (order > 1).

Consequently, a higher-kinded type is one that takes an argument of non-ground kind. That would require type variables of non-ground kind, which are not supported in many languages. Examples in Haskell:

type Ground = Int
type FirstOrder a = Maybe a  -- a is ground
type SecondOrder c = c Int   -- c is a first-order constructor
type ThirdOrder c = c Maybe  -- c is second-order

The latter two are higher-kinded.

Likewise, higher-kinded polymorphism describes the presence of (parametrically) polymorphic values that abstract over types that are not ground. Again, few languages support that. Example:

f : forall c. c Int -> c Int  -- c is a constructor

The statement that Rust supports parametric polymorphism "instead" of higher-kinded types does not make sense. Both are different dimensions of parameterisation that complement each other. And when you combine both you have higher-kinded polymorphism.