Typed heaps over identifier sets

Heap Ident (with [CellSpec Ident]) is a dependent function (i : Ident) → CellSpec.type i. It models package state as a collection of named, typed cells indexed by an identifier set Ident.

Composition uses disjoint sums of identifier sets. A heap over α ⊕ β splits canonically into a heap over α and a heap over β, and cell framing follows from ordinary function update: reading cell j after writing cell i ≠ j returns the old value.

Usage

inductive MyCells
  | counter
  | flag
  deriving DecidableEq

instance : CellSpec MyCells where
  type    | .counter => Nat | .flag => Bool
  default | .counter => 0   | .flag => false

def initial : Heap MyCells := Heap.empty
def stepped : Heap MyCells := initial.update .counter 5
example : stepped.get .counter = 5 := by simp [stepped]
example : stepped.get .flag    = false := by simp [stepped]

Stateful handlers can use this layer as a typed cell-keyed state convention: Heap Ident stores one value of the cell-specific type at every identifier.

CellSpec : a typed cell directory

A CellSpec Ident says: each identifier i : Ident carries a value type CellSpec.type i : Type v, with a designated CellSpec.default i. The default is what the heap holds before any cell is written.

Ident lives in Type u, value types in Type v; both universes are independent. Sum composition (Sum.instCellSpec below) requires both operands' universes to match.

class CellSpec (Ident : Type u) : Type (max u (v + 1))

• type : Ident → Type v

  Value type carried by the cell at identifier i.

• default (i : Ident) : type i

  Default value of the cell at identifier i, used to initialize a fresh heap (Heap.empty).

Heap : the dependent-function heap

Heap Ident is the type of states: one cell-value per identifier. Lives in Type max u v.

@[reducible, inline]

abbrev Heap (Ident : Type u) [CellSpec Ident] : Type (max u v)

def Heap.empty {Ident : Type u} [CellSpec Ident] : Heap Ident

The default heap: every cell holds its CellSpec-prescribed default.

@[implicit_reducible]

instance Heap.instInhabited {Ident : Type u} [CellSpec Ident] : Inhabited (Heap Ident)

@[reducible]

def Heap.get {Ident : Type u} [CellSpec Ident] (h : Heap Ident) (i : Ident) : CellSpec.type i

Read the cell at identifier i.

def Heap.update {Ident : Type u} [CellSpec Ident] [DecidableEq Ident] (h : Heap Ident) (i : Ident) (v : CellSpec.type i) : Heap Ident

Write v : CellSpec.type i to cell i, leaving all other cells unchanged.

@[simp]

theorem Heap.get_empty {Ident : Type u} [CellSpec Ident] (i : Ident) : empty.get i = CellSpec.default i

@[simp]

theorem Heap.get_update_self {Ident : Type u} [CellSpec Ident] [DecidableEq Ident] (h : Heap Ident) (i : Ident) (v : CellSpec.type i) : (h.update i v).get i = v

@[simp]

theorem Heap.get_update_of_ne {Ident : Type u} [CellSpec Ident] [DecidableEq Ident] {h : Heap Ident} {i j : Ident} (hij : j ≠ i) (v : CellSpec.type i) : (h.update i v).get j = h.get j

@[simp]

theorem Heap.update_eq_self {Ident : Type u} [CellSpec Ident] [DecidableEq Ident] (h : Heap Ident) (i : Ident) : h.update i (h.get i) = h

@[simp]

theorem Heap.update_idem {Ident : Type u} [CellSpec Ident] [DecidableEq Ident] (h : Heap Ident) (i : Ident) (v w : CellSpec.type i) : (h.update i v).update i w = h.update i w

Sum of identifier sets : CellSpec instance

Composing two packages with identifier sets α and β yields one with identifier set α ⊕ β. The cell directory is the disjoint union of the two, defaults too.

@[implicit_reducible]

instance Sum.instCellSpec {α β : Type u} [CellSpec α] [CellSpec β] : CellSpec (α ⊕ β)

