[brandonspark]

There's no reason this couldn't be done. Indeed, in OCaml (which I am more familiar with), you could easily define:

```ocaml

type 'a nonempty = Single of 'a | Cons of 'a * 'a nonempty

```

This would be the type of lists that contain one or more elements of the type parameter.

I think it's just convention that typically, when we talk about lists, we are interested in the empty case as well. Finding "all X that satisfy P in Y", as a general computational problem, is _very_ common (consider: filtering a list, querying for a predicate in a collection, finding sequences of moves in a search space), and generally could result in an empty list as a possible output.

In a non-practical sense, if you want the type theory, another reason is you can think of `[a]` as the free monoid on the collection of `a`. In other words, strings of elements of `a`, joined via concatenation. This monoid requires a unit, which is the empty list.