Skip to content

Commit

Permalink
write about inductive definition of lists
Browse files Browse the repository at this point in the history
  • Loading branch information
byorgey committed Jul 23, 2024
1 parent 890e919 commit 371e837
Showing 1 changed file with 43 additions and 3 deletions.
46 changes: 43 additions & 3 deletions docs/reference/list.rst
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,47 @@ In general, lists are written with square brackets.
Disco> 2 ∈ [1,2,3]
T

Inductive definition of lists
-----------------------------
Recursive list processing
-------------------------

Write more here.
Fundamentally, lists in Disco are built from two ingredients:

- The empty list ``[]``
- The "cons" operator ``::`` which adds one more element to the start
of a list. That is, ``x :: rest`` is a list which has a first element ``x``
and where ``rest`` is the rest of the list.

For example, ``1 :: [2,3,4,5]`` represents adding the element ``1`` to
the beginning of the list ``[2,3,4,5]``; it is the same as
``[1,2,3,4,5]``.

::

Disco> 1 :: [2,3,4,5]
[1, 2, 3, 4, 5]

In fact, any list can be written using only ``[]`` and ``::``.

- The empty list is ``[]``;
- ``x :: []`` represents a list with one element;
- ``x :: (y :: [])`` is a list with two elements;
- and so on.

::

Disco> 1 :: []
[1]
Disco> 1 :: (2 :: [])
[1, 2]
Disco> 1 :: (2 :: (3 :: []))
[1, 2, 3]

We can write recursive functions to process lists by :doc:`pattern
matching <pattern>` on ``[]`` and ``::``. For example, below is a
function to add all the elements of a list of natural numbers:

::

sum : List(N) -> N
sum([]) = 0
sum(n :: ns) = n + sum(ns)

0 comments on commit 371e837

Please sign in to comment.