Relational: trait 

% Taken from:
%
% A Relational Model of Data for Large Shared Data Banks
% E. F. Codd
%
% Reprinted from Communications of the ACM, Vol. 13, No. 6, June 1970, pp.
% 377-387. Copyright (c) 1970, Association for Computing Machinery, Inc.
% http://www.acm.org/classics/nov95/toc.html

% Notions yet to be captured:
%   primary key
%   nonredundant
%   foreign key
% named, expressible, and stored

% permutation

includes
  FiniteSet(Relation, Tuple)
  List(Tuple, Value)
  Set(Domain, Value)

% 
  Table tuple of schema: Schema, relation: Relation
  List(Schema, ColDesc)
  ColDesc tuple of label: Label, domain: Domain

%
  List(LabelList, Label)

%  Function(Schema, Identifier, Domain)
%  Relationship tuple of schema: Schema, rows: Rows


  Set(Query, Row)


introduces:
  empty: Schema -> Table

  check: Schema, Row -> Bool

  insert: Table, Row -> Table
  project: Table, FieldList -> Table
  select: Table, Query -> Table
  join: Table, Label, Table, Label -> Table

asserts:

% Permutation
% Projection

  project(t,[]).schema = []
  @@ subseq of schema w/matching names

% Join

  join(t1, t2, n1, n2).schema = @@append(t1.schema, t2.schema)
  r \in join(t1, t2).rows = head(r, length(t1.schema)) \in t1.rows /\ tail(r, length(t2.schema)) \in t2.rows

  r \in project(t, []) = (r = [])
  subseq(s, t.schema, map) -> (
    r \in project(t,s).rows = rr \in t.rows /\ subseq(r, rr, map) )


  empty(s).schema = s
  empty(s).rows = {}

  check([], []) = True
  check(s, r) = r[0] \in s[0].type /\ check(rest(s), rest(r))

  check(t.schema, r) -> insert(t,r).schema = t.schema
  check(t.schema, r) -> insert(t,r).rows = insert(r, t.rows)

  select(t,q).schema = t.schema
  r \in select(t,q).rows = r \in t.rows /\ r \in q