src/class.bend source

src/class.bend on the hub · documented module

import Base# class.bend: operations bundled with their laws, passed as one template# argument.##   import ./class.bend as C#   Sorted.sort(~Nat, ~Nat.ord(), xs)## A generic def or law takes ~d: C.Ord<A> (or Semigroup, Group) and reads# it through the accessors below; a match on ~d inside generic code# cannot be typed. Instances live with their types (Nat.ord(),# U32.group()).# a total order: a relation and a decision that returns the side that holdstype Ord<-A: Data> is Type:  Ord{R: A -> A -> Type, dec: @x: A -> @y: A -> Or(R(x, y), R(y, x))}def Ord.R(-A: Data, d: Ord<A>, x: A, y: A) -> Type:  match d:    case Ord{R, dec}:      R(x, y)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)):  match d:    case Ord{R, dec}:      dec(x, y)# an associative operationtype Semigroup<-A: Data> is Type:  Semigroup{op: A -> A -> A, assoc: @x: A -> @y: A -> @z: A -> {op(x, op(y, z)) == op(op(x, y), z) : A}}def Semigroup.op(-A: Data, d: Semigroup<A>, x: A, y: A) -> A:  match d:    case Semigroup{op, assoc}:      op(x, y)# op as a template function, for Base's templates (List.foldr, List.foldl)def Semigroup.fn(~A: Data, ~d: Semigroup<A>, x: A, y: A) -> A:  Semigroup.op(A, d, x, y)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}:  match d:    case Semigroup{op, assoc}:      assoc(x, y, z)# addition and subtraction that undo each other (wrapping integers)type Group<-A: Data> is Type:  Group{add: A -> A -> A, sub: A -> A -> A,    sub_add: @a: A -> @b: A -> {a == sub(add(a, b), b) : A},    add_sub: @a: A -> @b: A -> {a == add(sub(a, b), b) : A}}def Group.add(-A: Data, d: Group<A>, a: A, b: A) -> A:  match d:    case Group{add, sub, sub_add, add_sub}:      add(a, b)def Group.sub(-A: Data, d: Group<A>, a: A, b: A) -> A:  match d:    case Group{add, sub, sub_add, add_sub}:      sub(a, b)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}:  match d:    case Group{add, sub, sub_add, add_sub}:      sub_add(a, b)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}:  match d:    case Group{add, sub, sub_add, add_sub}:      add_sub(a, b)