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.
pure func len[#N](v: Float[#N]) -> Int:
length(v)
-- len({1.0, 2.0, 3.0}) == 3
Dimension-Preserving Functions
When the same #N appears in parameters and returns, the concrete length flows through the call.
pure func scale[#N](v: Float[#N]) -> Float[#N]:
v * 2.0
-- scale({1.0, 2.0, 3.0}) == {2.0, 4.0, 6.0}
Where
where constraints relate computed dimensions when one dimension must equal another.
pure func accepts_total[#M, #N, #R](
a: Int[#M],
b: Int[#N],
out: Int[#R],
) -> Int where #M + #N == #R:
length(out)
-- accepts_total({1, 2}, {3}, {0, 0, 0}) == 3
assert_shape
assert_shape refines a variadic-dimension array to a concrete dimension when the runtime shape matches.
data: Float[#3] = {1.0, 2.0, 3.0}
match assert_shape(data, 3):
-- v[0] == 1.0 when data has length 3
Some(v): v[0]
None: 0.0
Example
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