src/vec.bend

bend-lawful-stdlib@0.1.0.0 · 58 lines · 5 definitions

1import Base
2import bend-lawful-stdlib@0.1.0.0/src/nat.bend as Nat
3
4# vec.bend: lists whose length is part of their type.
5#
6#   import ./vec.bend as Vec
7#
8# Vec(A, n) is computed from n: Unit at 0n, a pair of an A and a
9# Vec(A, p) at 1n+p. Matching on n tells the checker the vector's shape,
10# so zip_with has no length-mismatch case and get has no out-of-bounds
11# case: at n = 0n its bound Nat.LT(i, 0n) is Empty.
12#
13# Indexing is O(i) and every element is a separate pair. For large numeric
14# data use Array.
15
16def Vec(-A: Data, n: Nat) -> Data:
17  match n:
18    case 0n:
19      Unit
20    case 1n+p:
21      Sigma<&2, &2, A, _ => Vec(A, p)>
22
23# a list as a Vec of its own length
24def from_list(-A: Data, xs: List<&2, A>) -> Vec(A, List.length(&2, A, xs)):
25  match xs:
26    case Nil{}:
27      Unit{}
28    case h <> t:
29      (h, from_list(A, t))
30
31def get(-A: Data, n: Nat, v: Vec(A, n), i: Nat, lt: Nat.LT(i, n)) -> A:
32  match n:
33    case 0n:
34      match lt:
35    case 1n+p:
36      (h, t) = v
37      match i:
38        case 0n:
39          h
40        case 1n+j:
41          get(A, p, t, j, lt)
42
43def 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):
44  match n:
45    case 0n:
46      Unit{}
47    case 1n+p:
48      (x, xt) = xs
49      (y, yt) = ys
50      (f(x, y), zip_with(~A, ~B, ~C, ~f, p, xt, yt))
51
52def foldr(~A: Data, ~B: Data, ~f: A -> B -> B, n: Nat, v: Vec(A, n), z: B) -> B:
53  match n:
54    case 0n:
55      z
56    case 1n+p:
57      (h, t) = v
58      f(h, foldr(~A, ~B, ~f, p, t, z))