Introduction
You are working on a project to develop a train scheduling system for a busy railway network.
You've been asked to develop a prototype for the train routes in the scheduling system.
Each route consists of a sequence of train stations that a given train stops at.
Instructions
Your team has decided to use a doubly linked list to represent each train route in the schedule.
Each station along the train's route will be represented by a node in the linked list.
You don't need to worry about arrival and departure times at the stations.
Each station will simply be represented by a number.
Routes can be extended, adding stations to the beginning or end of a route.
They can also be shortened by removing stations from the beginning or the end of a route.
Sometimes a station gets closed down, and in that case the station needs to be removed from the route, even if it is not at the beginning or end of the route.
The size of a route is measured not by how far the train travels, but by how many stations it stops at.
The linked list is a fundamental data structure in computer science, often used in the implementation of other data structures.
As the name suggests, it is a list of nodes that are linked together.
It is a list of "nodes", where each node links to its neighbor or neighbors.
In a singly linked list each node links only to the node that follows it.
In a doubly linked list each node links to both the node that comes before, as well as the node that comes after.
If you want to dig deeper into linked lists, check out this article that explains it using nice drawings.
Stateful data structures
In functional languages, such as Lean, most values are immutable by design.
This means updates are usually made by producing a new value.
Both the old and the new value coexist and may be referenced and used.
However, there are many situations where a stateful value is desired, or even necessary.
A stateful value is updated by mutation, replacing the old value rather than creating a new one.
After a mutation, only the updated value remains accessible.
Note that mutations can break some guarantees of the language.
A pure function must always return the same result for the same set of inputs, but if an input may change over time, then the function may return different results even when called with the same arguments.
Similarly, if a function can produce external changes other than returning a result, or can read from sources other than its parameters, then two calls to the same function may have different and sometimes unpredictable outcomes.
To handle such stateful behavior, Lean, like other functional languages, requires that effectful functions be wrapped in a special kind of structure that distinguishes them from pure functions.
These structures are called monads.
It is important to note that, although every stateful value lives inside some effectful monad, not every monad represents mutable state.
Notable examples of "pure" monads are Option, Except and Id.
In this exercise, you are going to define a stateful data structure called LinkedList.
Instances of this data structure are updated by mutation.
To support this, all functions are wrapped inside the ST monad.
In this monad, mutable state is the only side effect, and mutable references cannot escape.
For more information, you can check the reference.
Source
Classic computer science topic
