Order specifications: what a window's ORDER BY orders by

A window's ORDER BY does not order rows by the domain's own order. It names, for each order column, a direction and a null placement, and those two together give a total preorder on the order values: ASC or DESC on the values of the domain, NULLS FIRST or NULLS LAST on the nulls, which the domain's order knows nothing about. Order values that the preorder does not separate are SQL's peers.

This file gives the specification (OrderCol, OrderSpec) and proves that it is a total preorder (OrderSpec.le_trans, OrderSpec.le_total, and reflexivity as the diagonal of totality). Two things are defined from it, and both are things the domain's order cannot supply.

The first is the bound of a frame: RANGE BETWEEN UNBOUNDED PRECEDING AND CURRENT ROW is the peers of the current row and everything sorted before them, and which rows those are is a question about the clause. Those frames are built in Provenance.Frame, where ValueFrame is.

The second is the order a frame is read in, which is what an aggregate that is not symmetric depends on. OrderSpec.readLe is that order – the clause on the order values, its ties broken by the canonical order on the rows, so that two occurrences are tied exactly when they carry the same row – and OrderSpec.sortSeq puts a listing of a frame into it. It is what ValueFrame.frameSeqOn and hence the window operator read.

sortSeq_tiePerm is what makes that usable: any two listings of one frame come out related by a tie-block permutation whose blocks are the occurrences of one row, which is precisely the freedom every reading of a token is invariant under. map_eq_of_sorted is the working form – two readings of one frame give the same sequence of values – and filter_sortSeq_map_eq says cutting a frame down to a possible world and sorting commute on the values read off, which is what the random-world commutation needs.

A window with no ORDER BY has no order columns at all, OrderSpec.unordered; the clause then separates nothing (peer_of_zero) and the frame is read as a group is read (ValueFrame.frameListOf_of_peer).

One order column

structure OrderCol : Type

One column of an ORDER BY: which way the column reads, and where its nulls go.

• desc : Bool

  DESC: the domain's order on the non-null values, reversed.

• nullsFirst : Bool

  NULLS FIRST: every null sorts before every value of the domain.

@[instance_reducible]

instance instDecidableEqOrderCol : DecidableEq OrderCol

Equations

• instDecidableEqOrderCol = instDecidableEqOrderCol.decEq

