bend-ml-tensor

Releases (3):
  0.1.2.0  0x48e80e20946abebea50e06561806a40d  indexed  https://jend.leeeet.dev/files.txt?path=bend-ml-tensor@0.1.2.0
  0.1.1.0  0xdbe1000ee6707b4d38c0ad7eb1287363  unindexed  https://jend.leeeet.dev/files.txt?path=bend-ml-tensor@0.1.1.0
  0.1.0.0  0xf9837737d2c3f58ae1d0c5df42255584  unindexed  https://jend.leeeet.dev/files.txt?path=bend-ml-tensor@0.1.0.0

Definitions (78):
  BendMlTensor.Vec (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Vec)
   type Vec<-n: Nat> is Data:
     Vec{xs: List<&2, F32>}
  BendMlTensor.Mat (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Mat)
   type Mat<-r: Nat, -c: Nat> is Data:
     Mat{rows: List<&2, List<&2, F32>>}
  BendMlTensor.zip_with.add (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=zip_with.add)
   def zip_with.add(xs: List<&2, F32>, ys: List<&2, F32>) -> List<&2, F32>:
  BendMlTensor.zip_with.sub (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=zip_with.sub)
   def zip_with.sub(xs: List<&2, F32>, ys: List<&2, F32>) -> List<&2, F32>:
  BendMlTensor.zip_with.mul (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=zip_with.mul)
   def zip_with.mul(xs: List<&2, F32>, ys: List<&2, F32>) -> List<&2, F32>:
  BendMlTensor.scale.l (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=scale.l)
   def scale.l(+k: F32, xs: List<&2, F32>) -> List<&2, F32>:
  BendMlTensor.dot.go (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=dot.go)
   def dot.go(xs: List<&2, F32>, ys: List<&2, F32>, acc: F32) -> F32:
  BendMlTensor.sum.go (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=sum.go)
   def sum.go(xs: List<&2, F32>, acc: F32) -> F32:
  BendMlTensor.relu.l (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=relu.l)
   def relu.l(xs: List<&2, F32>) -> List<&2, F32>:
  BendMlTensor.fill.l (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=fill.l)
   def fill.l(n: Nat, +v: F32) -> List<&2, F32>:
  BendMlTensor.Vec.zeros (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Vec.zeros)
   def Vec.zeros(n: Nat) -> Vec<n>:
  BendMlTensor.Vec.fill (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Vec.fill)
   def Vec.fill(n: Nat, +v: F32) -> Vec<n>:
  BendMlTensor.Vec.add (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Vec.add)
   def Vec.add(-n: Nat, a: Vec<n>, b: Vec<n>) -> Vec<n>:
  BendMlTensor.Vec.sub (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Vec.sub)
   def Vec.sub(-n: Nat, a: Vec<n>, b: Vec<n>) -> Vec<n>:
  BendMlTensor.Vec.mul (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Vec.mul)
   def Vec.mul(-n: Nat, a: Vec<n>, b: Vec<n>) -> Vec<n>:
  BendMlTensor.Vec.scale (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Vec.scale)
   def Vec.scale(-n: Nat, +k: F32, a: Vec<n>) -> Vec<n>:
  BendMlTensor.Vec.dot (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Vec.dot)
   def Vec.dot(-n: Nat, a: Vec<n>, b: Vec<n>) -> F32:
  BendMlTensor.Vec.sum (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Vec.sum)
   def Vec.sum(-n: Nat, a: Vec<n>) -> F32:
  BendMlTensor.Vec.relu (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Vec.relu)
   def Vec.relu(-n: Nat, a: Vec<n>) -> Vec<n>:
  BendMlTensor.heads (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=heads)
   def heads(rows: List<&2, List<&2, F32>>) -> List<&2, F32>:
  BendMlTensor.tails (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=tails)
   def tails(rows: List<&2, List<&2, F32>>) -> List<&2, List<&2, F32>>:
  BendMlTensor.transpose.go (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=transpose.go)
   # transpose of a matrix with `c` columns (c is the one that shrinks, so it comes first)
   def transpose.go(c: Nat, +rows: List<&2, List<&2, F32>>) -> List<&2, List<&2, F32>>:
  BendMlTensor.rows.zip_add (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=rows.zip_add)
   def rows.zip_add(xs: List<&2, List<&2, F32>>, ys: List<&2, List<&2, F32>>) -> List<&2, List<&2, F32>>:
  BendMlTensor.rows.zip_sub (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=rows.zip_sub)
   def rows.zip_sub(xs: List<&2, List<&2, F32>>, ys: List<&2, List<&2, F32>>) -> List<&2, List<&2, F32>>:
  BendMlTensor.rows.zip_mul (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=rows.zip_mul)
   def rows.zip_mul(xs: List<&2, List<&2, F32>>, ys: List<&2, List<&2, F32>>) -> List<&2, List<&2, F32>>:
  BendMlTensor.rows.scale (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=rows.scale)
   def rows.scale(+k: F32, xs: List<&2, List<&2, F32>>) -> List<&2, List<&2, F32>>:
  BendMlTensor.rows.relu (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=rows.relu)
   def rows.relu(xs: List<&2, List<&2, F32>>) -> List<&2, List<&2, F32>>:
  BendMlTensor.rows.col_sums (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=rows.col_sums)
   # column sums
   def rows.col_sums(c: Nat, +rows: List<&2, List<&2, F32>>) -> List<&2, F32>:
  BendMlTensor.rows.add_row (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=rows.add_row)
   def rows.add_row(xs: List<&2, List<&2, F32>>, +b: List<&2, F32>) -> List<&2, List<&2, F32>>:
  BendMlTensor.matmul.row (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=matmul.row)
   def matmul.row(+ra: List<&2, F32>, bt: List<&2, List<&2, F32>>) -> List<&2, F32>:
  BendMlTensor.matmul.rows (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=matmul.rows)
   def matmul.rows(a: List<&2, List<&2, F32>>, +bt: List<&2, List<&2, F32>>) -> List<&2, List<&2, F32>>:
  BendMlTensor.flatten.l (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=flatten.l)
   # joins all the rows into a single list
   def flatten.l(rows: List<&2, List<&2, F32>>) -> List<&2, F32>:
  BendMlTensor.chunk.l (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=chunk.l)
   # splits a list into r rows of c numbers
   def chunk.l(r: Nat, +c: Nat, +xs: List<&2, F32>) -> List<&2, List<&2, F32>>:
  BendMlTensor.Mat.zeros (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Mat.zeros)
   def Mat.zeros(+r: Nat, +c: Nat) -> Mat<r, c>:
  BendMlTensor.Mat.fill (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Mat.fill)
   def Mat.fill(+r: Nat, +c: Nat, +v: F32) -> Mat<r, c>:
  BendMlTensor.Mat.add (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Mat.add)
   def Mat.add(-r: Nat, -c: Nat, a: Mat<r, c>, b: Mat<r, c>) -> Mat<r, c>:
  BendMlTensor.Mat.sub (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Mat.sub)
   def Mat.sub(-r: Nat, -c: Nat, a: Mat<r, c>, b: Mat<r, c>) -> Mat<r, c>:
  BendMlTensor.Mat.mul (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Mat.mul)
   # element-wise product (Hadamard)
   def Mat.mul(-r: Nat, -c: Nat, a: Mat<r, c>, b: Mat<r, c>) -> Mat<r, c>:
  BendMlTensor.Mat.scale (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Mat.scale)
   def Mat.scale(-r: Nat, -c: Nat, +k: F32, a: Mat<r, c>) -> Mat<r, c>:
  BendMlTensor.Mat.relu (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Mat.relu)
   def Mat.relu(-r: Nat, -c: Nat, a: Mat<r, c>) -> Mat<r, c>:
  BendMlTensor.Mat.transpose (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Mat.transpose)
   def Mat.transpose(-r: Nat, +c: Nat, a: Mat<r, c>) -> Mat<c, r>:
  BendMlTensor.Mat.matmul (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Mat.matmul)
   # (n x k) · (k x m) = (n x m): the inner dimensions must be the same k
   def Mat.matmul(-n: Nat, +k: Nat, +m: Nat, a: Mat<n, k>, b: Mat<k, m>) -> Mat<n, m>:
  BendMlTensor.Mat.matmul_t (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Mat.matmul_t)
   # (n x k) · (m x k)ᵀ = (n x m): the second operand arrives already TRANSPOSED (stored as
   # m rows of k numbers). It avoids transposing large weights on every call; the type
   # still requires the same inner dimension k.
   def Mat.matmul_t(-n: Nat, -k: Nat, -m: Nat, a: Mat<n, k>, bt: Mat<m, k>) -> Mat<n, m>:
  BendMlTensor.Mat.add_row (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Mat.add_row)
   # adds a bias (a vector of m numbers) to each row of an n x m matrix
   def Mat.add_row(-n: Nat, -m: Nat, a: Mat<n, m>, b: Vec<m>) -> Mat<n, m>:
  BendMlTensor.Mat.col_sums (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Mat.col_sums)
   # sum of each column: Mat<n, m> -> Vec<m>
   def Mat.col_sums(-n: Nat, +m: Nat, a: Mat<n, m>) -> Vec<m>:
  BendMlTensor.Mat.matvec (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Mat.matvec)
   # matrix · vector: (n x k) · k = n
   def Mat.matvec(-n: Nat, +k: Nat, a: Mat<n, k>, v: Vec<k>) -> Vec<n>:
  BendMlTensor.Mat.reshape (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Mat.reshape)
   # Reshape: compiles only with the PROOF that the number of elements does not change.
   def Mat.reshape(-r1: Nat, -c1: Nat, r2: Nat, +c2: Nat, -p: {Nat.mul(r1, c1) == Nat.mul(r2, c2) : Nat}, a: Mat<r1, c1>) -> Mat<r2, c2>:
  BendMlTensor.max.go (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=max.go)
   def max.go(xs: List<&2, F32>, cur: F32) -> F32:
  BendMlTensor.max.l (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=max.l)
   def max.l(xs: List<&2, F32>) -> F32:
  BendMlTensor.exp_shift (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=exp_shift)
   def exp_shift(xs: List<&2, F32>, +m: F32) -> List<&2, F32>:
  BendMlTensor.div.l (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=div.l)
   def div.l(xs: List<&2, F32>, +s: F32) -> List<&2, F32>:
  BendMlTensor.softmax.fin (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=softmax.fin)
   # stable softmax: subtracts the maximum before exponentiating
   def softmax.fin(+es: List<&2, F32>) -> List<&2, F32>:
  BendMlTensor.softmax.l (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=softmax.l)
   def softmax.l(+xs: List<&2, F32>) -> List<&2, F32>:
  BendMlTensor.rows.softmax (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=rows.softmax)
   def rows.softmax(xs: List<&2, List<&2, F32>>) -> List<&2, List<&2, F32>>:
  BendMlTensor.gelu.f (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=gelu.f)
   # GELU with the tanh approximation (the same as GPT-2)
   def gelu.f(+x: F32) -> F32:
  BendMlTensor.gelu.l (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=gelu.l)
   def gelu.l(xs: List<&2, F32>) -> List<&2, F32>:
  BendMlTensor.rows.gelu (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=rows.gelu)
   def rows.gelu(xs: List<&2, List<&2, F32>>) -> List<&2, List<&2, F32>>:
  BendMlTensor.sub_const (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=sub_const)
   def sub_const(xs: List<&2, F32>, +k: F32) -> List<&2, F32>:
  BendMlTensor.sq_sum (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=sq_sum)
   def sq_sum(xs: List<&2, F32>, acc: F32) -> F32:
  BendMlTensor.layernorm.fin (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=layernorm.fin)
   # (x - mean) / sqrt(variance + eps), then * gamma + beta
   def layernorm.fin(+cs: List<&2, F32>, +d: F32, +eps: F32, +gamma: List<&2, F32>, +beta: List<&2, F32>) -> List<&2, F32>:
  BendMlTensor.layernorm.l (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=layernorm.l)
   def layernorm.l(+xs: List<&2, F32>, +d: F32, +eps: F32, +gamma: List<&2, F32>, +beta: List<&2, F32>) -> List<&2, F32>:
  BendMlTensor.rows.layernorm (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=rows.layernorm)
   def rows.layernorm(xs: List<&2, List<&2, F32>>, +d: F32, +eps: F32, +gamma: List<&2, F32>, +beta: List<&2, F32>) -> List<&2, List<&2, F32>>:
  BendMlTensor.Mat.softmax (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Mat.softmax)
   def Mat.softmax(-r: Nat, -c: Nat, a: Mat<r, c>) -> Mat<r, c>:
  BendMlTensor.Mat.gelu (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Mat.gelu)
   def Mat.gelu(-r: Nat, -c: Nat, a: Mat<r, c>) -> Mat<r, c>:
  BendMlTensor.Mat.layernorm (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Mat.layernorm)
   # normalizes each row (d columns) and applies gamma and beta, vectors of d numbers
   def Mat.layernorm(-n: Nat, d: Nat, eps: F32, g: Vec<d>, bt: Vec<d>, a: Mat<n, d>) -> Mat<n, d>:
  BendMlTensor.Vec.softmax (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Vec.softmax)
   def Vec.softmax(-n: Nat, a: Vec<n>) -> Vec<n>:
  BendMlTensor.len.eq (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=len.eq)
   def len.eq(xs: List<&2, F32>, n: Nat) -> Bool:
  BendMlTensor.rows.ok (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=rows.ok)
   def rows.ok(rs: List<&2, List<&2, F32>>, +c: Nat, r: Nat) -> Bool:
  BendMlTensor.Vec.of2 (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Vec.of2)
   def Vec.of2(-n: Nat, ok: Bool, xs: List<&2, F32>) -> Maybe<&2, Vec<n>>:
  BendMlTensor.Vec.of (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Vec.of)
   # Vec<n> from a list, only if it has exactly n numbers
   def Vec.of(n: Nat, +xs: List<&2, F32>) -> Maybe<&2, Vec<n>>:
  BendMlTensor.Mat.of2 (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Mat.of2)
   def Mat.of2(-r: Nat, -c: Nat, ok: Bool, rs: List<&2, List<&2, F32>>) -> Maybe<&2, Mat<r, c>>:
  BendMlTensor.Mat.of (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Mat.of)
   # Mat<r, c> from rows, only if they are exactly r rows of c numbers
   def Mat.of(+r: Nat, +c: Nat, +rs: List<&2, List<&2, F32>>) -> Maybe<&2, Mat<r, c>>:
  BendMlTensor.Vec.to_list (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Vec.to_list)
   def Vec.to_list(-n: Nat, a: Vec<n>) -> List<&2, F32>:
  BendMlTensor.Mat.to_rows (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Mat.to_rows)
   def Mat.to_rows(-r: Nat, -c: Nat, a: Mat<r, c>) -> List<&2, List<&2, F32>>:
  BendMlTensor.reshape_swap (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=reshape_swap)
   # LAW (reshape_swap): r x c and c x r have the same number of elements
   # (multiplication is commutative), so this reshape always exists.
   law reshape_swap:
     for +r: Nat
     for +c: Nat
     {Nat.mul(r, c) == Nat.mul(c, r) : Nat}
  BendMlTensor.reshape_flat (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=reshape_flat)
   # LAW (reshape_flat): r x c has the same number of elements as 1 x (r*c)
   # (multiplying by 1 changes nothing), so flattening a matrix always exists.
   law reshape_flat:
     for +r: Nat
     for +c: Nat
     {Nat.mul(r, c) == Nat.mul(1n, Nat.mul(r, c)) : Nat}
  BendMlTensor.Mat.flatten (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Mat.flatten)
   # Mat<r, c> -> Mat<1, r*c>: the proof comes from the law above
   def Mat.flatten(+r: Nat, +c: Nat, a: Mat<r, c>) -> Mat<1n, Nat.mul(r, c)>:
  BendMlTensor.Mat.reshape_swap (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Mat.reshape_swap)
   # Mat<r, c> -> Mat<c, r> over the same data (it is NOT the transpose!): it only reinterprets
   def Mat.reshape_swap(+r: Nat, +c: Nat, a: Mat<r, c>) -> Mat<c, r>: