Recurrent Stacks with Independent Widths #
Adjacent cell dimensions agree by construction. The empty stack preserves the input width, and its state is empty. A nonempty stack carries one state of the appropriate width per layer.
A sequence of recurrent cells with independently chosen intermediate widths.
- nil
{Cell : ℕ → ℕ → Type}
{width : ℕ}
: RecurrentStack Cell width width
No recurrent layers.
- cons
{Cell : ℕ → ℕ → Type}
{inputWidth hiddenWidth outputWidth : ℕ}
(cell : Cell inputWidth hiddenWidth)
(rest : RecurrentStack Cell hiddenWidth outputWidth)
: RecurrentStack Cell inputWidth outputWidth
One cell followed by a stack consuming its hidden stream.
Instances For
def
Spec.RecurrentStack.States
{Cell : ℕ → ℕ → Type}
{inputWidth outputWidth : ℕ}
(layers : RecurrentStack Cell inputWidth outputWidth)
(State : ℕ → Type)
:
One state per layer, with no states for an empty stack.
Instances For
def
Spec.RecurrentStack.run
{α : Type}
[TorchLean.Storage α]
{Cell : ℕ → ℕ → Type}
{State : ℕ → Type}
{sequenceLength inputWidth outputWidth : ℕ}
(layers : RecurrentStack Cell inputWidth outputWidth)
(runCell :
{input hidden : ℕ} →
Cell input hidden →
TorchLean.Tensor α [sequenceLength, input] →
State hidden → TorchLean.Tensor α [sequenceLength, hidden] × State hidden)
(inputs : TorchLean.Tensor α [sequenceLength, inputWidth])
(states : layers.States State)
:
Run each cell on the preceding layer's entire sequence and retain every final state.
Instances For
def
Spec.RecurrentStack.toChain
{α : Type}
[TorchLean.Storage α]
{Cell : ℕ → ℕ → Type}
{sequenceLength inputWidth hiddenWidth outputWidth : ℕ}
(layers : RecurrentStack Cell inputWidth hiddenWidth)
(toModule : {input hidden : ℕ} → Cell input hidden → Module α [sequenceLength, input] [sequenceLength, hidden])
(head : Module α [sequenceLength, hiddenWidth] [sequenceLength, outputWidth])
:
Compose the recurrent modules and a head, including a head with no recurrent layers.