Explicit state

This article is part of a series of six articles:

At first glance, explicit state is just a minor extension to the declarative computation model: in addition to depending on its arguments, the component’s result also depends on an internal parameter, which is called its “state”. This parameter gives the component a long-term memory, a “sense of history” if you will.

A state is a sequence of values in time that contain the intermediate results of a desired computation.

We have already programmed with state in the declarative model. For example we have used Accumulators that express state.

Implicit (declarative) state

This kind of state only needs to exist in the mind of the programmer. It does not need any support from the computation model. There is also no need for the function callers to know about the internal state and for modularity reasons the callers should not know about the internal state.

Explicit state

It can be useful for a function to have state that lives across function calls and that is hidden from the callers.

An explicit state in a function is a state whose lifetime extends over more than one function call without being present in the functions arguments.

Explicit state cannot be expressed in the declarative model. To express explicit state we need a new language construct that has a name, an indefinite lifetime, and a content that can be changed. You will know this kind of language construct as mutable variables or cells.

Relation to declarative programming

In general, a stateful program is no longer declarative since running the program with the same inputs can give different outputs depending on the internal state. However it is possible to write stateful programs that behave as if they were declarative.

It is a good design principle to write stateful components so that they behave declaratively.

It is often possible to take a declarative program and convert it to a stateful program with the same behaviour by replacing the declarative state with explicit state. The reverse direction is often possible as well. There can be several reasons to choose a declarative or a stateful model, e.g. expressiveness, performance or reasoning.

Reasoning with state

Programs that use state in a haphazard way are very difficult to understand. If the state is visible throughout the whole program then it can be assigned anywhere. The only way to reason is to consider the whole program at once, but this is practically impossible for big programs.

The method of invariant assertions allows us to reason independently about parts of programs and therefore gets back one of the strongest properties of declarative programming. However, this property is only achieved at the price of a rigorous organisation of the program.

The basic idea is to organise the program as a hierarchy of abstract data types (ADTs). Each ADT can use other ADTs in their implementation, forming a directed graph of ADTs. Invariant assertions are a part of design-by-contract programming. An invariant is a condition that can be relied upon to be true during execution of a program, or some portion of it.

Normal termination

The partial correctness reasoning above does not say anything about whether or not a program terminates correctly. It just says, if a program terminates correctly then such and such is true. We also have to prove termination. The termination of a program could fail when it starts an infinite loop or when an error occurs and an exception is raised.

We can try our best to guarantee normal termination by:

  • Progress reasoning: Each time there is a loop or a recursion we have to be aware of the danger that it will not terminate. To show that a loop terminates it suffices to show that there is a function that approaches the base case of recursion upon successive iterations.
  • Type checking: Static type checking should prevent most type errors beforehand.
  • Testing: Other kinds of errors need other kinds of checking and software testing is key to finding and preventing those errors.

Resources: CTM