def instDecidableEqOrderCol.decEq (x✝ x✝¹ : OrderCol) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqOrderCol.decEq { desc := a, nullsFirst := a_1 } { desc := b, nullsFirst := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance instReprOrderCol : Repr OrderCol

Equations

• instReprOrderCol = { reprPrec := instReprOrderCol.repr }

def instReprOrderCol.repr : OrderCol → ℕ → Std.Format

Equations

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

def OrderCol.ASC : OrderCol

ASC with SQL's default null placement: a null sorts after every value of the domain.

Equations

• OrderCol.ASC = { }

def OrderCol.DESC : OrderCol

DESC with SQL's default null placement: reversing the direction reverses where the nulls go too, so a null sorts before every value.

Equations

• OrderCol.DESC = { desc := true, nullsFirst := true }

def OrderCol.le {T : Type} [ValueType T] (c : OrderCol) (a b : T) : Bool

Whether a sorts no later than b in this column. The nulls are placed by the specification and compare equal to each other, which is SQL: two nulls are peers in an ORDER BY, however the clause places them.

Equations

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

def OrderCol.peer {T : Type} [ValueType T] (c : OrderCol) (a b : T) : Bool

Two values are peers in a column when neither sorts before the other.

Equations

• c.peer a b = (c.le a b && c.le b a)

def OrderCol.reverse (c : OrderCol) : OrderCol

The column read backwards. Reversing the direction reverses where the nulls go with it, as ASC/DESC do: the reverse of OrderCol.ASC is OrderCol.DESC.

Equations

• c.reverse = { desc := !c.desc, nullsFirst := !c.nullsFirst }

Where the nulls go

Where nothing is null

The clause

@[reducible, inline]

abbrev OrderSpec (p : ℕ) : Type

An ORDER BY clause over p order columns: a direction and a null placement for each.

Equations

• OrderSpec p = (Fin p → OrderCol)

def OrderSpec.asc (p : ℕ) : OrderSpec p

Every column ASC, with SQL's default null placement.

Equations

• OrderSpec.asc p x✝ = OrderCol.ASC

def OrderSpec.desc (p : ℕ) : OrderSpec p

Every column DESC, with SQL's default null placement.

Equations

• OrderSpec.desc p x✝ = OrderCol.DESC

def OrderSpec.unordered : OrderSpec 0

No ORDER BY: the clause with no order columns, which separates nothing, so a frame under it is read as a group is read.

Equations

• OrderSpec.unordered k = k.elim0

def OrderSpec.leOn {T : Type} {p : ℕ} [ValueType T] (o : OrderSpec p) : List (Fin p) → Tuple T p → Tuple T p → Bool

Lexicographic comparison down a list of columns: the first column whose values are not peers decides, and tuples that are peers in every column of the list compare as equal.

Equations

• o.leOn [] x✝¹ x✝ = true
• o.leOn (k :: ks) x✝¹ x✝ = if (o k).peer (x✝¹ k) (x✝ k) = true then o.leOn ks x✝¹ x✝ else (o k).le (x✝¹ k) (x✝ k)

def OrderSpec.le {T : Type} {p : ℕ} [ValueType T] (o : OrderSpec p) (x y : Tuple T p) : Bool

Whether x sorts no later than y under the clause: lexicographically, the columns read in the order the clause names them.

Equations

• o.le x y = o.leOn (List.finRange p) x y

def OrderSpec.peer {T : Type} {p : ℕ} [ValueType T] (o : OrderSpec p) (x y : Tuple T p) : Bool

Two order values are peers when neither sorts before the other. SQL's frames are defined against the peer group, not against the row: CURRENT ROW in a RANGE frame means the current row's peers.

Equations

• o.peer x y = (o.le x y && o.le y x)

def OrderSpec.lt {T : Type} {p : ℕ} [ValueType T] (o : OrderSpec p) (x y : Tuple T p) : Bool

x sorts strictly before y: y is not at or before x.

Equations

• o.lt x y = !o.le y x

def OrderSpec.reverse {p : ℕ} (o : OrderSpec p) : OrderSpec p

The clause read backwards, column by column: what last_value reads its frame in where first_value reads it forwards.

Equations

• o.reverse k = (o k).reverse

@[simp]

theorem OrderSpec.le_reverse {T : Type} {p : ℕ} [ValueType T] (o : OrderSpec p) (x y : Tuple T p) : o.reverse.le x y = o.le y x

The clause is a total preorder

@[simp]

theorem OrderSpec.le_rfl {T : Type} {p : ℕ} [ValueType T] (o : OrderSpec p) (x : Tuple T p) : o.le x x = true

theorem OrderSpec.le_total {T : Type} {p : ℕ} [ValueType T] (o : OrderSpec p) (x y : Tuple T p) : o.le x y = true ∨ o.le y x = true

theorem OrderSpec.le_trans {T : Type} {p : ℕ} [ValueType T] (o : OrderSpec p) {x y z : Tuple T p} (h₁ : o.le x y = true) (h₂ : o.le y z = true) : o.le x z = true

Where nothing is null

With every column ASC and no null to place, the clause is the domain's own lexicographic order on the order values, and the frames it determines are the ones stated against that order.

def Tuple.tail {T : Type} {p : ℕ} (x : Tuple T (p + 1)) : Tuple T p

The tuple without its first column.

Equations

• x.tail k = x k.succ

theorem OrderSpec.asc_le {T : Type} [ValueType T] [NoNulls T] {p : ℕ} (x y : Tuple T p) : (asc p).le x y = decide (x ≤ y)

Every column ASC, on a domain where nothing is null, is the domain's own order on tuples: the clause's lexicographic reading and the tuple order the library already has are the same order.

The order a frame is read in

An aggregate is a function on sequences, so a window has to say in which order its frame is read. SQL says: the clause's. Since the clause is a preorder it does not settle the peers, and the library breaks those ties by its own order on rows – a choice invisible to every symmetric aggregate (SeqAggFunc.Symmetric), and one that leaves two occurrences tied exactly when they carry the same row, which is what a tie-block permutation is allowed to exchange.

def OrderSpec.readLe {T : Type} {p : ℕ} [ValueType T] {α β : Type} [LinearOrder β] (key : β → Tuple T p) (val : α → β) (o : OrderSpec p) (x y : α) : Bool

The order a window reads its frame in: the clause on the order values a row carries, its ties broken by the canonical order on the rows themselves. val reads an occurrence's row, key the order values of a row.

Equations

• OrderSpec.readLe key val o x y = if o.peer (key (val x)) (key (val y)) = true then decide (val x ≤ val y) else o.le (key (val x)) (key (val y))

def OrderSpec.sortSeq {T : Type} {p : ℕ} [ValueType T] {α β : Type} [LinearOrder β] (key : β → Tuple T p) (val : α → β) (o : OrderSpec p) (L : List α) : List α

The occurrences of a frame, in the order the clause reads them.

Equations

• OrderSpec.sortSeq key val o L = List.insSort (fun (x y : α) => OrderSpec.readLe key val o x y = true) L

instance OrderSpec.total_readLe {T : Type} {p : ℕ} [ValueType T] {α β : Type} [LinearOrder β] {key : β → Tuple T p} {val : α → β} {o : OrderSpec p} : Std.Total fun (x y : α) => readLe key val o x y = true

The clause's reading is total and transitive, which is what sorting a sequence by it asks.

instance OrderSpec.isTrans_readLe {T : Type} {p : ℕ} [ValueType T] {α β : Type} [LinearOrder β] {key : β → Tuple T p} {val : α → β} {o : OrderSpec p} : IsTrans α fun (x y : α) => readLe key val o x y = true

theorem OrderSpec.map_eq_of_sorted {T : Type} {p : ℕ} [ValueType T] {α β : Type} [LinearOrder β] {key : β → Tuple T p} {val : α → β} {o : OrderSpec p} [DecidableEq α] {γ : Type} (g : β → γ) {L L' : List α} (h : L.Perm L') (hL : List.Pairwise (fun (x y : α) => readLe key val o x y = true) L) (hL' : List.Pairwise (fun (x y : α) => readLe key val o x y = true) L') : List.map (fun (x : α) => g (val x)) L = List.map (fun (x : α) => g (val x)) L'

Any two readings of one frame in the clause's order give the same sequence of values. They differ only inside blocks of occurrences carrying equal rows, and equal rows give equal values.

Home · Documentation · Publications · Contributors · Source · Cite