gleamunison/effect_evidence

Whether a definition is effectful — the fact the evidence gate turns on.

A pure definition must be tested; an effectful one may instead carry a human io attestation, because a suite cannot drive real IO. That decision needs one answer to “is this effectful?”, and it belongs to the term, not to the command asking: publish and run must agree, or a definition gets admitted by one gate and refused by the other.

The term is the honest source. A top-level value type carries no requirement row, but an ability call is right there as a Do node.

Types

BatchEntry

</>

One elaborated definition in a publication batch.

pub type BatchEntry {
  BatchEntry(name: String, content_ref: String, term: ast.Term)
}

Constructors

BatchEntry(name: String, content_ref: String, term: ast.Term)

Values

batch_effectful

</>

pub fn batch_effectful(entries: List(BatchEntry)) -> List(String)

Names in the batch that must carry effect evidence.

A definition is effectful when its own term performs an ability op, or when it transitively references another batch definition that does. This is conservative: a Do sitting under a Handle still counts, matching the original single-definition check extended across the batch graph.

definition_is_effectful

</>

pub fn definition_is_effectful(
  definition: ast.Definition,
) -> Bool