Exception Postcondition Types

Heterogeneous lists of exception postconditions for monads with multiple exception layers.

An EPost is a type-level list that tracks postconditions for each exception type in a monad transformer stack. For example, ExceptT Nat (ExceptT String (StateM σ)) would use EPost⟨Nat → σ → Prop, String → σ → Prop⟩ to specify postconditions for both exception types.

Overview

• EPost.nil is the empty exception postcondition (no exceptions).
• EPost.cons eh et pairs a head postcondition type eh with a tail et.
• EPost⟨e₁, e₂, ...⟩ is notation for nested EPost.cons.
• epost⟨v₁, v₂, ...⟩ is notation for constructing exception postcondition values.

structure Std.Do'.EPost.nil : Type

The empty exception postcondition type, used when a monad has no exception layers.

structure Std.Do'.EPost.cons (eh : Type u) (et : Type v) : Type (max u v)

A cons cell pairing a head exception postcondition type eh with a tail et.

For a monad with exception type ε over lattice l, the head eh is typically ε → l and the tail et tracks remaining exception layers.

• head : eh

  The head exception postcondition.

• tail : et

  The tail exception postconditions.

Partial Order and Complete Lattice Instances

Exception postconditions are ordered componentwise: p ⊑ q iff each component of p is below the corresponding component of q.

@[implicit_reducible]

instance Std.Do'.instPartialOrderNil : Lean.Order.PartialOrder EPost⟨⟩

The trivial partial order on EPost.nil: all values are equal.

@[implicit_reducible]

instance Std.Do'.instCompleteLatticeNil : Lean.Order.CompleteLattice EPost⟨⟩

The trivial complete lattice on EPost.nil.

@[implicit_reducible]

instance Std.Do'.instPartialOrderCons {eh : Type u_1} {et : Type u_2} [Lean.Order.PartialOrder eh] [Lean.Order.PartialOrder et] : Lean.Order.PartialOrder (EPost.cons✝ eh et)

Componentwise partial order on EPost.cons, via PProd.

@[implicit_reducible]

instance Std.Do'.instCompleteLatticeCons {eh : Type u_1} {et : Type u_2} [Lean.Order.CompleteLattice eh] [Lean.Order.CompleteLattice et] : Lean.Order.CompleteLattice (EPost.cons✝ eh et)

Componentwise complete lattice on EPost.cons, via PProd.

Ordering Lemmas

theorem Std.Do'.EPost.cons.rel_head {eh : Type u_1} {et : Type u_2} [Lean.Order.PartialOrder eh] [Lean.Order.PartialOrder et] {p q : EPost.cons✝ eh et} (h : Lean.Order.PartialOrder.rel p q) : Lean.Order.PartialOrder.rel p.head q.head

Extract a head ordering from an EPost.cons ordering.

theorem Std.Do'.EPost.cons.rel_tail {eh : Type u_1} {et : Type u_2} [Lean.Order.PartialOrder eh] [Lean.Order.PartialOrder et] {p q : EPost.cons✝ eh et} (h : Lean.Order.PartialOrder.rel p q) : Lean.Order.PartialOrder.rel p.tail q.tail

Extract a tail ordering from an EPost.cons ordering.

theorem Std.Do'.EPost.cons_rel {e : Type u_1} {e' : Type u_2} [Lean.Order.PartialOrder e] [Lean.Order.PartialOrder e'] (eposth : e) (epostt : e') (epost : EPost.cons✝ e e') : Lean.Order.PartialOrder.rel eposth epost.head → Lean.Order.PartialOrder.rel epostt epost.tail → Lean.Order.PartialOrder.rel (EPost.cons.mk✝ eposth epostt) epost

An EPost.cons value is below another if both components are below.

theorem Std.Do'.EPost.nil_rel (epost : EPost⟨⟩) : Lean.Order.PartialOrder.rel epost⟨⟩ epost

The unique EPost.nil value is below any EPost.nil value.

Notation

• EPost⟨e₁, e₂, ...⟩ builds an exception postcondition type (nested EPost.cons).
• epost⟨v₁, v₂, ...⟩ builds an exception postcondition value (nested EPost.cons.mk).

def Std.Do'.«termEPost⟨_⟩» : Lean.ParserDescr

Exception postcondition type notation: EPost⟨ε₁ → l, ε₂ → l⟩ for nested EPost.cons.

def Std.Do'.«termEpost⟨_⟩» : Lean.ParserDescr

Exception postcondition value notation: epost⟨h₁, h₂⟩ for nested EPost.cons.mk.

def Std.Do'.unexpandEPostNil : Lean.PrettyPrinter.Unexpander

Pretty-print EPost.nil as EPost⟨⟩.

def Std.Do'.unexpandEPostCons : Lean.PrettyPrinter.Unexpander

Pretty-print EPost.cons as EPost⟨e₁, e₂, ...⟩.

def Std.Do'.unexpandEPostNilMk : Lean.PrettyPrinter.Unexpander

Pretty-print EPost.nil.mk as epost⟨⟩.

def Std.Do'.unexpandEPostConsMk : Lean.PrettyPrinter.Unexpander

Pretty-print EPost.cons.mk as epost⟨v₁, v₂, ...⟩.