What is [] (list constructor) in Haskell?
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.
It's (confusingly, I'll grant you) syntactically overloaded to be both a type constructor and a value constructor.
It means that (the value constructor)
[]
has the type that, for all typesa
, it is a list ofa
(which is written[a]
). This is because there is an empty list at every type.The value constructor
[]
isn't typeda -> [a]
because the empty list has no elements, and therefore it doesn't need ana
to make an empty list ofa
's. Compare toNothing :: Maybe a
instead.LYAH is talking about the type constructor
[]
with kind* -> *
, as opposed to the value constructor[]
with type[a]
.
- it is a type constructor (e.g. [Int] is a type), and a data constructor ([2] is a list structure).
- The empty list is a list holding any type
- [a] is like Maybe a, [2] is like Just 2.
- [] is a zero-ary function (a constant) so it doesn't have function type.
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 typesList a
and[a]
respectively -
Cons
=:
, data constructors with typesa -> List a -> List a
anda -> [a] -> [a]
respectively -
Cons 5 Nil
=[5]
or5:[]
, 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.