tur/vec-existential
Vec[A] as a size-hiding existential for heterogeneous collections.
Phase EX2-4: wraps Vec[A] in an existential to hide the element type.
Since: Phase EX2
vec-of-sized
(vec-of-sized [sv])
wrap a SizedVec into a Vec, hiding the size index.
Implements the pack half of the SizedVec <-> Vec round-trip. At runtime this is a plain pack -- the SizedVec payload is reboxed as an opaque existential carrying no constraint witnesses.
| sv | a SizedVec value whose size index will be sealed |
A value of type (exists [n] (SizedVec n int)) -- representable uniformly regardless of the original size index.
(vec-of-sized (SVCons 1 (SVCons 2 (SVNil)))) ; => packed Vec; opening it recovers a length-2 SizedVec.
Since: Phase EX2-4
open-vec
(open-vec [vec-expr n-name sv-name & body])
bind the hidden size index and the underlying SizedVec.
Expands to a native open whose binder vector is [n-name sv-name]. The first symbol becomes the phantom binder for the size index (used only by the type-checker -- no runtime presence); the second binds the underlying SizedVec value for use in the body.
The EX1d/EX2-3 escape checks still apply: the body's tail must not return sv-name (or an alias) and must not surface a type carrying the phantom binder.
| vec-expr | a Vec value (typically produced by vec-of-sized) | |
| n-name | symbol that names the fresh abstract size index | |
| sv-name | symbol that names the underlying SizedVec | |
| body | one or more body forms evaluated in the binders' scope |
The value of the last body form.
(open-vec (vec-of-sized (SVCons 1 (SVNil))) n sv (sized-vec-len sv)) ; => 1
Since: Phase EX2-4