tur/refined
refinement newtypes for total collection accessors.
Replaces partial functions over lists and vectors with total versions guarded by refinement newtypes:
NonEmpty -- a list proven to hold at least one element; ne-head /
ne-tail are total (no empty-list panic).
BoundedIdx -- an index proven to fall within a collection's length;
vec-get-checked / slice-get-checked are total (no
out-of-bounds panic).
The proof obligation is discharged by smart constructors (ne-from?, bidx-of?) that return Option: the caller pattern-matches on the Option once and then holds a value whose accessors can never fail. The existing partial accessors (list-head, vec-get, slice-get) stay callable -- this module is purely additive.
Both newtypes lower to :int in the C ABI (defopaque over :int), so they compose with the int-carrier Option and list/vec/slice helpers at zero runtime cost. NonEmpty now carries a phantom element type A in its type spelling -- (NonEmpty A) -- via parameterized defopaque, so ne-head / ne-of are typed in terms of the element type instead of a bare :int. BoundedIdx stays a bare carrier (its length n is a value-level fact the smart constructor checks, not a type the checker can track). See docs/archive/history/parameterized-defopaque.md.
Since: stdlib-refinement-collections-plan (R1, R2)
NonEmpty
(defopaque NonEmpty [A] :int)
a cons list of element type A, proven to contain at least one element.
Lowers to :int (the head cons-cell pointer, never 0); the type parameter A is a phantom that tracks the element type so ne-head returns A rather than a bare :int. Construct it with ne-of / ne-singleton (always non-empty by construction) or recover it from an arbitrary list with the ne-from? smart constructor.
Since: R1
ne-of
(ne-of [A])
build a NonEmpty by prepending a head to an existing list.
| x | the head element (carrier :int) | |
| xs | the rest of the list (a cons list; may be empty / tnil) |
A NonEmpty whose head is x and whose tail is xs.
(ne-head (ne-of 7 (tnil))) ; => 7
Since: R1
ne-singleton
(ne-singleton [A])
build a one-element NonEmpty.
| x | the sole element (carrier :int) |
A NonEmpty containing exactly x.
(ne-head (ne-singleton 42)) ; => 42
Since: R1
ne-head
(ne-head [A])
the first element of a NonEmpty (total).
Unlike list-head, this never panics: a NonEmpty is non-empty by construction, so the head always exists.
| ne | the NonEmpty to inspect |
The first element (carrier :int).
(ne-head (ne-of 1 (tcons 2 (tnil)))) ; => 1
Since: R1
ne-tail
(ne-tail [A])
the elements after the head, as an ordinary (possibly empty) list.
| ne | the NonEmpty to inspect |
The tail as a cons list (tnil when ne has a single element).
(list-head (ne-tail (ne-of 1 (tcons 2 (tnil))))) ; => 2
Since: R1
ne->list
(ne->list [A])
view a NonEmpty as an ordinary cons list.
| ne | the NonEmpty to convert |
The underlying cons list (never empty).
(list-head (ne->list (ne-singleton 5))) ; => 5
Since: R1
ne-len
(ne-len [A])
the number of elements in a NonEmpty (always >= 1).
| ne | the NonEmpty to measure |
The element count as an :int.
(ne-len (ne-of 1 (tcons 2 (tnil)))) ; => 2
Since: R1
ne-from?
(ne-from? [A])
smart constructor: recover a NonEmpty from an arbitrary list.
This is the proof obligation: match the resulting Option once, and the some-branch holds a NonEmpty whose ne-head / ne-tail are total.
| xs | an arbitrary typed list (may be empty) |
(some ne) when xs is non-empty, (none) when xs is empty. The payload is a (NonEmpty A) whose element type A is recovered from the (List A) arg; recover it with ne-unwrap.
(some? (ne-from? (list-of 1))) ; => true (some? (ne-from? (list-of))) ; => false
Since: R1
ne-unwrap
(ne-unwrap [A])
recover the NonEmpty payload from a non-none Option.
Pair with ne-from? after a some? check; on a none Option this yields a NonEmpty over 0, so guard with some? first.
| o | a (Option (NonEmpty A)) as returned by ne-from? |
The wrapped (NonEmpty A).
(let [o (ne-from? (list-of 9))] (if (some? o) (ne-head (ne-unwrap o)) -1)) ; => 9
Since: R1
BoundedIdx
(defopaque BoundedIdx :int)
an index proven to satisfy 0 <= i < n for some length n.
Lowers to :int. Construct it only through bidx-of?, which checks the index against a length; the resulting BoundedIdx can then drive a total accessor (vec-get-checked / slice-get-checked) without a second bounds check. (The length n is tracked at the value level by the smart constructor rather than in the type, pending parameterized defopaque.)
Since: R2
bidx->int
(bidx->int [b :BoundedIdx] :int)
recover the raw :int index from a BoundedIdx.
| b | the BoundedIdx to unwrap |
The underlying index as a plain :int.
(bidx->int (bidx-unwrap (bidx-of? 5 3))) ; => 3
Since: R2
bidx-of?
(bidx-of? [n :int i :int] :(Option BoundedIdx))
smart constructor: prove an index lies within [0, n).
| n | the exclusive upper bound (e.g. a collection's length) | |
| i | the candidate index |
(some b) when 0 <= i < n, (none) otherwise. Recover the BoundedIdx payload with bidx-unwrap.
(some? (bidx-of? 5 3)) ; => true (some? (bidx-of? 5 9)) ; => false
Since: R2
bidx-unwrap
(bidx-unwrap [o :(Option BoundedIdx)] :BoundedIdx)
recover the BoundedIdx payload from a non-none Option.
Pair with bidx-of? after a some? check.
| o | a (Option BoundedIdx) as returned by bidx-of? |
The wrapped BoundedIdx.
(let [o (bidx-of? 4 2)] (if (some? o) (bidx->int (bidx-unwrap o)) -1)) ; => 2
Since: R2
vec-get-checked
(vec-get-checked [A])
index a Vec with a proven-in-range BoundedIdx (total).
Because the BoundedIdx was validated against the vector's length by bidx-of?, this access never reaches vec-get's out-of-bounds path.
| v | the Vec[A] pointer to read | |
| b | a BoundedIdx proven against (vec-len v) |
The element at the index (carrier :int).
(let [o (bidx-of? (vec-len v) 1)] (if (some? o) (vec-get-checked v (bidx-unwrap o)) -1))
Since: R2
slice-get-checked
(slice-get-checked [s :int b :BoundedIdx] :int)
index a Slice with a proven-in-range BoundedIdx (total).
| s | the Slice pointer to read | |
| b | a BoundedIdx proven against (slice-len s) |
The element at the index (carrier :int).
(let [o (bidx-of? (slice-len s) 0)] (if (some? o) (slice-get-checked s (bidx-unwrap o)) -1))
Since: R2
Internal definitions
__ne-len-acc-- tail-recursive length accumulator over a cons list.