3 ms·

Can someone steeped in type theory explain the following: I never understood why the default for [a] means that the list could be empty. If ... foo: [a]

Can someone steeped in type theory explain the following: I never understood why the default for [a] means that the list could be empty. If ... foo: [a] -> a ... foo is supposed to get a list of a's, it should get a list of a's, with at least one a. If the list can be empty, then explicitly annotate it so: foo: [a*] -> a One way or the other one has to deal with the empty list explicitly (in the signature). If you allow empty lists, it will have to return a 'Maybe a'. It seems to me that it just makes processing the result easier in the common case if the input were to be constrained.

noelwelsh 2y ago
The definition of a list is that it contains zero or more elements. There's nothing deep about it; it's just the way the type is defined (and always has been, back to the early days of Lisp from which functional programming evolved.)
- TeMPOraL 2y ago
  Conceptually, I see this as seeing a list as its own thing, independent of its contents. That is, a List<Int> is a value in itself, that can exist even if no instance of an Int exists anywhere in the program; it'll just be a List of Int that happens to have zero Ints in it. Probably makes more sense when you come from imperative programming background, where List<Int> is a piece of mutable state that you can construct and then fill, in two explicitly separate steps (and then possibly empty it again in yet another step). Then again, I believe even mathematicians are fine with ideas of an empty set, or of a one-element set being distinct from the element itself.
  - nyssos 2y ago
    > Then again, I believe even mathematicians are fine with ideas of an empty set, or of a one-element set being distinct from the element itself. Especially mathematicians. Distinguishing stuff and structure is a common theme throughout mathematics.
- sriram_malhar 2y ago
  Yes, that's true. But Lisp is untyped. The notation [a] could just as easily have meant a non-empty list
  - HelloNurse 2y ago
    It is necessary to represent the empty list whose elements (if it had any) are type A, and its type must be the same as a nonempty list of A, because concatenating the two must be a well-defined and representable operation while concatenating empty lists of different types must be as wrong as concatenating nonempty ones. Moreover, in practice most variables, function parameters and the like should be declared as a possibly empty list of A, without special cases.
brandonspark 2y ago
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.
layer8 2y ago
The type of elements and the number of elements are two orthogonal aspects. You might need at least one element, or you might need at least two elements, or you might need an even number of elements, and so on. This is independent from whether you need the elements to be of type a (or some other condition on the element types). Ideally, all these conditions could be expressed in the type system. But the requirement "all elements must be of type a" by itself does not imply "there must be at least one element", nor does it necessarily imply having to special-case the empty list.
zeendo 2y ago
Haskell has this simply for historical reasons. It's a wart and we wish it weren't so but changing it would break a lot of legacy code (and probably have adverse performance impacts in some cases) so it remains. So as it is today, [a] indeed means it can be empty or not. And a function signature of "[a] -> a" is essentially an unsafe partial function. That isn't to say you _have_ to write it this way for new things and there are packages like https://hackage.haskell.org/package/safe https://hackage.haskell.org/package/safe which provide non-partial/safe versions of the various unsafe base functions (like head, maximum and friends). The base package in Haskell also includes nonempty which is probably what you want in a lot of cases, anyway.

noelwelsh 2y ago

The definition of a list is that it contains zero or more elements. There's nothing deep about it; it's just the way the type is defined (and always has been, back to the early days of Lisp from which functional programming evolved.)

TeMPOraL 2y ago
Conceptually, I see this as seeing a list as its own thing, independent of its contents. That is, a List<Int> is a value in itself, that can exist even if no instance of an Int exists anywhere in the program; it'll just be a List of Int that happens to have zero Ints in it. Probably makes more sense when you come from imperative programming background, where List<Int> is a piece of mutable state that you can construct and then fill, in two explicitly separate steps (and then possibly empty it again in yet another step). Then again, I believe even mathematicians are fine with ideas of an empty set, or of a one-element set being distinct from the element itself.
- nyssos 2y ago
  > Then again, I believe even mathematicians are fine with ideas of an empty set, or of a one-element set being distinct from the element itself. Especially mathematicians. Distinguishing stuff and structure is a common theme throughout mathematics.
sriram_malhar 2y ago
Yes, that's true. But Lisp is untyped. The notation [a] could just as easily have meant a non-empty list
- HelloNurse 2y ago
  It is necessary to represent the empty list whose elements (if it had any) are type A, and its type must be the same as a nonempty list of A, because concatenating the two must be a well-defined and representable operation while concatenating empty lists of different types must be as wrong as concatenating nonempty ones. Moreover, in practice most variables, function parameters and the like should be declared as a possibly empty list of A, without special cases.

brandonspark 2y ago

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.

layer8 2y ago

The type of elements and the number of elements are two orthogonal aspects. You might need at least one element, or you might need at least two elements, or you might need an even number of elements, and so on. This is independent from whether you need the elements to be of type a (or some other condition on the element types). Ideally, all these conditions could be expressed in the type system. But the requirement "all elements must be of type a" by itself does not imply "there must be at least one element", nor does it necessarily imply having to special-case the empty list.

zeendo 2y ago

Haskell has this simply for historical reasons. It's a wart and we wish it weren't so but changing it would break a lot of legacy code (and probably have adverse performance impacts in some cases) so it remains. So as it is today, [a] indeed means it can be empty or not. And a function signature of "[a] -> a" is essentially an unsafe partial function. That isn't to say you _have_ to write it this way for new things and there are packages like https://hackage.haskell.org/package/safe https://hackage.haskell.org/package/safe which provide non-partial/safe versions of the various unsafe base functions (like head, maximum and friends). The base package in Haskell also includes nonempty which is probably what you want in a lot of cases, anyway.