Sequential GraphSpec syntax #
This module defines the extensible primitive interface and the shape-indexed Chain language.
A chain records its ordered parameter ABI at the type level, and sequential composition
concatenates those parameter lists.
A primitive operation in the sequential GraphSpec language.
The pure specFwd interpretation and executable program share the same parameter, input, and
output shape indices. The optional layer conversion supports deterministic initialization and
conversion to Runtime.Autograd.Model.Layers.Seq.
- name : String
Short name used mainly for debugging and error messages.
- specFwd {α : Type} [TorchLean.Storage α] [Context α] : TorchLean.TensorPack α ps → TorchLean.Tensor α σ → TorchLean.Tensor α τ
Pure reference semantics of the primitive.
- program {α : Type} [TorchLean.Storage α] [Context α] : Runtime.Autograd.Model.Program α (ps ++ [σ]) τ
Executable TorchLean forward program, with parameters followed by the data input.
- toLayerM? : Option (ℕ → { l : Runtime.Autograd.Model.Layers.Layer σ τ // l.stateShapes = ps })
Optional conversion to a TorchLean layer, indexed by its occurrence in the surrounding chain.
- countsAsLayer : Bool
Whether this primitive advances the layer-occurrence counter.
Instances For
Chain ps σ τ is a sequential model from shape σ to shape τ whose parameters have shapes
ps, in order. Composition concatenates parameter ABIs; use NN.GraphSpec.DAG when explicit
sharing or multi-input nodes are required.
- id
(s : Spec.Shape)
: Chain [] s s
Identity chain: passes the input through unchanged and requires no parameters.
- seq
{ps₁ ps₂ : List Spec.Shape}
{σ τ υ : Spec.Shape}
: Chain ps₁ σ τ → Chain ps₂ τ υ → Chain (ps₁ ++ ps₂) σ υ
Sequential composition. Parameter lists concatenate.
- prim
{ps : List Spec.Shape}
{σ τ : Spec.Shape}
: Primitive ps σ τ → Chain ps σ τ
Embed a single primitive node in a chain.