1	import 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
15	type Ord<-A: Data> is Type:
16	  Ord{R: A -> A -> Type, dec: @x: A -> @y: A -> Or(R(x, y), R(y, x))}
17	
18	def 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	
23	def 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
29	type 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	
32	def 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)
38	def Semigroup.fn(~A: Data, ~d: Semigroup<A>, x: A, y: A) -> A:
39	  Semigroup.op(A, d, x, y)
40	
41	def 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)
47	type 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	
52	def 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	
57	def 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	
62	def 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	
67	def 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)