Same Kinds for List of Int compared to List of Int -> Int?

Question

Why do both of these have the same kind?

ghci> :k [Int]
[Int] :: *
ghci> :k [Int -> Int]
[Int -> Int] :: *

EDIT per @Gabriel Gonzalez's helpful comment.

I don't understand kinds well, so I don't have a good basis for expecting the above types to vary in kind.

Answer 1

Well, let's check.

Int :: *
[] :: * -> *

So when you apply the Int type to the [] type constructor:

[] Int :: *

Which is just another (legal) way of writing

[Int] :: *

Ok, that one follows pretty easily.

Int :: *
(->) :: * -> * -> *
[] :: * -> *

(->) Int :: * -> *
(->) Int Int :: *

Which is the same as

Int -> Int :: *

and therefore, by the same reasoning as above,

[Int -> Int] :: *

But here's a secret.. Take a closer look at the kind of [].

[] :: * -> *

That means that it's a compile error to put any type inside a list that isn't of kind *. And when you do provide it with something of kind *, the result will always have kind *.

Your confusion comes from not keeping levels separate. Many, many different types have the same kind. After all, kind * more or less means "this type can have values". (There are some minor exceptions, but they're low-level internals things that you have to work quite hard to see.) If you can have a value of a type, it's a very good bet that the type has kind *.

Answer 2

The kind * stands for a concrete type. One way to think of a concrete type is that it doesn't take any type parameters. All of these are concrete types:

Int
Int -> Int

The type [] has kind * -> * -- it takes a concrete type and returns a concrete type. Therefore both of these are concrete types (i.e. has kind *):

[ Int ]
[ Int -> Int ]