Skip to content
coeval

The ladder

coeval does not read a definition to learn what a document means. It asks the document a question, and the answer comes from the first rung of the ladder that has an entry for the verb.

The glyphs so far: 6, 1 new on this page
  • 42Data: a value without a type
  • number
    42
    A document: the tab is its type
  • number
    42
    A dashed tab: the container declares the type
  • add
    number
    1
    number
    2
    Parts: a card inside a card
  • kindA kind: a document of type kind
  • OKDA rung: own, kind or defaultnew
  1. Own entry. The header of a document can name an evaluator for a verb, in its field own. This changes one document.
  2. Kind. The kind names an evaluator for each verb that it answers. The type comes from the envelope, or else from the container.
  3. Default. The world has a default evaluator for some verbs, for example a JSON view.
Document
Verb
The answerrule.viewThe evaluator is rule.view, from the kind.
The document
rule
use“stack”withgap8
The JSON
{
  "type": "rule",
  "value": {
    "use": "stack",
    "with": { "gap": 8 }
  }
}
The question: view. It starts at rung 1.
  1. 3DefaultNot visited.
    view → json.view, check → schema.check
  2. 2KindAnswers with rule.view.
    rule: eval → rule.eval, view → rule.view
  3. 1Own entryNo entry for view.
    No own entries.
A question visits the rungs in order. The first rung with an entry for the verb answers. The type comes from the envelope or from the container. It does not come from the shape of the data.

Try these

Section titled “Try these”
  • Select A card in a list. The card is bare, and its list declares the type card. Its tab is dashed.
  • Select A typo. The kind rul does not exist. The question stops with an error, because the ladder does not guess a name.
  • Select Plain data and the verb view. No type is known, thus the default answers.
  • Give the document its own entry. The question stops at the first rung.

Why “coinductive”

Section titled “Why “coinductive””

A document is finite data that a store can keep and a checker can examine. Its meaning is different: it is the set of answers to questions. Nothing outside the ladder decides the meaning, and the answers come when something asks. Thus the meaning of a document is a set of observations, not a definition. The theory calls this view coinductive, and it gives coeval its name.

The cost of the rule

Section titled “The cost of the rule”

A new kind is one write: a document with the entries of the kind. A new verb needs a default, or an entry in each kind that answers it. This is the usual trade between objects and data types. The default rung keeps a new verb cheap.