src/class.bend

bend-lawful-stdlib@0.1.0.0 · 70 lines · 12 definitions

1import Base
2
3# class.bend: operations bundled with their laws, passed as one template
4# argument.
5#
6#   import ./class.bend as C
7#   Sorted.sort(~Nat, ~Nat.ord(), xs)
8#
9# A generic def or law takes ~d: C.Ord<A> (or Semigroup, Group) and reads
10# it through the accessors below; a match on ~d inside generic code
11# cannot be typed. Instances live with their types (Nat.ord(),
12# U32.group()).
13
14# a total order: a relation and a decision that returns the side that holds
15type Ord<-A: Data> is Type:
16  Ord{R: A -> A -> Type, dec: @x: A -> @y: A -> Or(R(x, y), R(y, x))}
17
18def Ord.R(-A: Data, d: Ord<A>, x: A, y: A) -> Type:
19  match d:
20    case Ord{R, dec}:
21      R(x, y)
22
23def Ord.dec(-A: Data, d: Ord<A>, x: A, y: A) -> Or(Ord.R(A, d, x, y), Ord.R(A, d, y, x)):
24  match d:
25    case Ord{R, dec}:
26      dec(x, y)
27
28# an associative operation
29type Semigroup<-A: Data> is Type:
30  Semigroup{op: A -> A -> A, assoc: @x: A -> @y: A -> @z: A -> {op(x, op(y, z)) == op(op(x, y), z) : A}}
31
32def Semigroup.op(-A: Data, d: Semigroup<A>, x: A, y: A) -> A:
33  match d:
34    case Semigroup{op, assoc}:
35      op(x, y)
36
37# op as a template function, for Base's templates (List.foldr, List.foldl)
38def Semigroup.fn(~A: Data, ~d: Semigroup<A>, x: A, y: A) -> A:
39  Semigroup.op(A, d, x, y)
40
41def Semigroup.assoc(-A: Data, d: Semigroup<A>, x: A, y: A, z: A) -> {Semigroup.op(A, d, x, Semigroup.op(A, d, y, z)) == Semigroup.op(A, d, Semigroup.op(A, d, x, y), z) : A}:
42  match d:
43    case Semigroup{op, assoc}:
44      assoc(x, y, z)
45
46# addition and subtraction that undo each other (wrapping integers)
47type Group<-A: Data> is Type:
48  Group{add: A -> A -> A, sub: A -> A -> A,
49    sub_add: @a: A -> @b: A -> {a == sub(add(a, b), b) : A},
50    add_sub: @a: A -> @b: A -> {a == add(sub(a, b), b) : A}}
51
52def Group.add(-A: Data, d: Group<A>, a: A, b: A) -> A:
53  match d:
54    case Group{add, sub, sub_add, add_sub}:
55      add(a, b)
56
57def Group.sub(-A: Data, d: Group<A>, a: A, b: A) -> A:
58  match d:
59    case Group{add, sub, sub_add, add_sub}:
60      sub(a, b)
61
62def Group.sub_add(-A: Data, d: Group<A>, a: A, b: A) -> {a == Group.sub(A, d, Group.add(A, d, a, b), b) : A}:
63  match d:
64    case Group{add, sub, sub_add, add_sub}:
65      sub_add(a, b)
66
67def Group.add_sub(-A: Data, d: Group<A>, a: A, b: A) -> {a == Group.add(A, d, Group.sub(A, d, a, b), b) : A}:
68  match d:
69    case Group{add, sub, sub_add, add_sub}:
70      add_sub(a, b)