Tensor Conversion #
Total in-memory conversion belongs here. Sources carry their intrinsic shape:
ordinary arrays and lists become vectors, while future structured sources may
provide richer shapes through Tensor.From.
Changing only the interpretation of a flat row-major buffer is Tensor.reshape
and requires a proof that the scalar count is unchanged. Validation of external
files and untrusted runtime metadata belongs in the corresponding loader.
Intrinsic tensor shape described by an in-memory source value.
- shape : source → Spec.Shape
Shape intrinsically described by the source value.
Instances
Extensible, total materialization of a shaped in-memory source.
- make (value : source) : Tensor α (SourceShape.shape value)
Construct the tensor without a runtime failure branch.
Instances
Convert an in-memory value into a tensor with its intrinsic shape.
Instances For
An Array describes one dimension, its length.
The shape is computed from the value rather than declared by the caller, which is what lets
Tensor.from be written without a shape annotation.
The shape an Array describes is its length.
The shape a List describes is its length.
Materialize a List as a rank-one tensor, copying once through List.toArray.
A Vector α n carries its length in its type, so the shape is known without inspecting the
value at all.
The shape a Vector α n describes is [n], independently of the value.
A FloatArray describes one dimension, the length reported by its Storage instance.
A FloatArray is already the unboxed Float storage, so materialization is a rewrap.
A ByteArray describes one dimension, the length reported by its Storage instance.
Reinterpret the same contiguous row-major buffer at an equal-size shape.
The equality is the complete safety condition: reshape neither pads, truncates, nor moves scalar data.
Example:
-- Same buffer, new shape. The size equality is the entire safety condition, and it is checked
-- here rather than trusted.
def matrix (flat : Tensor Float [12]) : Tensor Float [3, 4] :=
Tensor.reshape flat [3, 4]
Instances For
Extensible conversion from a tensor to a requested in-memory target type.
- convert : Tensor α shape → target
Materialize or expose the requested target representation.
Instances
Convert a tensor to the requested target type.
Instances For
Read a tensor out as its row-major array.
Read a tensor out as its row-major list.
Read a tensor out as a length-indexed vector.
Expose the native buffer of a Float tensor.
Expose the native buffer of a byte tensor.
Converting to Array exposes the row-major observation, boxing packed storage if needed.
Converting to List is the array conversion followed by Array.toList.
Array in, array out: Tensor.from then Tensor.to is the identity.
The four round-trip lemmas that follow are the reason the conversion layer can be trusted at the boundary. Nothing in the tensor representation reorders or pads the data, so importing and exporting gives back exactly what was handed in.
A shape cast does not touch the data, so exporting before or after it gives the same array.
This is the statement that makes castShape free: it is a retyping, not a copy.
The list version of to_array_castShape.
Reshaping is likewise data-preserving: only the interpretation of the flat buffer changes.
Together with to_array_castShape this pins down the row-major convention. A reshape that permuted
elements would break this lemma, so it doubles as a regression test on the layout.
Converting a filled tensor to a list produces one value per scalar position.
A filled natural-number vector describes the corresponding uniform shape.