Context Requirementsconcept:context-requirements

satisfies-emptyclaim:satisfies-empty

The empty requirement is satisfied by every context

Law 7 (satisfaction, empty): every environment satisfies the empty row.

Module

Effect4.Machine.Context

Literature

PetricekOrchardMycroft2014, audit C8 (analogy)

∀ {U : Effect4.ServiceUniverse} (self : Effect4.Machine.Env.Context U),
  self.Satisfies Effect4.Machine.Env.Requirement.empty

satisfies-singleclaim:satisfies-single

A singleton requirement is satisfied iff the key is present in the context

Law 8 (satisfaction, singleton): iff the key is bound.

Module

Effect4.Machine.Context

∀ {U : Effect4.ServiceUniverse} (self : Effect4.Machine.Env.Context U) (key : Effect4.ServiceKey),
  Iff (self.Satisfies (Effect4.Machine.Env.Requirement.single key))
    (Eq (self.get? key).isSome Bool.true)

satisfies-unionclaim:satisfies-union

Union requirement satisfaction splits across components

Law 9 (satisfaction, union): iff both rows are satisfied.

Module

Effect4.Machine.Context

∀ {U : Effect4.ServiceUniverse} (self : Effect4.Machine.Env.Context U)
  (r s : Effect4.Machine.Env.Requirement),
  Iff (self.Satisfies (r.union s)) (And (self.Satisfies r) (self.Satisfies s))

satisfies-weakenclaim:satisfies-weaken

Context satisfaction is monotone under requirement row inclusion

Law 10 (weakening): satisfying a row satisfies every subrow.

Module

Effect4.Machine.Context

∀ {U : Effect4.ServiceUniverse} (self : Effect4.Machine.Env.Context U)
  {r s : Effect4.Machine.Env.Requirement},
  self.Satisfies s → Effect4.Row.Subset r s → self.Satisfies r

emission-requirements-completeclaim:emission-requirements-complete

A checked emission's main declaration carries its answer, error and complete requirement row

R5/R8: a checked emission retains an explicit answer, error and complete requirement annotation on its main declaration. This certifies generated syntax, not TypeScript execution.

Module

Effect4.Laws.Codegen.Checked

∀ {program : Effect4.Program.NativeEff} {table : Effect4.Program.RowTable} {name : String}
  (emission : Effect4.Codegen.ModuleEmission program table name),
  Exists fun layers =>
    Exists fun main =>
      Exists fun body =>
        Exists fun answer =>
          Exists fun error =>
            And
              (Eq emission.declarations
                (instHAppendOfAppend.hAppend layers (List.cons main List.nil)))
              (And
                (Eq
                  (Effect4.Program.printDecl name emission.typing.ty body
                    Effect4.Program.nativeScopeKey)
                  (Except.ok main))
                (Eq main.type
                  (Option.some
                    (TypeScript.TypeRef.name (List.cons "Effect" (List.cons "Effect" List.nil))
                      (List.cons answer
                        (List.cons error
                          (List.cons
                            (Effect4.Program.requirementType Effect4.Program.nativeScopeKey
                              emission.typing.ty.requires)
                            List.nil)))))))

provide-dischargesclaim:provide-discharges

Providing a layer discharges its output services from requirement rows

A requirement of the dependent that the dependency provides is discharged.

Module

Effect4.Program.Provision

Literature

Leijen2014, audit P22 (adaptedResult)

∀ (s t : Effect4.Program.LayerTy) (key : Effect4.ServiceKey),
  Effect4.Row.instMembership.mem t.out key →
    Not (Effect4.Row.instMembership.mem t.requires key) →
      Not (Effect4.Row.instMembership.mem (s.provide t).requires key)

provide-closedclaim:provide-closed

A closed dependency layer that covers all requirements yields a closed program

The closure theorem. A dependency that is itself closed and provides everything the dependent needs closes the dependent: Layer<ROut, E, never>. This is the sentence Effect.provide(program, layer) type-checks by, and the sentence a deployment is checked by.

Module

Effect4.Program.Provision

∀ (s t : Effect4.Program.LayerTy),
  t.Closed → Effect4.Row.Subset s.requires t.out → (s.provide t).Closed

build-totalclaim:build-total

Build totality: under a typed leaf semantics, a layer the checker types builds under every context satisfying its requirement row, and the built context satisfies its output row (restored, decisions row 147)

Build totality (build_total, cut at b08f3b58, restored under decisions row 147): under a typed leaf semantics, a layer the checker types builds under every context that satisfies its requirement row, and the built context satisfies its output row.

Module

Effect4.Laws.Program.BuildTotal

∀ {Op : Type} (sig : Effect4.Program.Signature Op) (sem : Effect4.Program.Provision.LeafSem Op),
  Effect4.Program.Provision.LeafSem.Typed sig sem →
    ∀ (l : Effect4.Program.LayerTerm Op) (t : Effect4.Program.LayerTy)
      (ctx : Effect4.Machine.Env.Ctx),
      Eq (Effect4.Program.layerTy sig l) (Option.some t) →
        Effect4.Machine.Env.Context.Satisfies ctx t.requires →
          Exists fun out =>
            And (Eq (Effect4.Program.Provision.build sem l ctx) (Option.some out))
              (Effect4.Machine.Env.Context.Satisfies out t.out)