Numerics and SystemsDimension Safety
Blorp by Example

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

Where

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