Why is a list of kind * -> *?

Question

In GHCI, using :info on a list [], will show that it is of kind * -> *

Prelude> :i []
type [] :: * -> *

How can I reason about this when I can construct a list with multiple elements, e.g. [1, 2, 3]

Answer 1

Lists have special syntax in Haskell.

You could define a datatype such as lists yourself, using normal syntax, as

data List a = Nil | Cons a (List a)

Now note in particular that with this definition, the empty list is written Nil rather than [], and that the type of lists of integers is written List Int rather than [Int].

If we look at the type of lists of integers, it consists of two components, the List and the Int. Looking at List in isolation, it is a "type constructor", a function on the type-level that takes an argument which is itself a type (such as Int) and forms a new type List Int. It is useful to be able to talk about List without an argument in some circumstances, for example as an argument to other type constructors, or as an argument of type classes such as Functor or Applicative. Therefore, List has kind * -> *, because it expects one argument.

For Haskell's built-in list type, as stated above, List Int is typically written [Int], but it can also be written as [] Int, and indeed [] corresponds to List in isolation, refers to the list type constructor written without being applied to its argument, and it therefore also has kind * -> *.

Tuple type constructors are also having special syntax in Haskell. For example, a pair of an integer and a Boolean is typically written as (Int, Bool), but it can also be written as (,) Int Bool, where (,) is the unapplied pair type constructor, and has kind * -> * -> *, because it expects two arguments.

Answer 2

First, please forget about those * symbols. They're a historic oddity; Haskell is switching to the name Type for them. In GHC-8.x, you should turn on the -XTypeInType extension to allow that, and -XNoStarIsType to disable the old syntax. Then it will read

> :k []
[] :: Type -> Type

This function arrow has nothing to do with how many elements are to be put in the list, rather it is about what type of element is supposed to be contained in the list – and that is always exactly one type. The list values of that list type will of course be able to contain multiple elements of that contained type

       Int ⟼ [Int]        % [3], [74,12,-394], []
      Bool ⟼ [Bool]       % [True], repeat [False]
(Int,Bool) ⟼ [(Int,Bool)] % [(0,False)], [(3,True)]
      Char ⟼ String       % ['y'], "bla bla", ""

Contrast this with the HList container: heterogeneous lists which contain multiple different types (exactly one element of each type):

> :k HList
HList :: [Type] -> Type

And now

       '[Int] ⟼ HList '[Int]          % HL[3], HL[-394]
          '[] ⟼ HList '[]             % HL[]
'[Int,String] ⟼ HList '[(Int,String)] % HL[(0,"0")], HL[(1,"one")]