What is [] (list constructor) *really* in Haskell?

Question

I'm Having problems understanding functors, specifically what a concrete type is in LYAH. I believe this is because I don't understand what [] really is.

fmap :: (a -> b) -> f a -> f b  

1. Is [], a type-constructor? Or, is it a value constructor?
2. What does it mean to have the type of: [] :: [a]?
3. Is it like Maybe type-constructor, or Just value constructor?
   1. If it is like Just then how come Just has a signature like Just :: a -> Maybe a rather than Just :: Maybe a, in other words why isn't [] typed [] :: a -> [a]
4. LYAH says this as it applies to functors: Notice how we didn't write instance Functor [a] where, because from fmap :: (a -> b) -> f a -> f b, we see that the f has to be a type constructor that takes one type. [a] is already a concrete type (of a list with any type inside it), while [] is a type constructor that takes one type and can produce types such as [Int], [String] or even [[String]]. I'm confused though the type of [] implies it is like a literal for [a] what is LYAH trying to get at?

Answer 1

1) It's (confusingly, I'll grant you) syntactically overloaded to be both a type constructor and a value constructor.

2) It means that (the value constructor) [] has the type that, for all types a, it is a list of a (which is written [a]). This is because there is an empty list at every type.

3) The value constructor [] isn't typed a -> [a] because the empty list has no elements, and therefore it doesn't need an a to make an empty list of a's. Compare to Nothing :: Maybe a instead.

4) LYAH is talking about the type constructor [] with kind * -> *, as opposed to the value constructor [] with type [a].

Answer 2

1. it is a type constructor (e.g. [Int] is a type), and a data constructor ([2] is a list structure).
2. The empty list is a list holding any type
3. [a] is like Maybe a, [2] is like Just 2.
4. [] is a zero-ary function (a constant) so it doesn't have function type.

Answer 3

Just to make things more explicit, this data type:

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

...has the same structure as the built-in list type, but without the (nicer, but potentially confusing) special syntax. Here's what some correspondences look like:

• List = [], type constructors with kind * -> *
• List a = [a], types with kind *
• Nil = [], values with polymorphic types List a and [a] respectively
• Cons = :, data constructors with types a -> List a -> List a and a -> [a] -> [a] respectively
• Cons 5 Nil = [5] or 5:[], single element lists
• f Nil = ... = f [] = ..., pattern matching empty lists
• f (Cons x Nil) = ... = f [x] = ...`, pattern matching single-element lists
• f (Cons x xs) = ... = f (x:xs) = ..., pattern matching non-empty lists

In fact, if you ask ghci about [], it tells you pretty much the same definition:

> :i []
data [] a = [] | a : [a]           -- Defined in GHC.Types

But you can't write such a definition yourself because the list syntax and its "outfix" type constructor is a special case, defined in the language spec.

Answer 4

The type is described (in a GHCI session) as:

$ ghci
Prelude> :info []
data [] a = [] | a : [a] -- Defined 

We may also think about it as though it were defined as:

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

or

data List a = EmptyList
            | ListElement a (List a)

Type Constructor

[a] is a polymorphic data type, which may also be written [] a as above. This may be thought about as though it were List a

In this case, [] is a type constructor taking one type argument a and returning the type [] a, which is also permitted to be written as [a].

One may write the type of a function like:

sum :: (Num a) => [a] => a

Data Constructor

[] is a data constructor which essentially means "empty list." This data constructor takes no value arguments.

There is another data constructor, :, which prepends an element to the front of another list. The signature for this data constructor is a : [a] - it takes an element and another list of elements and returns a resultant list of elements.

The [] notation may also be used as shorthand for constructing a list. Normally we would construct a list as:

myNums = 3 : 2 : 4 : 7 : 12 : 8 : []

which is interpreted as

myNums = 3 : (2 : (4 : (7 : (12 : (8 : [])))))

but Haskell permits us also to use the shorthand

myNums = [ 3, 2, 4, 7, 12, 8 ]

as an equivalent in meaning, but slightly nicer in appearance, notation.

Ambiguous Case

There is an ambiguous case that is commonly seen: [a]. Depending on the context, this notation can mean either "a list of a's" or "a list with exactly one element, namely a." The first meaning is the intended meaning when [a] appears within a type, while the second meaning is the intended meaning when [a] appears within a value.