src/vec.bend source

src/vec.bend on the hub · documented module

import Baseimport ./nat.bend as Nat# vec.bend: lists whose length is part of their type.##   import ./vec.bend as Vec## Vec(A, n) is computed from n: Unit at 0n, a pair of an A and a# Vec(A, p) at 1n+p. Matching on n tells the checker the vector's shape,# so zip_with has no length-mismatch case and get has no out-of-bounds# case: at n = 0n its bound Nat.LT(i, 0n) is Empty.## Indexing is O(i) and every element is a separate pair. For large numeric# data use Array.def Vec(-A: Data, n: Nat) -> Data:  match n:    case 0n:      Unit    case 1n+p:      Sigma<&2, &2, A, _ => Vec(A, p)># a list as a Vec of its own lengthdef from_list(-A: Data, xs: List<&2, A>) -> Vec(A, List.length(&2, A, xs)):  match xs:    case Nil{}:      Unit{}    case h <> t:      (h, from_list(A, t))def get(-A: Data, n: Nat, v: Vec(A, n), i: Nat, lt: Nat.LT(i, n)) -> A:  match n:    case 0n:      match lt:    case 1n+p:      (h, t) = v      match i:        case 0n:          h        case 1n+j:          get(A, p, t, j, lt)def zip_with(~A: Data, ~B: Data, ~C: Data, ~f: A -> B -> C, n: Nat, xs: Vec(A, n), ys: Vec(B, n)) -> Vec(C, n):  match n:    case 0n:      Unit{}    case 1n+p:      (x, xt) = xs      (y, yt) = ys      (f(x, y), zip_with(~A, ~B, ~C, ~f, p, xt, yt))def foldr(~A: Data, ~B: Data, ~f: A -> B -> B, n: Nat, v: Vec(A, n), z: B) -> B:  match n:    case 0n:      z    case 1n+p:      (h, t) = v      f(h, foldr(~A, ~B, ~f, p, t, z))