Value domains with a null

SQL's NULL is a value of the domain like any other, and it is the same value in every possible world: it is not an unknown ranging over values. What sets it apart is how the operations treat it. Arithmetic is null-strict – a NULL operand makes the result NULL – and a comparison with a NULL operand is neither true nor false but unknown (Provenance.Util.Kleene).

Two equalities follow, as in SQL. Comparison equality is the three-valued one, CompOp.eval3 CompOp.eq, which is never true of a NULL. Syntactic equality is = on the domain, under which two NULLs are identical; it is what grouping, partitioning, duplicate elimination and difference use, and it is two-valued. The library already decides those four with DecidableEq, so they need nothing new: what this module adds is the null, the strictness it obeys, and the three-valued comparison.

ValueTypeNull extends ValueType rather than replacing it, so that the statements proved over a domain without a null stay true as stated, and WithNull T builds the canonical instance over any value type: a copy of T with one further value, where strictness holds by construction.

class ValueTypeNull (T : Type) extends ValueType T : Type

A value domain with a null: null-strict arithmetic, and a null distinct from the zero of the domain.

• zero : T
• add : T → T → T
• add_assoc (a b c : T) : a + b + c = a + (b + c)
• add_comm (a b : T) : a + b = b + a
• sub : T → T → T
• mul : T → T → T
• le : T → T → Prop
• lt : T → T → Prop
• le_refl (a : T) : a ≤ a
• le_trans (a b c : T) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : T) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : T) : a ≤ b → b ≤ a → a = b
• min : T → T → T
• max : T → T → T
• compare : T → T → Ordering
• le_total (a b : T) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE T
• toDecidableEq : DecidableEq T
• toDecidableLT : DecidableLT T
• min_def (a b : T) : min a b = if a ≤ b then a else b
• max_def (a b : T) : max a b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : T) : compare a b = compareOfLessAndEq a b
• isNull : T → Bool
• isNull_zero : isNull 0 = false
• nonzero : T
• nonzero_ne_zero : nonzero ≠ 0
• isNull_nonzero : isNull nonzero = false
• nullVal : Option T
• isNull_iff_nullVal (a : T) : isNull a = true ↔ nullVal = some a
• null : T

  The distinguished value.

• isNull_iff (a : T) : ValueType.isNull a = decide (a = null)

  The domain's null test is the test for that value.

• null_add (a : T) : null + a = null

  Addition is null-strict.

• null_sub (a : T) : null - a = null

  Subtraction is null-strict on the left.

• sub_null (a : T) : a - null = null

  Subtraction is null-strict on the right.

• null_mul (a : T) : null * a = null

  Multiplication is null-strict on the left.

• mul_null (a : T) : a * null = null

  Multiplication is null-strict on the right.

The three-valued comparison

def CompOp.eval3 {T : Type} [ValueType T] (op : CompOp) (a b : T) : Kleene

Three-valued evaluation of a comparison: unknown as soon as an operand is NULL, and the two-valued answer otherwise.

Equations

• op.eval3 a b = if op.strict = true ∧ (ValueType.isNull a = true ∨ ValueType.isNull b = true) then Kleene.unknown else Kleene.ofBool (decide (op.eval a b))

@[simp]

theorem CompOp.syneq_eval3_eq_true_iff {T : Type} [ValueType T] (a b : T) : syneq.eval3 a b = Kleene.true ↔ a = b

theorem CompOp.eval3_eq_true_iff {T : Type} [ValueType T] (op : CompOp) {a b : T} (ha : ValueType.isNull a = false) (hb : ValueType.isNull b = false) : op.eval3 a b = Kleene.true ↔ op.eval a b

Away from the null the three-valued reading is the two-valued one. This is what lets the statements proved under two-valued logic be recovered: they are the null-free case.

@[simp]

theorem CompOp.negate_eval3 {T : Type} [ValueType T] (op : CompOp) (a b : T) : op.negate.eval3 a b = (op.eval3 a b).not

The negator is the three-valued negation, and unconditionally so. Away from the null it is the Boolean complement; at the null both readings are unknown, and Kleene negation fixes unknown – so the equality holds there not because the negator complements anything but because there is nothing to complement. Pushing NOT through a comparison by PostgreSQL's operator negator is therefore sound as it stands.

The canonical null-bearing domain

Adjoining one value to a value type gives a ValueTypeNull, with strictness holding by construction: the operations are defined only where both operands are. This is the domain the examples use, and the one an implementation's nullable column has.

def WithNull (T : Type) : Type

A value type with one further value adjoined, the null.

Equations

• WithNull T = Option T

def WithNull.nil {T : Type} : WithNull T

The adjoined value.

Equations

• WithNull.nil = none

def WithNull.val {T : Type} (x : T) : WithNull T

A value of the domain, read in the adjoined domain.

Equations

• WithNull.val x = some x

@[instance_reducible]

instance WithNull.instDecidableEq {T : Type} [DecidableEq T] : DecidableEq (WithNull T)

Equations

• WithNull.instDecidableEq = WithNull.instDecidableEq._aux_1

@[instance_reducible]

instance WithNull.instLinearOrder {T : Type} [LinearOrder T] : LinearOrder (WithNull T)

The canonical order, with the null first. It orders group and frame sequences and has no ORDER BY meaning, so where the null falls in it is immaterial.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance WithNull.instZero {T : Type} [Zero T] : Zero (WithNull T)

Equations

• WithNull.instZero = { zero := WithNull.val 0 }

@[instance_reducible]

instance WithNull.instAdd {T : Type} [Add T] : Add (WithNull T)

Equations

• WithNull.instAdd = { add := fun (a b : WithNull T) => Option.map₂ (fun (x1 x2 : T) => x1 + x2) a b }

@[instance_reducible]

instance WithNull.instSub {T : Type} [Sub T] : Sub (WithNull T)

Equations

• WithNull.instSub = { sub := fun (a b : WithNull T) => Option.map₂ (fun (x1 x2 : T) => x1 - x2) a b }

@[instance_reducible]

instance WithNull.instMul {T : Type} [Mul T] : Mul (WithNull T)

Equations

• WithNull.instMul = { mul := fun (a b : WithNull T) => Option.map₂ (fun (x1 x2 : T) => x1 * x2) a b }

@[instance_reducible]

instance WithNull.instAddCommSemigroup {T : Type} [AddCommSemigroup T] : AddCommSemigroup (WithNull T)

Equations

• WithNull.instAddCommSemigroup = { toAdd := WithNull.instAdd, add_assoc := ⋯, add_comm := ⋯ }

@[instance_reducible]

instance WithNull.instValueType {T : Type} [ValueType T] : ValueType (WithNull T)

The adjoined value is the null, and nothing else is.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance WithNull.instValueTypeNullOfValueType {T : Type} [ValueType T] : ValueTypeNull (WithNull T)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance WithNull.instToString {T : Type} [ToString T] : ToString (WithNull T)

Equations

• WithNull.instToString = { toString := fun (a : WithNull T) => match a with | none => "NULL" | some x => toString x }

The rewriting domain reads its data arm as the data domain

The rewritten world lives in V ⊕ K, the data on the left and the annotation on the right. A term carried into it reads the same values on the data arm, which is what the lemmas below say of the comparison and of the null test.

Home · Documentation · Publications · Contributors · Source · Cite