Reference 00 · DeepSeek Harness and Cordis

Foundations

Values, types, functions, calls, and pairs

The four levels

For this toy, empty = {}, has_model = {"model"}, and remove_model(s) removes "model" from the set s.

TYPE: effect : State → (State, Undo) VALUE: effect CALL: effect(empty) RESULT: (has_model, remove_model)

Core vocabulary

Term	Meaning	Example
Value	Concrete runtime thing	`empty`
Type	Description of allowed values	`State`
Function	Value mapping inputs to outputs	`effect`
Call	Running a function on an input	`effect(empty)`
Pair	Two values bundled together	`(state, undo)`

Translation table

Plain name	Cordis symbol
State space	`Γ`
Current state	`γ`
New state	`δ`
Effect	`e`
Inverse	`g`
Effect type	`EΓ`

Generic letters

X = input type x : X = one input value Y = output type y : Y = one output value f : X → Y f(x) = y

In f : Γ × X → Γ × Y, γ is the current context and x is an ordinary input:

f(γ, x) = (δ, y)

Here × means a product or pair type, not multiplication. It is the same idea as the pair notation (A, B) from Lesson 00.

One equation, expanded

EΓ = Γ → (Γ × (Γ → Γ)) means: Effect = State → (State, Undo) Undo = State → State actual run: γ : Γ e(γ) = (δ, g)

Do not confuse a type with the names of its returned values:

type: e : Γ → (Γ × (Γ → Γ)) input: γ : Γ run: e(γ) = (new_state, inverse_function) new_state : Γ inverse_function : Γ → Γ

new_state and inverse_function are names introduced after the call. They do not replace the product type.

Important: Γ → Γ is only a function shape. It does not mean undo by itself. For the returned-effect model, the local witness is:

e(γ) = (δ, g) g(δ) = γ

This constrains g at the particular output δ; it says nothing about g at unrelated states. A stronger fixed-pair law would need to be stated separately.

For the toy model-registration example, this behavior has a precondition: the model key must not already be present. Without that precondition, removing "model" could delete an older registration.

Back to Lesson 00