PEmpty : CellSpec instance for the empty identifier set

The trivial heap Heap PEmpty has a unique inhabitant (the empty function). It is useful whenever a typed-heap construction needs a stateless identifier set.

@[implicit_reducible]

instance PEmpty.instCellSpec : CellSpec PEmpty

Heap.split : the canonical decomposition

Heap (α ⊕ β) ≃ Heap α × Heap β, the lynchpin of state-separating composition in this layer. The forward direction restricts to inl / inr cells; the inverse is Sum.rec on the identifier. Both directions reduce by case-analysis on the identifier and are rfl-definitional after cases.

def Heap.split (α β : Type u) [CellSpec α] [CellSpec β] : Heap (α ⊕ β) ≃ Heap α × Heap β

@[simp]

theorem Heap.split_apply_inl {α β : Type u} [CellSpec α] [CellSpec β] (h : Heap (α ⊕ β)) (a : α) : ((split α β) h).fst a = h (Sum.inl a)

@[simp]

theorem Heap.split_apply_inr {α β : Type u} [CellSpec α] [CellSpec β] (h : Heap (α ⊕ β)) (b : β) : ((split α β) h).snd b = h (Sum.inr b)

@[simp]

theorem Heap.split_symm_apply_inl {α β : Type u} [CellSpec α] [CellSpec β] (p : Heap α × Heap β) (a : α) : (split α β).symm p (Sum.inl a) = p.fst a

@[simp]

theorem Heap.split_symm_apply_inr {α β : Type u} [CellSpec α] [CellSpec β] (p : Heap α × Heap β) (b : β) : (split α β).symm p (Sum.inr b) = p.snd b

@[simp]

theorem Heap.split_empty (α β : Type u) [CellSpec α] [CellSpec β] : (split α β) empty = (empty, empty)

@[simp]

theorem Heap.split_update_inl {α β : Type u} [CellSpec α] [CellSpec β] [DecidableEq α] [DecidableEq β] (h : Heap (α ⊕ β)) (a : α) (v : CellSpec.type a) : (split α β) (h.update (Sum.inl a) v) = (((split α β) h).fst.update a v, ((split α β) h).snd)

Splitting after an update on the left identifier set updates only the left split component.

@[simp]

theorem Heap.split_update_inr {α β : Type u} [CellSpec α] [CellSpec β] [DecidableEq α] [DecidableEq β] (h : Heap (α ⊕ β)) (b : β) (v : CellSpec.type b) : (split α β) (h.update (Sum.inr b) v) = (((split α β) h).fst, ((split α β) h).snd.update b v)

Splitting after an update on the right identifier set updates only the right split component.

@[simp]

theorem Heap.split_symm_update_inl {α β : Type u} [CellSpec α] [CellSpec β] [DecidableEq α] [DecidableEq β] (p : Heap α × Heap β) (a : α) (v : CellSpec.type a) : (split α β).symm (p.fst.update a v, p.snd) = ((split α β).symm p).update (Sum.inl a) v

Rebuilding a split heap after updating the left component is the same as updating the composite heap at the corresponding Sum.inl cell.

@[simp]

theorem Heap.split_symm_update_inr {α β : Type u} [CellSpec α] [CellSpec β] [DecidableEq α] [DecidableEq β] (p : Heap α × Heap β) (b : β) (v : CellSpec.type b) : (split α β).symm (p.fst, p.snd.update b v) = ((split α β).symm p).update (Sum.inr b) v

Rebuilding a split heap after updating the right component is the same as updating the composite heap at the corresponding Sum.inr cell.

Sanity check: a two-cell heap

A small example demonstrating cell access, frame, and the canonical Sum-split. If you're reading this to learn the API, this is the right starting point.

inductive HeapExample.Id : Type

• counter : Id
• flag : Id

@[implicit_reducible]

instance HeapExample.instDecidableEqId : DecidableEq Id

@[implicit_reducible]

instance HeapExample.instCellSpecId : CellSpec Id