HORIZON HASKELLDocslts/ghc-9.14.x45dd5372026-10-11Search names, modules, packages, or :: a typeCtrl K

GHC 9.14.1 · lts/ghc-9.14.x · 45dd537 · 2026-10-11

Modulevortex-journal-0.1.0GHC2024

Vortex.Journal.Theory

The journal as a sheaf theory: its sorts, its operations and its laws, each law named. It is a linear/non-linear theory: the resource sorts (tokens and markings) are linear, read in a symmetric monoidal category where nothing is copied or discarded (a net's free model), and the information sorts (logs, answers, versions, snapshots, refusals, conflicts) are cartesian, freely copied. The fold of a log and the recorded answer are the bridge between the two.

sheaf's sorts carry only a name, so the usage of each sort and the mode of each operation's arguments are kept here, beside the theory, and linearityErrors checks the theory's laws against them.

  • 4 types
  • 7 values

The theory

2 declarations
valuelaws :: [(String, Equation)]
#

The laws, each with its name. The numbers are the journal's equations as first stated; the rest are the multiset, version and decision laws they rest on.

Linear and cartesian sorts

6 declarations
datadata Usage
#

How a sort's values may be used: a linear value exactly once, a cartesian one any number of times.

LinearCartesian
Instances2Eq, Show
  • Eq UsageDefined in vortex-journal-0.1.0 · Vortex.Journal.Theory
  • Show UsageDefined in vortex-journal-0.1.0 · Vortex.Journal.Theory
datadata Mode
#

How an operation uses an argument. A linear argument is either Consumed (the resource flows into the result), a Pattern (it only names which tokens, as the second argument of a difference does) or Observed (it is looked at, not used up, as by an inclusion test). A cartesian argument is Copied.

ConsumedPatternObservedCopied
Instances2Eq, Show
  • Eq ModeDefined in vortex-journal-0.1.0 · Vortex.Journal.Theory
  • Show ModeDefined in vortex-journal-0.1.0 · Vortex.Journal.Theory
valueopModes :: [(Op, [Mode])]
#

Each operation with its signature and the mode of each argument.

datadata Role
#

Where an operation stands between the two worlds.

Constructors

  • Resource

    consumes linear values into a linear result

  • Bridge

    makes a linear value from cartesian ones (the fold, pre and post)

  • Observation

    looks at linear values for a cartesian result

  • Information

    cartesian in, cartesian out

Instances2Eq, Show
  • Eq RoleDefined in vortex-journal-0.1.0 · Vortex.Journal.Theory
  • Show RoleDefined in vortex-journal-0.1.0 · Vortex.Journal.Theory
valueopRole :: Op -> [Mode] -> Role
#

An operation's role, from its signature and modes.

Checking linearity

3 declarations
datadata LinearityError
#

Why a theory is not linear in its resources.

Constructors

Instances2Eq, Show
valuelinearityErrors :: [(Op, [Mode])] -> Theory -> [LinearityError]
#

Check a theory's linearity against the usage table and a mode table: every sort and operation is classified, the modes fit the sorts, no operation consumes a resource into a cartesian value, and every law consumes each resource variable once on each side or on neither, and never consumes and observes it on the same side. Premises are guards on the cartesian shadow of the state and are not counted.