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

newtype 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.

OrderedMap

newtype OrderedMap(k, v, brand) = OrderedMap(Map(k, v, brand))

A map whose representation is sealed to the comparator carried by its witness. Hiding this wrapper matters as much as hiding OrdWitness: a raw Map(k, v, brand) can otherwise be instantiated at any phantom brand and smuggled into the explicit-ordering API after being built by another comparator.

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)

Named as the scoping form it is, since it reads at the call site as the block that opens the brand rather than as another operation on an ordered map.

ord_empty

ord_empty : forall a b c. (Data.Ordered.OrdWitness(a, b)) -> Data.Ordered.OrderedMap(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, Data.Ordered.OrderedMap(a, c, b)) -> Data.Ordered.OrderedMap(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))))

1

ord_lookup

ord_lookup : forall a b c. (Data.Ordered.OrdWitness(a, b), a, Data.Ordered.OrderedMap(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, Data.Ordered.OrderedMap(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), Data.Ordered.OrderedMap(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), Data.Ordered.OrderedMap(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)))))

2