Lesson 00 · DeepSeek Harness and Cordis

Values, Types, and Function Calls

The zero-prerequisite foundation for the entire formal course

Your tangible win

After this lesson, you will be able to look at a compact formal statement and separate four different things:

Most of the confusion in formal papers comes from accidentally treating a description of a value as if it were the value being executed. This lesson prevents that mistake.

1. Values are the things in memory

A value is a concrete thing a program can hold or use.

All of those are values. A function is also a value. The function named remove_model is not the same thing as running it.

For this running example, let a State be a set of capability names:

Because remove_model removes the model key from {"model"}, we can verify:

Compare the difference:

The first line refers to a function. The second line runs the function on one concrete state and, in our example, produces {}.

2. Types describe allowed values

A type is a description of what kind of value something is allowed to be. It is not one concrete value.

This is why a type signature does not show one current state:

This does not mean that abs is currently receiving a number. It says that whenever we give abs a number, it returns a number.

The 9 appears only in the actual call, not in the general type description.

3. Function types

The arrow symbol describes a function type:

Read it as:

A function that accepts an A and returns a B.

Examples:

The last one describes a state transformation:

The type tells us the input and output categories. The call tells us what happened for one particular input.

What do X and x mean?

Formal writing often uses uppercase letters for types and lowercase letters for values:

So x is not a special kind of thing. It is just a placeholder name, like empty or 9. In the Cordis paper, a generic line such as f_impure : X → Y means: the function accepts some ordinary input x : X and returns some result y : Y. Later, when context is made explicit, the same idea can be written:

That says the function receives both the current context γ and the ordinary input x, then returns a new context δ and an ordinary result y.

4. A pair is two values bundled together

A pair, also called a product, is a value containing two values:

The pair type can be written with the product constructor:

A pair value is written with concrete values:

Some informal writing uses (A, B) as shorthand for the pair type, but keep the levels separate: uppercase A and B name types, while lowercase a and b name values.

Here × does not mean multiplication. It means "a pair of an A and a B."

For example, the pair type (State, Undo) has:

5. Functions can return pairs

Put the previous two ideas together. First, name the type of an undo function:

An undo function is just a state-transforming function that we intend to use for recovery; the type alone does not prove that it really undoes anything.

This says:

1. effect is a function.
2. It accepts one State.
3. It returns one pair.
4. The pair contains a new State and an Undo function.

Now make it concrete:

That is the complete idea before any Greek notation appears.

6. Now translate into the paper's symbols

Only now do we introduce the paper's names:

Our plain-English type:

becomes:

Notice the direction of the explanation: the formal line does not turn into a different type. We first choose an input and run the function:

After that run, we can name the two returned values. Their types are:

So (new_state, inverse_function) is the result of a call, not a replacement for the type-level pair Γ × (Γ → Γ).

And our concrete call:

becomes:

The symbols are not introducing a new operation. They are short names for the same ordinary idea:

7. What the course will do next

Lesson 01 combines contexts, inverse effects, accumulators, and dependency predicates. Later lessons add the unified context, lifecycle calculus, asynchronous transitions, and system-wide theorems.

Retrieval checkpoint

Try to answer before revealing the models.