Data.Ordered

Explicit ordering witnesses: the branded, statically coherent path to ordered maps.

An unbranded Map(k, v) is ordered by the ambient canonical Ord(k). When a program needs two orderings of the same keys at once (one map ascending, one descending), the phantom brand on Map(k, v, brand) keeps their values from being mixed. with_ordering hands its body a witness carrying a comparator; the witness’s brand is a rigid, scope-local skolem, so a map built under one witness never unifies with a map built under another. Passing a map of one witness to another witness’s operation is a compile error that names both brands.

This is the explicit half of the ordered-container coherence story, closed statically. The implicit using ordRev path (calling the ambient map_insert under a non-canonical Ord) is guarded at runtime when an ordered map crosses a package boundary: Wire’s map reader faults when a map arrives ordered by a different Ord(k) than the reader canonicalizes. No claim is made here of automatic static closure of the implicit path.

Opt-in: this module is not in Base, so ambient effect rows and the unbranded Map surface are untouched unless a program imports it.

Types

`OrdWitness`

type OrdWitness(k, brand) = OrdBy((k, k) -> Int)

An ordering witness: a comparator branded by the phantom brand. The only way to obtain one is with_ordering, which mints a fresh brand per call, so two witnesses always carry incompatible brands.

Functions and Values

`with_ordering`

with_ordering : forall a b. ((a, a) -> Int, forall brand. (Data.Ordered.OrdWitness(a, brand)) -> b) -> b

Run body with a fresh ordering witness carrying cmp. The witness’s brand is rigid and unique to this call: a map built under it cannot be handed to a different witness’s operation, and that mismatch is a compile error naming both brands. The result a may not mention the brand, so a branded map never escapes the block, only a summary of it (a size, a looked-up value, an encoded form).

The brand binder is spelled brand rather than a bare letter on purpose: it must not collide with the a, b, c a scheme’s own quantifiers are canonicalized to, which would capture the result type under the inner quantifier.

with_ordering(\(a, b) -> cmp(a, b), \(w) ->
  ord_lookup(w, 1, ord_insert(w, 1, "a", ord_empty(w))))

Some(a)

`ord_empty`

ord_empty : forall a b c. (Data.Ordered.OrdWitness(a, b)) -> Map(a, c, b)

The empty map under witness w, carrying w’s brand.

`ord_insert`

ord_insert : forall a b c. (Data.Ordered.OrdWitness(a, b), a, c, Map(a, c, b)) -> Map(a, c, b)

Insert under witness w; the result carries w’s brand.

with_ordering(\(a, b) -> cmp(a, b), \(w) ->
  ord_size(w, ord_insert(w, 1, "a", ord_empty(w))))

`ord_lookup`

ord_lookup : forall a b c. (Data.Ordered.OrdWitness(a, b), a, Map(a, c, b)) -> Option(c)

Look key up under witness w. Only a map of w’s brand type-checks here.

with_ordering(\(a, b) -> cmp(a, b), \(w) ->
  ord_lookup(w, 9, ord_insert(w, 1, "a", ord_empty(w))))

None

`ord_member`

ord_member : forall a b c. (Data.Ordered.OrdWitness(a, b), a, Map(a, c, b)) -> Bool

True when key is present under witness w.

with_ordering(\(a, b) -> cmp(a, b), \(w) ->
  ord_member(w, 1, ord_insert(w, 1, "a", ord_empty(w))))

true

`ord_to_list`

ord_to_list : forall a b c. (Data.Ordered.OrdWitness(a, b), Map(a, c, b)) -> List((a, c))

The (key, value) pairs of a w-branded map, in tree (in-order) order.

with_ordering(\(a, b) -> cmp(a, b), \(w) ->
  ord_to_list(w, ord_insert(w, 2, "b", ord_insert(w, 1, "a", ord_empty(w)))))

[(1, a), (2, b)]

`ord_size`

ord_size : forall a b c. (Data.Ordered.OrdWitness(a, b), Map(a, c, b)) -> Int

The number of entries in a w-branded map.

with_ordering(\(a, b) -> cmp(a, b), \(w) ->
  ord_size(w, ord_insert(w, 2, "b", ord_insert(w, 1, "a", ord_empty(w)))))

Keyboard shortcuts

Prism