Dimension Safety
Dimension parameters let reusable numeric code state shape requirements in the type.
#n
A # name is a dimension parameter, not a runtime integer.
dim.brp
pure func len[#N](v: Float[#N]) -> Int:
length(v)Dimension-preserving Functions
When the same #N appears in parameters and returns, the concrete length flows through the call.
preserve.brp
pure func scale[#N](v: Float[#N]) -> Float[#N]:
v * 2.0Where
where constraints relate computed dimensions when one dimension must equal another.
where.brp
pure func accepts_total[#M, #N, #R](a: Int[#M], b: Int[#N], out: Int[#R]) -> Int where #M + #N == #R:
length(out)Assert_shape
assert_shape refines a variadic-dimension array to a concrete dimension when the runtime shape matches.
assert-shape.brp
match assert_shape(data, 3):
Some(v): v[0]
None: 0.0Example
dimension-dot.brp
import:
vector: dot
pure func same_length_dot[#N](a: Float[#N], b: Float[#N]) -> Float:
dot(a, b)
pure func total_after_refine(data: Float[#Ds...]) -> Option[Float]:
values ?= assert_shape(data, 3)
Some(same_length_dot(values, {1.0, 1.0, 1.0}))
pure func keep_total_shape[T, #M, #N, #R](
a: T[#M],
b: T[#N],
out: T[#R],
) -> T[#R] where #M + #N == #R:
out
Try It
terminal
blorp check dimension-dot.brp