diff --git a/HaskRel.cabal b/HaskRel.cabal
new file mode 100644
--- /dev/null
+++ b/HaskRel.cabal
@@ -0,0 +1,96 @@
+name:                HaskRel
+
+version:             0.1.0.0
+
+synopsis:            HaskRel, Haskell as a DBMS with support for the relational algebra
+
+description:         HaskRel aims to define the elements of the relational theory of database management as first-class Haskell objects, thus enabling Haskell in its own right as a DBMS with first-class support for the relational algebra. It does not qualify as a proper RDBMS since it as-is only defines the relational algebra, relational variables and relational assignment. It does not define the relational calculus, views, constraints and transactions (beyond the fundamental requirement that the tuples of relations are to be unique), certain operators like relation valued aggregate operators, nor a few minor or even deprecated operators such as DIVIDE. The implemented parts are decently complete even if there are major implementation shortcomings that prevent this from being practically usable as an actual DBMS.
+                    .
+                     I refer to it as "/first-class/" since the types of the relational model are first-class types to Haskell, and the Haskell type system is able to induce the type resulting of relational expressions (for instance that a natural join of two relations results in a relation with a heading that is the setwise union of the headings of the original relations).
+                    .
+                     == Model
+                    .
+                     HaskRel is based on the relational model of database management, as defined by Chris Date and Hugh Darwen today. Is is not based on SQL in any way. SQL and Relational Theory, 2nd ed. [1] has been the principal guide in this endeavor (I have plenty of SQL in my background so a book on SQL and the relational model has been a good introduction to the latter). See also The Third Manifesto [2], and the additional material on http://www.thethirdmanifesto.com/ (this might be better to start with for those mathematically inclined but not steeped in SQL).
+                    .
+                     In addition to naming certain other aspects of Tutorial D has been adopted, such as argument order. Such aspects may be changed in the future if HaskRel is found to be solid enough to stand on its own, particularly if there are ways to express this that are more idiomatic vis-a-vis Haskell (Tutorial D is, after all, not a definition of the relational model, but vehicle for understanding it).
+                    .
+                     == Implementation
+                    .
+                     HaskRel is developed and tested with GHC 7.10.2. It builds upon HList (at least version 0.4.0.0). Separately from this library there is also an optional variant that builds on TIPs instead of records, which additionally relies on Lens (tested with version 4.12.3).
+                    .
+                     = Examples
+                    .
+                     The examples in this documentation are based on "the old warhorse" that is the suppliers-parts database (see [1] for more). This gives a body of relational expressions with known results to base examples upon. See also examples\/SuppliersPartsExamples.hs (not visible from this documentation) for Haskell versions of a selection of the Tutorial D expressions given as examples in chapters 6 and 7 of [1]. These can be run by starting examples\/suppliersPartsDB.sh and then running @snrt2ndExamples@. While most Tutorial D expressions translate fairly verbatim to Haskell there are a few where one must be a bit more explicit. While most Tutorial D expressions translate fairly verbatim to Haskell there are a few where Haskell is stricter than Tutorial D and one must be a bit more explicit.
+                    .
+                     $ is always used after `p`\/`rPrint` or `pt`\/`rPrintTyped` in the examples to keep them uniform (and so it kinda looks like a prompt), even when not required. The short forms `p` and `pt` are used whenever there isn't a conflict with other identifiers, whereas for the SuppliersPartsExample, which has a relvar "@p@", `rPrint` is used instead of `p` for presentation of relational objects without type information.
+                    .
+                     = Terminology
+                    .
+                     Since this builds on both Haskell and relational theory this documentation uses terms as they have been established in material related to either. Several terms of Haskell and HList have been redefined in terms of relational theory in this library, mostly to illustrate how terms and concepts have been mapped from the latter to the former. (I'm trying to keep this open to change later if it turns out to be an unhelpful crutch.)
+                    .
+                     The following table gives a quick overview of either terms or concepts as found in Haskell, the relational model (as presented in [1]), HaskRel and SQL, and how they are mapped from the second to the first:
+                    .
+                     @
+                     ┌───────────────────────────┬────────────────────┬────────────┬────────────────────────────────────────────────┐
+                     │ haskell                   │ relModel           │ haskRel    │ sql                                            │
+                     ╞═══════════════════════════╪════════════════════╪════════════╪════════════════════════════════════════════════╡
+                     │ <https://hackage.haskell.org/package/tagged/docs/Data-Tagged.html Data.Tagged.Tagged>        │ attribute          │ Attr       │ field, column                                  │
+                     │ <https://hackage.haskell.org/package/HList/docs/Data-HList-Record.html Data.HList.Record.Record>  │ tuple              │ RTuple     │ row                                            │
+                     │ ( <https://hackage.haskell.org/package/containers/docs/Data-Set.html Set> (<https://hackage.haskell.org/package/HList/docs/Data-HList-Record.html Record> a) )        │ relation           │ Relation a │ table                                          │
+                     │ <https://hackage.haskell.org/package/filepath/docs/System-FilePath.html FilePath> (<https://hackage.haskell.org/package/containers/docs/Data-Set.html Set> (<https://hackage.haskell.org/package/HList/docs/Data-HList-Record.html Record> a)) │ relvar             │ Relvar a   │ table                                          │
+                     │ <https://hackage.haskell.org/package/HList/docs/Data-HList-FakePrelude.html#t:Label Data.HList.Record.Label>   │ attribute name     │ Label      │ field name, column name                        │
+                     │ <https://hackage.haskell.org/package/HList/docs/Data-HList-Record.html#t:Labels Data.HList.Record.Labels>  │ attribute name set │ Labels     │ list of field/column names                     │
+                     │ function, operator        │ operator           │ function   │ operator, function, procedure, routine, method │
+                     └───────────────────────────┴────────────────────┴────────────┴────────────────────────────────────────────────┘
+                     @
+                    .
+                     Found in "example\/Terminology.hs". Note that this is just an overview, study of [1] or [2], Haskell itself, HList and HaskRel is required to see how terms and concepts correlate.
+                    .
+                     The term \"RTuple\", or "r-tuple", is chosen to simultaneously distinguish the concept from Haskell tuples while relating it to tuples of the relational model. For the type of either "Record a" or "Set ( Record a )" in Haskell the term "heading" is used in relational theory, and "row type" or "composite type" in SQL. In relational theory the term "scalar" is used to refer to data types that are neither tuples nor relations, which corresponds to everything but "Record a" or "Set ( Record a )" in Haskell. Note also that HaskRel /does/ use the term "table", but then only in the sense of "presentation of a relation value" (see above).
+                    .
+                     == The HaskRel library
+                    .
+                     Not all modules of this library are relevant to gain an understanding of how it functions, the next part to go to at this point is "Database.HaskRel.RDBMS", and the modules it reexports.
+                    .
+                     [1] <http://shop.oreilly.com/product/0636920022879.do SQL and Relational Theory, 2nd ed. (2011), C.J. Date>
+                     [2] <http://www.dcs.warwick.ac.uk/~hugh/TTM/TTM-2013-02-07.pdf The Third Manifesto, C. J. Date and Hugh Darwen, February 7th, 2013>
+
+license:             GPL-2
+
+license-file:        LICENSE
+
+author:              Thor Michael Støre
+
+maintainer:          thormichael@gmail.com
+
+copyright:           Thor Michael Støre 2015
+
+category:            Database
+
+build-type:          Simple
+
+extra-source-files:  examples/*.hs, examples/*.sh, examples/SuppliersPartsDB/*.hs
+
+data-files:          README.md, examples/SuppliersPartsDB/README.md, examples/SuppliersPartsDB/*.rv
+
+cabal-version:       >=1.10
+
+tested-with:         GHC==7.10.2
+
+source-repository head
+  type:     git
+  location: https://github.com/thormick/HaskRel
+
+library
+  exposed-modules:     Database.HaskRel.RDBMS, Database.HaskRel.FWTabulation, Database.HaskRel.HFWTabulation, Database.HaskRel.Order, Database.HaskRel.Support, Database.HaskRel.Relational.Algebra, Database.HaskRel.Relational.Assignment, Database.HaskRel.Relational.Definition, Database.HaskRel.Relational.Expression, Database.HaskRel.Relational.Unicode, Database.HaskRel.Relational.Variable
+  
+  default-extensions:  DataKinds
+  
+  other-extensions:    TypeOperators, FlexibleContexts, ScopedTypeVariables, PolyKinds, TypeFamilies, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances, KindSignatures
+  
+  build-depends:       base >=4.8 && <4.9, HList >=0.4 && <0.5, lens >=4.12 && <4.13, containers >=0.5 && <0.6, tagged >=0.8 && <0.9, directory >=1.2 && <1.3, ghc-prim >=0.4 && <0.5
+  
+  hs-source-dirs:      src
+  
+  default-language:    Haskell2010
+  
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,339 @@
+             GNU GENERAL PUBLIC LICENSE
+                Version 2, June 1991
+
+ Copyright (C) 1989, 1991 Free Software Foundation, Inc.,
+ 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+                     Preamble
+
+  The licenses for most software are designed to take away your
+freedom to share and change it.  By contrast, the GNU General Public
+License is intended to guarantee your freedom to share and change free
+software--to make sure the software is free for all its users.  This
+General Public License applies to most of the Free Software
+Foundation's software and to any other program whose authors commit to
+using it.  (Some other Free Software Foundation software is covered by
+the GNU Lesser General Public License instead.)  You can apply it to
+your programs, too.
+
+  When we speak of free software, we are referring to freedom, not
+price.  Our General Public Licenses are designed to make sure that you
+have the freedom to distribute copies of free software (and charge for
+this service if you wish), that you receive source code or can get it
+if you want it, that you can change the software or use pieces of it
+in new free programs; and that you know you can do these things.
+
+  To protect your rights, we need to make restrictions that forbid
+anyone to deny you these rights or to ask you to surrender the rights.
+These restrictions translate to certain responsibilities for you if you
+distribute copies of the software, or if you modify it.
+
+  For example, if you distribute copies of such a program, whether
+gratis or for a fee, you must give the recipients all the rights that
+you have.  You must make sure that they, too, receive or can get the
+source code.  And you must show them these terms so they know their
+rights.
+
+  We protect your rights with two steps: (1) copyright the software, and
+(2) offer you this license which gives you legal permission to copy,
+distribute and/or modify the software.
+
+  Also, for each author's protection and ours, we want to make certain
+that everyone understands that there is no warranty for this free
+software.  If the software is modified by someone else and passed on, we
+want its recipients to know that what they have is not the original, so
+that any problems introduced by others will not reflect on the original
+authors' reputations.
+
+  Finally, any free program is threatened constantly by software
+patents.  We wish to avoid the danger that redistributors of a free
+program will individually obtain patent licenses, in effect making the
+program proprietary.  To prevent this, we have made it clear that any
+patent must be licensed for everyone's free use or not licensed at all.
+
+  The precise terms and conditions for copying, distribution and
+modification follow.
+
+             GNU GENERAL PUBLIC LICENSE
+   TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION
+
+  0. This License applies to any program or other work which contains
+a notice placed by the copyright holder saying it may be distributed
+under the terms of this General Public License.  The "Program", below,
+refers to any such program or work, and a "work based on the Program"
+means either the Program or any derivative work under copyright law:
+that is to say, a work containing the Program or a portion of it,
+either verbatim or with modifications and/or translated into another
+language.  (Hereinafter, translation is included without limitation in
+the term "modification".)  Each licensee is addressed as "you".
+
+Activities other than copying, distribution and modification are not
+covered by this License; they are outside its scope.  The act of
+running the Program is not restricted, and the output from the Program
+is covered only if its contents constitute a work based on the
+Program (independent of having been made by running the Program).
+Whether that is true depends on what the Program does.
+
+  1. You may copy and distribute verbatim copies of the Program's
+source code as you receive it, in any medium, provided that you
+conspicuously and appropriately publish on each copy an appropriate
+copyright notice and disclaimer of warranty; keep intact all the
+notices that refer to this License and to the absence of any warranty;
+and give any other recipients of the Program a copy of this License
+along with the Program.
+
+You may charge a fee for the physical act of transferring a copy, and
+you may at your option offer warranty protection in exchange for a fee.
+
+  2. You may modify your copy or copies of the Program or any portion
+of it, thus forming a work based on the Program, and copy and
+distribute such modifications or work under the terms of Section 1
+above, provided that you also meet all of these conditions:
+
+    a) You must cause the modified files to carry prominent notices
+    stating that you changed the files and the date of any change.
+
+    b) You must cause any work that you distribute or publish, that in
+    whole or in part contains or is derived from the Program or any
+    part thereof, to be licensed as a whole at no charge to all third
+    parties under the terms of this License.
+
+    c) If the modified program normally reads commands interactively
+    when run, you must cause it, when started running for such
+    interactive use in the most ordinary way, to print or display an
+    announcement including an appropriate copyright notice and a
+    notice that there is no warranty (or else, saying that you provide
+    a warranty) and that users may redistribute the program under
+    these conditions, and telling the user how to view a copy of this
+    License.  (Exception: if the Program itself is interactive but
+    does not normally print such an announcement, your work based on
+    the Program is not required to print an announcement.)
+
+These requirements apply to the modified work as a whole.  If
+identifiable sections of that work are not derived from the Program,
+and can be reasonably considered independent and separate works in
+themselves, then this License, and its terms, do not apply to those
+sections when you distribute them as separate works.  But when you
+distribute the same sections as part of a whole which is a work based
+on the Program, the distribution of the whole must be on the terms of
+this License, whose permissions for other licensees extend to the
+entire whole, and thus to each and every part regardless of who wrote it.
+
+Thus, it is not the intent of this section to claim rights or contest
+your rights to work written entirely by you; rather, the intent is to
+exercise the right to control the distribution of derivative or
+collective works based on the Program.
+
+In addition, mere aggregation of another work not based on the Program
+with the Program (or with a work based on the Program) on a volume of
+a storage or distribution medium does not bring the other work under
+the scope of this License.
+
+  3. You may copy and distribute the Program (or a work based on it,
+under Section 2) in object code or executable form under the terms of
+Sections 1 and 2 above provided that you also do one of the following:
+
+    a) Accompany it with the complete corresponding machine-readable
+    source code, which must be distributed under the terms of Sections
+    1 and 2 above on a medium customarily used for software interchange; or,
+
+    b) Accompany it with a written offer, valid for at least three
+    years, to give any third party, for a charge no more than your
+    cost of physically performing source distribution, a complete
+    machine-readable copy of the corresponding source code, to be
+    distributed under the terms of Sections 1 and 2 above on a medium
+    customarily used for software interchange; or,
+
+    c) Accompany it with the information you received as to the offer
+    to distribute corresponding source code.  (This alternative is
+    allowed only for noncommercial distribution and only if you
+    received the program in object code or executable form with such
+    an offer, in accord with Subsection b above.)
+
+The source code for a work means the preferred form of the work for
+making modifications to it.  For an executable work, complete source
+code means all the source code for all modules it contains, plus any
+associated interface definition files, plus the scripts used to
+control compilation and installation of the executable.  However, as a
+special exception, the source code distributed need not include
+anything that is normally distributed (in either source or binary
+form) with the major components (compiler, kernel, and so on) of the
+operating system on which the executable runs, unless that component
+itself accompanies the executable.
+
+If distribution of executable or object code is made by offering
+access to copy from a designated place, then offering equivalent
+access to copy the source code from the same place counts as
+distribution of the source code, even though third parties are not
+compelled to copy the source along with the object code.
+
+  4. You may not copy, modify, sublicense, or distribute the Program
+except as expressly provided under this License.  Any attempt
+otherwise to copy, modify, sublicense or distribute the Program is
+void, and will automatically terminate your rights under this License.
+However, parties who have received copies, or rights, from you under
+this License will not have their licenses terminated so long as such
+parties remain in full compliance.
+
+  5. You are not required to accept this License, since you have not
+signed it.  However, nothing else grants you permission to modify or
+distribute the Program or its derivative works.  These actions are
+prohibited by law if you do not accept this License.  Therefore, by
+modifying or distributing the Program (or any work based on the
+Program), you indicate your acceptance of this License to do so, and
+all its terms and conditions for copying, distributing or modifying
+the Program or works based on it.
+
+  6. Each time you redistribute the Program (or any work based on the
+Program), the recipient automatically receives a license from the
+original licensor to copy, distribute or modify the Program subject to
+these terms and conditions.  You may not impose any further
+restrictions on the recipients' exercise of the rights granted herein.
+You are not responsible for enforcing compliance by third parties to
+this License.
+
+  7. If, as a consequence of a court judgment or allegation of patent
+infringement or for any other reason (not limited to patent issues),
+conditions are imposed on you (whether by court order, agreement or
+otherwise) that contradict the conditions of this License, they do not
+excuse you from the conditions of this License.  If you cannot
+distribute so as to satisfy simultaneously your obligations under this
+License and any other pertinent obligations, then as a consequence you
+may not distribute the Program at all.  For example, if a patent
+license would not permit royalty-free redistribution of the Program by
+all those who receive copies directly or indirectly through you, then
+the only way you could satisfy both it and this License would be to
+refrain entirely from distribution of the Program.
+
+If any portion of this section is held invalid or unenforceable under
+any particular circumstance, the balance of the section is intended to
+apply and the section as a whole is intended to apply in other
+circumstances.
+
+It is not the purpose of this section to induce you to infringe any
+patents or other property right claims or to contest validity of any
+such claims; this section has the sole purpose of protecting the
+integrity of the free software distribution system, which is
+implemented by public license practices.  Many people have made
+generous contributions to the wide range of software distributed
+through that system in reliance on consistent application of that
+system; it is up to the author/donor to decide if he or she is willing
+to distribute software through any other system and a licensee cannot
+impose that choice.
+
+This section is intended to make thoroughly clear what is believed to
+be a consequence of the rest of this License.
+
+  8. If the distribution and/or use of the Program is restricted in
+certain countries either by patents or by copyrighted interfaces, the
+original copyright holder who places the Program under this License
+may add an explicit geographical distribution limitation excluding
+those countries, so that distribution is permitted only in or among
+countries not thus excluded.  In such case, this License incorporates
+the limitation as if written in the body of this License.
+
+  9. The Free Software Foundation may publish revised and/or new versions
+of the General Public License from time to time.  Such new versions will
+be similar in spirit to the present version, but may differ in detail to
+address new problems or concerns.
+
+Each version is given a distinguishing version number.  If the Program
+specifies a version number of this License which applies to it and "any
+later version", you have the option of following the terms and conditions
+either of that version or of any later version published by the Free
+Software Foundation.  If the Program does not specify a version number of
+this License, you may choose any version ever published by the Free Software
+Foundation.
+
+  10. If you wish to incorporate parts of the Program into other free
+programs whose distribution conditions are different, write to the author
+to ask for permission.  For software which is copyrighted by the Free
+Software Foundation, write to the Free Software Foundation; we sometimes
+make exceptions for this.  Our decision will be guided by the two goals
+of preserving the free status of all derivatives of our free software and
+of promoting the sharing and reuse of software generally.
+
+                     NO WARRANTY
+
+  11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY
+FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW.  EXCEPT WHEN
+OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES
+PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED
+OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
+MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS
+TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU.  SHOULD THE
+PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING,
+REPAIR OR CORRECTION.
+
+  12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING
+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR
+REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES,
+INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING
+OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED
+TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY
+YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER
+PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGES.
+
+              END OF TERMS AND CONDITIONS
+
+     How to Apply These Terms to Your New Programs
+
+  If you develop a new program, and you want it to be of the greatest
+possible use to the public, the best way to achieve this is to make it
+free software which everyone can redistribute and change under these terms.
+
+  To do so, attach the following notices to the program.  It is safest
+to attach them to the start of each source file to most effectively
+convey the exclusion of warranty; and each file should have at least
+the "copyright" line and a pointer to where the full notice is found.
+
+    <one line to give the program's name and a brief idea of what it does.>
+    Copyright (C) <year>  <name of author>
+
+    This program is free software; you can redistribute it and/or modify
+    it under the terms of the GNU General Public License as published by
+    the Free Software Foundation; either version 2 of the License, or
+    (at your option) any later version.
+
+    This program is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+    GNU General Public License for more details.
+
+    You should have received a copy of the GNU General Public License along
+    with this program; if not, write to the Free Software Foundation, Inc.,
+    51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+
+Also add information on how to contact you by electronic and paper mail.
+
+If the program is interactive, make it output a short notice like this
+when it starts in an interactive mode:
+
+    Gnomovision version 69, Copyright (C) year name of author
+    Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'.
+    This is free software, and you are welcome to redistribute it
+    under certain conditions; type `show c' for details.
+
+The hypothetical commands `show w' and `show c' should show the appropriate
+parts of the General Public License.  Of course, the commands you use may
+be called something other than `show w' and `show c'; they could even be
+mouse-clicks or menu items--whatever suits your program.
+
+You should also get your employer (if you work as a programmer) or your
+school, if any, to sign a "copyright disclaimer" for the program, if
+necessary.  Here is a sample; alter the names:
+
+  Yoyodyne, Inc., hereby disclaims all copyright interest in the program
+  `Gnomovision' (which makes passes at compilers) written by James Hacker.
+
+  <signature of Ty Coon>, 1 April 1989
+  Ty Coon, President of Vice
+
+This General Public License does not permit incorporating your program into
+proprietary programs.  If your program is a subroutine library, you may
+consider it more useful to permit linking proprietary applications with the
+library.  If this is what you want to do, use the GNU Lesser General
+Public License instead of this License.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,132 @@
+HaskRel, Haskell as a DBMS with support for the relational algebra
+==================================================================
+
+(C) 2015, Thor Michael Støre
+
+HaskRel aims to define the elements of the relational theory of database management as first-class Haskell objects, thus enabling Haskell in its own right as a DBMS with first-class support for the relational algebra. It does not qualify as a proper RDBMS since it as-is only defines the relational algebra, relational variables and relational assignment. It does not define the relational calculus, views, constraints and transactions (beyond the fundamental requirement that the tuples of relations are to be unique), certain operators like relation valued aggregate operators, nor a few minor or even deprecated operators such as DIVIDE. The implemented parts are decently complete even if there are major implementation shortcomings that prevent this from being practically usable as an actual DBMS.
+
+I refer to it as _first-class_ since the types of the relational model are first-class types to Haskell, and the Haskell type system is able to induce the type resulting of relational expressions (for instance that a natural join of two relations results in a relation with a heading that is the setwise union of the headings of the original relations).
+
+As such it isn't as much just an implementation of the relational model built using Haskell (the way, say, PostgreSQL is an implementation of SQL using C), as a Haskell library that accommodates a subset of the relational model (unlike PostgreSQL, which doesn't turn C into an RDBMS), where GHCi is employed as a database terminal front-end.
+
+HaskRel is not based on SQL, there is no support for anything that it defines beyond what the relational model does, nor plans for that. It is instead inspired by Tutorial D. For a project of this kind it is generally more sensible to follow developed theory as it stands rather than an industry standard. More specifically, HaskRel is intended as an exploration of the possibilities to directly employ a general purpose programming language and its associated REPL as a relational database management system, or even as a bit of an academic exercise, and a great deal of SQL is not relevant towards this end. (SQL defines for instance its own types, while HaskRel is explicitly intended to build upon Haskell's, and SQL's type system is weaker than Haskell's, in that it employs a wide range of coercions between types). Features and aspects of SQL are either irrelevant for the purpose of HaskRel, or overlap or conflict with Haskell idioms that are more relevant to adhere to for a "make an RDBMS out of a general purpose programming language" project. (Parts of Tutorial D also overlap, such as the `THE_` operator and selectors vs. show and read, but all in all a fraction of what SQL does.) Even if there were plans to go beyond this and support SQL it would be a good first step to first support the fundamentals of the relational model both as _completely_ as it is reasonable to do, and to do so _properly_.
+
+For an understanding of the foundation HaskRel builds on see for instance [SQL and Relational Theory, 2nd ed.](http://shop.oreilly.com/product/0636920022879.do), [The Third Manifesto](http://www.dcs.warwick.ac.uk/~hugh/TTM/TTM-2013-02-07.pdf), and the additional material on [http://www.thethirdmanifesto.com/]().
+
+Of the shortcomings of model that are mentioned above the relational calculus, database constraints, and transactions would be possible to add in a reasonably complete manner (I hope I am able to work on this). Views would be the most difficult, as far as I able to tell it is not possible to properly implement this fully within Haskell, although I don't know if some part of it can be. (This is something SQL products have had difficulties with, after all, and an area where the SQL standard is obtuse.) One further particular issue is that data definition is performed by writing, compiling and loading Haskell, which is particularly static compared to DDL in a proper DBMS.
+
+There are many missing implementation level features that database products rely on, enough so that HaskRel neither is nor will be usable as a production system, even if the shortcomings mentioned regarding the model was in place. Query optimization and indexes are the major ones, just for starters, which would require a monumental effort that there are no plans for. There is also the issue that even slightly complex queries have compile times running into several seconds. HaskRel also builds on Data.Set to manage relation bodies, although this is too limited to support a practically usable RDBMS, at least by itself.
+
+In any case, HaskRel is very, very far from being a usable database management system, and there is as such no plan to bring it there, but I hope it's useful from an academic perspective.
+
+
+Trying it out
+-------------
+
+To get started with an example database cd into examples, run suppliersPartsDB.sh, look through SuppliersPartsExample.hs, and run examples from the Haddock or that file.
+
+Alternatively, if one runs `cabal repl` one will have to either load a file with definitions, or define some elements to play around with. In the example below most everything is ad-hoc, predefining a few values would make certain expressions look less messy. Here are what constants look like:
+
+    *Database.HaskRel.RDBMS> let foo = relation' [( 10, "foo" ),( 20, "bar" ) ] :: Relation '[Attr "asdf" Int, Attr "qwer" String]
+    *Database.HaskRel.RDBMS> let bar = relation' [( 10, "one" ),( 30, "two" ) ] :: Relation '[Attr "asdf" Int, Attr "zxcv" String]
+    *Database.HaskRel.RDBMS> pt foo
+    ┌─────────────┬────────────────┐
+    │ asdf :: Int │ qwer :: String │
+    ╞═════════════╪════════════════╡
+    │ 10          │ foo            │
+    │ 20          │ bar            │
+    └─────────────┴────────────────┘
+    *Database.HaskRel.RDBMS> pt bar
+    ┌─────────────┬────────────────┐
+    │ asdf :: Int │ zxcv :: String │
+    ╞═════════════╪════════════════╡
+    │ 10          │ one            │
+    │ 30          │ two            │
+    └─────────────┴────────────────┘
+    *Database.HaskRel.RDBMS> pt$ foo `naturalJoin` bar
+    ┌─────────────┬────────────────┬────────────────┐
+    │ asdf :: Int │ qwer :: String │ zxcv :: String │
+    ╞═════════════╪════════════════╪════════════════╡
+    │ 10          │ foo            │ one            │
+    └─────────────┴────────────────┴────────────────┘
+
+(Note that certain operating systems and browsers have difficulties displaying the double underline of tables. On OS X Firefox has worked better than Chrome.)
+
+As advertised, Haskell infers the type of relational expressions:
+
+    *Database.HaskRel.RDBMS> :t foo
+    foo :: Relation '[Attr "asdf" Int, Attr "qwer" String]
+    *Database.HaskRel.RDBMS> :t bar
+    bar :: Relation '[Attr "asdf" Int, Attr "zxcv" String]
+    *Database.HaskRel.RDBMS> :t (foo `naturalJoin` bar)
+    (foo `nJoin` bar)
+      :: containers-0.5.6.2:Data.Set.Base.Set
+           (RTuple
+              '[Tagged "asdf" Int, Tagged "qwer" String, Tagged "zxcv" [Char]])
+
+Ad-hoc relvars can be defined thusly:
+
+    *Database.HaskRel.RDBMS> let baz = Relvar "baz.rv" :: Relvar '[Attr "asdf" Int, Attr "qwer" String]
+    *Database.HaskRel.RDBMS> assign baz (empty :: Relation '[Attr "asdf" Int, Attr "qwer" String] )
+    Value assigned to baz.rv
+
+See "examples" for the proper way to do this.
+
+`assign` against a newly defined relvar initializes it in the file system, and will create a file relative to the directory the interpreter is run from.
+
+    *Database.HaskRel.RDBMS> pt baz
+    ┌─────────────┬────────────────┐
+    │ asdf :: Int │ qwer :: String │
+    ╞═════════════╪════════════════╡
+    └─────────────┴────────────────┘
+    *Database.HaskRel.RDBMS> insert baz foo
+    Inserted 2 of 2 tuples into baz.rv
+    *Database.HaskRel.RDBMS> pt baz
+    ┌─────────────┬────────────────┐
+    │ asdf :: Int │ qwer :: String │
+    ╞═════════════╪════════════════╡
+    │ 10          │ foo            │
+    │ 20          │ bar            │
+    └─────────────┴────────────────┘
+    *Database.HaskRel.RDBMS> insert baz ( relation [rTuple ((Label::Label "asdf") .=. 30, (Label::Label "qwer") .=. "frotz")] )
+    Inserted 1 of 1 tuples into baz.rv
+    *Database.HaskRel.RDBMS> pt baz
+    ┌─────────────┬────────────────┐
+    │ asdf :: Int │ qwer :: String │
+    ╞═════════════╪════════════════╡
+    │ 10          │ foo            │
+    │ 20          │ bar            │
+    │ 30          │ frotz          │
+    └─────────────┴────────────────┘
+
+Concise expression of updates require a set of language extensions:
+
+    *Database.HaskRel.RDBMS> :set -XQuasiQuotes -XKindSignatures -XViewPatterns
+    *Database.HaskRel.RDBMS> update baz (\ [pun|asdf|] -> asdf > 15 ) (\ [pun|qwer|] -> case (qwer ++ "-new") of (qwer) -> [pun|qwer|])
+    Updated 2 of 3 tuples in baz.rv
+    *Database.HaskRel.RDBMS> pt baz
+    ┌─────────────┬────────────────┐
+    │ asdf :: Int │ qwer :: String │
+    ╞═════════════╪════════════════╡
+    │ 10          │ foo            │
+    │ 20          │ bar-new        │
+    │ 30          │ frotz-new      │
+    └─────────────┴────────────────┘
+
+All functions of the relational algebra that HaskRel implement work against both relation constants and relvars, as do the print functions `p` and `pt`:
+
+    *Database.HaskRel.RDBMS> p$ baz `nJoin` bar
+    ┌──────┬───────────┬──────┐
+    │ asdf │ qwer      │ zxcv │
+    ╞══════╪═══════════╪══════╡
+    │ 10   │ foo       │ one  │
+    │ 30   │ frotz-new │ two  │
+    └──────┴───────────┴──────┘
+
+
+Contributions
+-------------
+
+While contributions to HaskRel itself would be great, the limiting factors for HaskRel to develop further, let alone be usable, is in its foundations. The most interesting work that could be done with HaskRel is to go through it and find points where Haskell or its ecosystem could be improved to the benefit of both HaskRel and other projects, and focus development efforts on that. The two most important libraries that HaskRel builds on are HList and Data.Set; efforts towards improving them or arguments towards replacing them would be beneficial.
+
+Making HaskRel usable for practical purposes is not on the horizon, but it may be possible to improve it further towards being a demonstrator of the relational model. A list of "things Haskell needs in order to qualify as a first class RDBMS" would also be a fun list to have, even if there isn't a chance of it happening.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/examples/AlgebraExample.hs b/examples/AlgebraExample.hs
new file mode 100644
--- /dev/null
+++ b/examples/AlgebraExample.hs
@@ -0,0 +1,131 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE FlexibleContexts #-} 
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
+--{-# LANGUAGE ViewPatterns #-}
+
+module AlgebraExample where
+
+import Data.HList.CommonMain
+
+import Control.Lens ( (^.), from, to )
+
+-- To make a few type signatures prettier
+import Data.Set ( Set )
+
+-- To use HList constructors directly, instead of "relation"/"relation'"
+import Data.Set ( fromList )
+
+--
+
+import Database.HaskRel.Support
+import Database.HaskRel.Relational.Definition
+import Database.HaskRel.Relational.Algebra
+
+
+import SuppliersPartsDB.Definition
+import SuppliersPartsDB.Default
+
+--
+import qualified Data.Set ( map )
+
+{-
+
+let fooAgg = agg sno
+
+let sumqty = sum . agg qty
+
+
+λ> :t agg
+agg :: (Foldable t, HasField l a a1) => Label l -> t a -> [a1]
+λ> :t (\a -> agg (\ [pun|sno pno|] -> sno ) a )
+nope
+
+aggP: aggregate-on-pun, to give multiple variables based on aggregated attributes...
+
+λ> :t  [pun|sno pno|]
+[pun|sno pno|]
+  :: HExtendR
+       (Tagged "sno" (Label "sno")) (Record '[Tagged "pno" (Label "pno")])
+
+-- Relation '[Tagged "sno" String, Tagged "qty" Integer] -> Record '[Tagged "qty" Integer]
+
+
+:t groupR2 sp' (undefined :: Relation '[Tagged "pno" String, Tagged "qty" Integer] -> Record '[Tagged "qty" Integer] )
+
+
+groupR2 sp' (\(r:: Relation '[Tagged "pno" String, Tagged "qty" Integer] -> Record '[Tagged "qty" Integer]) -> ( Label :: Label "qty" ) .=. agg qty r .*. emptyRecord)
+
+
+(undefined :: Relation '[Tagged "pno" String, Tagged "qty" Integer] -> Record '[Tagged "qty" Integer] )
+
+-}
+-- group rel attsIn = extendByImage rel $ rel `projectAllBut` attsIn
+
+-- sno .=. "qwer" .*. hDeleteAtLabel (Label::Label "sno") (sno .=. "asf" .*. emptyRecord)
+
+extendOrUpdate ::
+     (HExtend e (r v'), HDeleteAtLabel r l v v') =>
+     r v -> e -> Label l -> HExtendR e (r v')
+extendOrUpdate r v l = v .*. hDeleteAtLabel l r
+
+extendOrUpdate' :: forall l e r v v'.
+    (HDeleteAtLabel r l v v', HExtend (Tagged l e) (r v')) =>
+    r v -> Tagged l e -> HExtendR (Tagged l e) (r v')
+extendOrUpdate' r v = v .*. hDeleteAtLabel (Label::Label l) r
+
+-- * Different ways to represent relations
+
+{-
+The standard representation, patterned after Tutorial D. Dependent upon defining
+data construction functions, or using the HList .=. operator. Uses the rTuple
+function and explicit construction of the fields.
+-}
+snoStatusR1 = relation [rTuple (sno .=. "S1", status .=. 40),
+                        rTuple (sno .=. "S2", status .=. 30)]
+
+{-
+The inductive representation, where the body is made more consise by only
+specifying the values, and relying on type induction to define the type and the
+labels of the elements (attribute type and attribute name in the relational
+model). This also frees one from dependence upon defining data construction
+functions. It holds that snoStatusR1 == snoStatusR2
+-}
+snoStatusR2 = relation' [("S1", 40),
+                         ("S2", 30)]
+              :: Relation '[SNO, Status]
+{- Remembering how SNO and Status are type synonyms, the last line could just as well be:
+              :: Relation '[Attr "sno" String, Attr "status" Int]
+
+Which is the form one must employ when building relation values of ad-hoc types.
+-}
+
+{-
+If one wants to use the relation/rTuple functions, but in a completely ad-hoc
+manner, it'll have to look as follows.
+-}
+snoStatusR3 = relation [
+  rTuple ((Label :: Label "sno") .=. "S1", (Label :: Label "status") .=. (40::Int)),
+  rTuple ((Label :: Label "sno") .=. "S2", (Label :: Label "status") .=. 30)]
+
+{-
+While the standard Haskell and HList approach will look like this:
+-}
+
+snoStatusR4 = Data.Set.fromList [
+  (Label :: Label "sno") .=. "S1" .*. (Label :: Label "status") .=. (40::Int) .*. emptyRecord,
+  (Label :: Label "sno") .=. "S2" .*. (Label :: Label "status") .=. 30 .*. emptyRecord]
+
+
+-- Single attribute extension:
+-- (\ ((\[pun|sno status|] -> (sno++"-foo", status+5)) -> sno) -> (Label::Label "sno") .=. sno ) (sno "input" .*. status (5::Integer) .*. emptyRecord)
+
+type GMWT   = Attr "gmwt"   Rational
+gmwt = Label::Label "gmwt"
+
+type SCity   = Attr "sCity"   String
+sCity = Label :: Label "sCity"
+
+type PQ = Attr "pq" (Relation '[PNO,QTY])
+pq = Label :: Label "pq"
diff --git a/examples/HFWTest.hs b/examples/HFWTest.hs
new file mode 100644
--- /dev/null
+++ b/examples/HFWTest.hs
@@ -0,0 +1,71 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+
+
+module HFWTest where
+
+import Control.Lens.Wrapped ( Wrapped, Unwrapped, _Wrapped', _Unwrapped' )
+import Control.Lens ( (^.) )
+import Control.Lens.TH ( makeWrapped )
+
+import Data.Typeable
+import Data.Data
+
+import Data.HList.CommonMain
+
+import Database.HaskRel.FWTabulation
+import Database.HaskRel.HFWTabulation
+import Database.HaskRel.TIPFWTabulation
+
+import Database.HaskRel.Relational.TIP.Definition
+
+
+
+
+
+sno = Label :: Label "sno"
+status = Label :: Label "status"
+sno_status = Label :: Label "sno_status"
+
+
+
+
+newtype SNO    = SNO    String   deriving ( Eq, Show, Read, Ord, Typeable, Data )
+newtype SName  = SName  String   deriving ( Eq, Show, Read, Ord, Typeable, Data )
+newtype Status = Status Integer  deriving ( Eq, Show, Read, Ord, Typeable, Data )
+newtype City   = City   String   deriving ( Eq, Show, Read, Ord, Typeable, Data )
+
+newtype PNO    = PNO    String   deriving ( Eq, Show, Read, Ord, Typeable, Data )
+newtype PName  = PName  String   deriving ( Eq, Show, Read, Ord, Typeable, Data )
+newtype Color  = Color  String   deriving ( Eq, Show, Read, Ord, Typeable, Data )
+newtype Weight = Weight Rational deriving ( Eq, Show, Read, Ord, Typeable, Data )
+
+newtype QTY    = QTY    Integer  deriving ( Eq, Show, Read, Ord, Typeable, Data )
+
+makeWrapped ''SNO
+makeWrapped ''SName
+makeWrapped ''Status
+makeWrapped ''City
+
+makeWrapped ''PNO
+makeWrapped ''PName
+makeWrapped ''Color
+makeWrapped ''Weight
+
+makeWrapped ''QTY
+
+{-
+newtype PQ = PQ ( Relation '[PNO, QTY] ) deriving ( Eq, Show, Ord, Typeable, Data )
+instance {-# OVERLAPPING #-} Data ( TIP '[Tagged PNO PNO, Tagged QTY QTY] ) where
+    gunfold = undefined
+    toConstr = undefined
+    dataTypeOf = undefined
+
+makeWrapped ''PQ
+-}
diff --git a/examples/SuppliersPartsDB/Default.hs b/examples/SuppliersPartsDB/Default.hs
new file mode 100644
--- /dev/null
+++ b/examples/SuppliersPartsDB/Default.hs
@@ -0,0 +1,86 @@
+{-# LANGUAGE DataKinds #-}
+
+{-|
+Default contents for the SuppliersPartsDB.
+-}
+module SuppliersPartsDB.Default where
+
+import Database.HaskRel.Relational.Definition ( Relation, relation, relation', rTuple )
+
+import SuppliersPartsDB.Definition
+
+import Data.HList.CommonMain ((.=.))
+
+{-
+Tutorial D:
+
+RELATION
+{ TUPLE { SNO ‘S1’ , SNAME ‘Smith’ , STATUS 20 , CITY ‘London’ } ,
+  TUPLE { SNO ‘S2’ , SNAME ‘Jones’ , STATUS 10 , CITY ‘Paris’ } ,
+  TUPLE { SNO ‘S3’ , SNAME ‘Blake’ , STATUS 30 , CITY ‘Paris’ } ,
+  TUPLE { SNO ‘S4’ , SNAME ‘Clark’ , STATUS 20 , CITY ‘London’ } ,
+  TUPLE { SNO ‘S5’ , SNAME ‘Adams’ , STATUS 30 , CITY ‘Athens’ } }
+
+
+In Tutorial D attribute identifiers can both be used without arguments (within a query to denote a attribute of a relation in scope), or with an argument as above, as a attribute constructor. The same can be achieved in Haskell in various ways. One way is defining all pertinent functions such that they allow both a label and a constructor without an argument, and then only defining such constructors:
+
+status a = (Label::Label "status") .=. (a::Integer)
+
+Which would allow:
+
+rTuple ( sno "S1" , sName "Smith" , status 20 , city "London" )
+
+While still letting one use sno, sName, etc as attribute identifiers in functions. However, doing this consistently requires some rather convoluted type-level acrobatics that causes exponential growth in function definition complexity. As such only labels are defined in these examples, which one must use .=. to construct into the tagged values that are directly employed by HaskRel as relational attributes.
+
+An alternative would be https://hackage.haskell.org/package/HList/docs/Data-HList-Labelable.html, though HaskRel records don't build on lens and can't accomodate that approach as-is.
+-}
+
+
+s' =
+    relation
+    [ rTuple ( sno .=. "S1" , sName .=. "Smith" , status .=. 20 , city .=. "London" ) ,
+      rTuple ( sno .=. "S2" , sName .=. "Jones" , status .=. 10 , city .=. "Paris" ) ,
+      rTuple ( sno .=. "S3" , sName .=. "Blake" , status .=. 30 , city .=. "Paris" ) ,
+      rTuple ( sno .=. "S4" , sName .=. "Clark" , status .=. 20 , city .=. "London" ) ,
+      rTuple ( sno .=. "S5" , sName .=. "Adams" , status .=. 30 , city .=. "Athens" ) ]
+        :: Relation '[SNO, SName, Status, City]
+
+p' =
+    relation
+    [ rTuple ( pno .=. "P1" , pName .=. "Nut" , color .=. "Red" , weight .=. 12.0 , city .=. "London" ) ,
+      rTuple ( pno .=. "P2" , pName .=. "Bolt" , color .=. "Green" , weight .=. 17.0 , city .=. "Paris" ) ,
+      rTuple ( pno .=. "P3" , pName .=. "Screw" , color .=. "Blue" , weight .=. 17.0 , city .=. "Oslo" ) ,
+      rTuple ( pno .=. "P4" , pName .=. "Screw" , color .=. "Red" , weight .=. 14.0 , city .=. "London" ) ,
+      rTuple ( pno .=. "P5" , pName .=. "Cam" , color .=. "Blue" , weight .=. 12.0 , city .=. "Paris" ) ,
+      rTuple ( pno .=. "P6" , pName .=. "Cog" , color .=. "Red" , weight .=. 19.0 , city .=. "London" ) ]
+        :: Relation '[PNO, PName, Color, Weight, City]
+
+-- Let's say that I'm tired of repeating the attribute names; syntactic sugar to
+-- the rescue, note the use of relation' instead of relation, and that the type
+-- annotation becomes mandatory:
+sp' =
+    relation'
+    [ ("S1", "P1", 300), 
+      ("S1", "P2", 200), 
+      ("S1", "P3", 400), 
+      ("S1", "P4", 200), 
+      ("S1", "P5", 100), 
+      ("S1", "P6", 100), 
+      ("S2", "P1", 300), 
+      ("S2", "P2", 400), 
+      ("S3", "P2", 200), 
+      ("S4", "P2", 200), 
+      ("S4", "P4", 300), 
+      ("S4", "P5", 400) ] :: Relation '[SNO, PNO, QTY]
+
+{-
+Also note how the attribute names above, SNO etc, are declared type synonyms in Definition.hs, and not ad-hoc. An equivalent ad-hoc definition would be:
+
+Relation '[Tagged "sno" String, Tagged "pno" String, Tagged "qty" Integer]
+
+
+An alternative approach is to define constructors for each label, which would also make it more type-safe:
+sno' a = (Label :: Label "sno") .=. a :: SNO
+
+There may be a way to build the functions of the relational algebra such that they accept both "Label l" and "v -> Tagged l v" types, which would make it possible that instead of label constants one could just define constructors and used those against the functions of the relational algebra, but an investigation into that revealed no attempt that didn't have an unacceptable drawback.
+-}
diff --git a/examples/SuppliersPartsDB/Definition.hs b/examples/SuppliersPartsDB/Definition.hs
new file mode 100644
--- /dev/null
+++ b/examples/SuppliersPartsDB/Definition.hs
@@ -0,0 +1,72 @@
+{-# LANGUAGE DataKinds, TemplateHaskell #-}
+
+{- | Data definition for HList record based suppliers and parts database. -}
+
+module SuppliersPartsDB.Definition where
+
+import Data.HList.CommonMain
+import Database.HaskRel.Relational.Definition
+import Database.HaskRel.Relational.Variable
+
+dbPath = "SuppliersPartsDB/"
+--dbPath = "examples/SuppliersPartsDB/"
+
+-- Attributes
+
+type SNO    = Attr "sno"    String
+type SName  = Attr "sName"  String
+type Status = Attr "status" Integer
+type City   = Attr "city"   String
+
+makeLabels6 ["sno","sName","status","city"]
+{- Expands to:
+sno = Label :: Label "sno"
+sName = Label :: Label "sName"
+status = Label :: Label "status"
+city = Label :: Label "city"
+
+Which is what one must append to "let " to do the same in GHCi.
+-}
+
+-- Tagged value/attribute constructors. These are convenient to have since the label names collide with the label functions when punning, which is a particular nuisance when using 'extend' to alter an attribute:
+_sno a = sno .=. a :: SNO
+_sName a = sName .=. a :: SName
+_status a = status .=. a :: Status
+_city a = city .=. a :: City
+
+
+
+type PNO    = Attr "pno"    String
+type PName  = Attr "pName"  String
+type Color  = Attr "color"  String
+type Weight = Attr "weight" Rational
+
+makeLabels6 ["pno","pName","color","weight"]
+
+_pno a = pno .=. a :: PNO
+_pName a = pName .=. a :: PName
+_color a = color .=. a :: Color
+_weight a = weight .=. a :: Weight
+
+
+type QTY    = Attr "qty"    Integer
+
+makeLabels6 ["qty"]
+
+_qty a = qty .=. a :: QTY
+
+
+-- Types. Header types in relational theory, of either relations or tuples.
+type S  = '[SNO, SName, Status, City]
+type SP = '[SNO, PNO, QTY]
+type P  = '[PNO, PName, Color, Weight, City]
+
+
+-- "Relvar S" could be used instead, but when doing ":t s" it's nicer to list the attributes.
+s  :: Relvar '[SNO, SName, Status, City]
+s   = Relvar ( dbPath ++ "S.rv" )
+sp :: Relvar '[SNO, PNO, QTY]
+sp  = Relvar ( dbPath ++ "SP.rv" )
+p  :: Relvar '[PNO, PName, Color, Weight, City]
+p   = Relvar ( dbPath ++ "P.rv" )
+
diff --git a/examples/SuppliersPartsDB/P.rv b/examples/SuppliersPartsDB/P.rv
new file mode 100644
--- /dev/null
+++ b/examples/SuppliersPartsDB/P.rv
@@ -0,0 +1,1 @@
+H["P1","Nut","Red",12 % 1,"London"],H["P2","Bolt","Green",17 % 1,"Paris"],H["P3","Screw","Blue",17 % 1,"Oslo"],H["P4","Screw","Red",14 % 1,"London"],H["P5","Cam","Blue",12 % 1,"Paris"],H["P6","Cog","Red",19 % 1,"London"]
diff --git a/examples/SuppliersPartsDB/README.md b/examples/SuppliersPartsDB/README.md
new file mode 100644
--- /dev/null
+++ b/examples/SuppliersPartsDB/README.md
@@ -0,0 +1,56 @@
+The relvars of SuppliersPartsDB, with types:
+
+    >>> pt$ s
+    ┌───────────────┬─────────────────┬───────────────────┬────────────────┐
+    │ sno :: String │ sName :: String │ status :: Integer │ city :: String │
+    ╞═══════════════╪═════════════════╪═══════════════════╪════════════════╡
+    │ S1            │ Smith           │ 20                │ London         │
+    │ S2            │ Jones           │ 10                │ Paris          │
+    │ S3            │ Blake           │ 30                │ Paris          │
+    │ S4            │ Clark           │ 20                │ London         │
+    │ S5            │ Adams           │ 30                │ Athens         │
+    └───────────────┴─────────────────┴───────────────────┴────────────────┘
+    >>> pt$ p
+    ┌───────────────┬─────────────────┬─────────────────┬─────────────────────────┬────────────────┐
+    │ pno :: String │ pName :: String │ color :: String │ weight :: Ratio Integer │ city :: String │
+    ╞═══════════════╪═════════════════╪═════════════════╪═════════════════════════╪════════════════╡
+    │ P1            │ Nut             │ Red             │ 12 % 1                  │ London         │
+    │ P2            │ Bolt            │ Green           │ 17 % 1                  │ Paris          │
+    │ P3            │ Screw           │ Blue            │ 17 % 1                  │ Oslo           │
+    │ P4            │ Screw           │ Red             │ 14 % 1                  │ London         │
+    │ P5            │ Cam             │ Blue            │ 12 % 1                  │ Paris          │
+    │ P6            │ Cog             │ Red             │ 19 % 1                  │ London         │
+    └───────────────┴─────────────────┴─────────────────┴─────────────────────────┴────────────────┘
+    >>> pt$ sp
+    ┌───────────────┬───────────────┬────────────────┐
+    │ sno :: String │ pno :: String │ qty :: Integer │
+    ╞═══════════════╪═══════════════╪════════════════╡
+    │ S1            │ P1            │ 300            │
+    │ S1            │ P2            │ 200            │
+    │ S1            │ P3            │ 400            │
+    │ S1            │ P4            │ 200            │
+    │ S1            │ P5            │ 100            │
+    │ S1            │ P6            │ 100            │
+    │ S2            │ P1            │ 300            │
+    │ S2            │ P2            │ 400            │
+    │ S3            │ P2            │ 200            │
+    │ S4            │ P2            │ 200            │
+    │ S4            │ P4            │ 300            │
+    │ S4            │ P5            │ 400            │
+    └───────────────┴───────────────┴────────────────┘
+
+(Note that certain combinations of operating systems and browsers don't seem to want to display the double line of the tables correctly. On OS X 10.8 Google Chrome doesn't, whereas Firefox seems to do just fine. See also the [Wikipedia entry on box-drawing characters](http://en.wikipedia.org/wiki/Box-drawing_character#Examples).)
+
+Relation values named s', p' and sp' are also defined, of the same values as above.
+
+    >>> :t s
+    s :: Relvar '[SNO, SName, Status, City]
+    >>> :t s'
+    s' :: Relation '[SNO, SName, Status, City]
+    >>> :i SNO
+    type SNO = Attr "sno" String
+      	-- Defined at SuppliersPartsDB/Definition.hs:16:1
+    >>> s `rEq` s'
+    True
+
+`pt$ s'`, `pt$ p'` and `pt$ sp'` will give the same result as above.
diff --git a/examples/SuppliersPartsDB/S.rv b/examples/SuppliersPartsDB/S.rv
new file mode 100644
--- /dev/null
+++ b/examples/SuppliersPartsDB/S.rv
@@ -0,0 +1,1 @@
+H["S1","Smith",20,"London"],H["S2","Jones",10,"Paris"],H["S3","Blake",30,"Paris"],H["S4","Clark",20,"London"],H["S5","Adams",30,"Athens"]
diff --git a/examples/SuppliersPartsDB/SP.rv b/examples/SuppliersPartsDB/SP.rv
new file mode 100644
--- /dev/null
+++ b/examples/SuppliersPartsDB/SP.rv
@@ -0,0 +1,1 @@
+H["S1","P1",300],H["S1","P2",200],H["S1","P3",400],H["S1","P4",200],H["S1","P5",100],H["S1","P6",100],H["S2","P1",300],H["S2","P2",400],H["S3","P2",200],H["S4","P2",200],H["S4","P4",300],H["S4","P5",400]
diff --git a/examples/SuppliersPartsExample.hs b/examples/SuppliersPartsExample.hs
new file mode 100644
--- /dev/null
+++ b/examples/SuppliersPartsExample.hs
@@ -0,0 +1,314 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts, TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE KindSignatures, QuasiQuotes, ViewPatterns #-}
+
+-- TODO: Does this have more performance issues than the TIP based version?
+module SuppliersPartsExample where
+
+import Database.HaskRel.Relational.Definition ( Relation, RTuple, Attr, relation, relation', tableDum, tableDee, empty, rTuple, pt, rPrint )
+
+import Database.HaskRel.RDBMS hiding ( p )
+import Database.HaskRel.Support
+import Database.HaskRel.Order
+
+import SuppliersPartsDB.Definition
+import SuppliersPartsDB.Default
+
+-- To make a few type signatures prettier, and to use HList constructors
+-- directly, instead of "relation"/"relation'"
+import Data.Set ( Set, fromList )
+
+makeLabels6 ["pnoRel","pq","sn","pn","x","y","nc","nw","qtys"]
+
+recreate = do
+  putStrLn $ "\nRecreating database at "++ dbPath
+  assign s s'
+  assign sp sp'
+  assign p p'
+  putStrLn "\nDone."
+
+
+main = do
+  recreate
+  putStrLn $ "\n"++ show s
+  pt$ s
+  putStrLn $ "\n"++ show p
+  pt$ p
+  putStrLn $ "\n"++ show sp
+  pt$ sp
+  snrt2ndExamples
+
+
+r1 = relation [rTuple (sno .=. "S2", pno .=. "P1"),
+               rTuple (sno .=. "S2", pno .=. "P2"),
+               rTuple (sno .=. "S3", pno .=. "P2"),
+               rTuple (sno .=. "S4", pno .=. "P2"),
+               rTuple (sno .=. "S4", pno .=. "P4"),
+               rTuple (sno .=. "S4", pno .=. "P5")]
+
+r4 = relation [rTuple (sno .=. "S2", pnoRel .=. relation [pno .=. "P1" .*. emptyRecord, pno .=. "P2"  .*. emptyRecord]),
+               rTuple (sno .=. "S3", pnoRel .=. relation [pno .=. "P2" .*. emptyRecord]),
+               rTuple (sno .=. "S4", pnoRel .=. relation [pno .=. "P2" .*. emptyRecord, pno .=. "P4" .*. emptyRecord, pno .=. "P5" .*. emptyRecord])]
+
+
+-- TODO: This should be a relvar, check that RVAs work for them.
+spq = relation [rTuple (sno .=. "S5", sName .=. "Adams", status .=. 30, city .=. "Athens", pq .=. relation []),
+                rTuple (sno .=. "S1", sName .=. "Smith", status .=. 20, city .=. "London", pq .=. relation [rTuple (pno .=. "P1", qty .=. 300), rTuple (pno .=. "P2", qty .=. 200), rTuple (pno .=. "P3", qty .=. 400), rTuple (pno .=. "P4", qty .=. 200), rTuple (pno .=. "P5", qty .=. 100), rTuple (pno .=. "P6", qty .=. 100)]),
+                rTuple (sno .=. "S2", sName .=. "Jones", status .=. 10, city .=. "Paris", pq .=. relation [rTuple (pno .=. "P1", qty .=. 300), rTuple (pno .=. "P2", qty .=. 400)]),
+                rTuple (sno .=. "S3", sName .=. "Blake", status .=. 30, city .=. "Paris", pq .=. relation [rTuple (pno .=. "P2", qty .=. 200)]),
+                rTuple (sno .=. "S4", sName .=. "Clark", status .=. 20, city .=. "London", pq .=. relation [rTuple (pno .=. "P2", qty .=. 200), rTuple (pno .=. "P4", qty .=. 300), rTuple (pno .=. "P5", qty .=. 400)])]
+
+-- | "undefined" is used liberally enough that a concise alias for it is convenient.
+ü = undefined
+
+-- | As assumed on page 116
+pX = p `extendA` (\[pun|weight|] -> status .=. ( floor ( weight / 4 ) * 10 ))
+
+-- | Examples from pp. 108-167 of SQL and Relational Theory 2nd Edition.
+snrt2ndExamples = do
+{- Note that there are many redundant brackets here, either to help make certain
+expressions more akin to the Tutorial D expressions they are based on, or just
+to make them slightly more explicit. -}
+  putStrLn "108"
+  rPrint$ ( p `nJoin` s ) `restrict` (\[pun|pName sName|] -> pName > sName )
+--
+  putStrLn "\n110"
+  rPrint$ p `restrict` (\[pun|weight|] -> weight < 17.5)
+--
+  putStrLn "\n111"
+  rPrint$ p `project` (rHdr (color, city))
+--
+  putStrLn "\n113"
+  rPrint$ ( p `projectAllBut` (rHdr (city))) `times` ( s `projectAllBut` (rHdr (city)) )
+--
+  putStrLn "\n116"
+  rPrint$ ( pX `project` (rHdr (status, city)) ) `union` ( s `project` (rHdr (city, status)) )
+  -- See function "shouldFail" below for expression on page 117
+--
+  putStrLn "\n118"
+  rPrint$ ( pX `project` (rHdr (status, city)) ) `intersect` ( s `project` (rHdr (city,status)) )
+  rPrint$ ( pX `project` (rHdr (status, city)) ) `minus` ( s `project` (rHdr (city,status)) )
+--
+  putStrLn "\n119"
+  rPrint$
+    let r1 = ( renameA s (sno `as` (Label :: Label "sa")) ) `project` (ü :: Labels '["sa", "sno"])
+        r2 = ( renameA s (sno `as` (Label :: Label "sb")) ) `project` (ü :: Labels '["sb", "sno"])
+        r3 = r1 `nJoin` r2
+        r4 = r3 `restrict` (\[pun|sa sb|] -> sa < sb)
+     in r4 `project` (ü :: Labels '["sa", "sb"])
+--
+  putStrLn "\n122"
+  rPrint$ ( renameA s (city `as` (Label :: Label "sCity"))
+            `times`
+            renameA p (city `as` (Label :: Label "pCity")) )
+          `restrict` (\[pun|sCity pCity|] -> sCity ≠ pCity)
+--
+  putStrLn "\n123"
+  rPrint$ ( s `nJoin` sp ) `restrict` (\[pun|pno|] -> pno == "P2") `projectAllBut` (rHdr (pno))
+  -- TODO: Expressions for the exercises for chapter 6, page 127-130
+--
+  putStrLn "\n132"
+  rPrint$ ( pX `project` (rHdr (status, city)) ) `xUnion` ( s `project` (rHdr (city,status)) )
+--
+  putStrLn "\n133"
+  rPrint$ s `matching` sp
+  rPrint$ s `notMatching` sp
+  rPrint$ extend p (\[pun|weight|] -> (Label::Label "gmwt") .=. weight * 454 .*. emptyRecord)
+--
+  putStrLn "\n134"
+  rPrint$ ( ( extend p
+              (\[pun|weight|] -> (Label::Label "gmwt") .=. weight * 454 .*. emptyRecord))
+            `restrict` (\[pun|gmwt|] -> gmwt > 7000) )
+              `project` (ü :: Labels '["pno", "gmwt"])
+--
+  putStrLn "\n136"
+{-
+A bit of an issue: relvars are as of now not usable inside the function that
+restrict or extend takes, so they have to be manually read with readRelvar
+
+Also, I use "!!" to denote the image relation function in this case just to show
+how that will have to look in Haskell, but since that has to be enclosed in
+parenthesis I'll instead use "ii" below, which will work as a prefix operator
+since it starts with an alphabetic character (and kinda looks like !! upside
+down).
+-}
+  rPrint$ do spx <- readRelvar sp
+             px <- readRelvar p
+             s `restrict` (\( image -> (!!) ) ->
+                            ( ((!!)spx) `project` (rHdr (pno)) )
+                              == ( px `project` (rHdr (pno)) ) )
+{- The above example uses view patterns to make sure that the expression part of
+the lambda is specified as in Tutorial D. Alternatively, one could use the tuple
+directly and employ the "image" function on that: -}
+{-
+  rPrint$ do spx <- readRelvar sp
+             px <- readRelvar p
+             s `restrict` (\t ->
+                            ( (t `image` spx) `project` (rHdr (pno)) )
+                              == px `project` (rHdr (pno)) )
+-}
+-- This is necessary when using it against multiple relations of different types,
+-- since the former form locks it to a specific argument type.
+--
+
+  putStrLn "\n137"
+-- Note how the variable sno overrides the defined label sno, which is worked
+-- around by using the constructor _sno instead. Another alternative would be
+-- (Label::Label "sno") .=. sno.
+  rPrint$ do spx <- readRelvar sp
+             px <- readRelvar p
+             s `restrict` (\[pun|sno|] ->
+                             ( ( spx `matching` ( relation [rTuple (_sno sno)] ) )
+                               `project` (rHdr (pno)) )
+                             == px `project` (rHdr (pno)))
+  -- Skipping pp. 138-139 and DIVIDE since it's not implemented in HaskRel, see
+  -- below for the image relation formulation.
+--
+  putStrLn "\n140"
+  -- Just like with lambdas non-relational expressions don't work with direct
+  -- relvars. Here the result of the operation is bound to a variable...
+  do n <- count s
+     putStrLn $ show n
+  -- ... or readRelvar s could be bound and an expression that takes the
+  -- relation value can be used:
+  do s' <- readRelvar s
+     putStrLn $ show $ count (s' `project` (ü :: Labels '["status"]))
+  -- But note: Both "count s" and "count (s `project` (ü :: Labels
+  -- '["status"]))" work just fine in GHCi, without any do block or similar (in
+  -- contrast with lambda expressions).
+  putStrLn "1."
+  -- Another similar issue: While "agg"/"aggU" supports types similar to "IO
+  -- [Integer]", "sum", of course, does not
+  do spx <- readRelvar sp
+     putStrLn $ show $ sum $ agg qty spx
+  putStrLn "2."
+  do qtys <- aggU ( sp `project` (ü :: Labels '["qty"]) )
+     putStrLn $ show $ sum qtys
+  putStrLn "3."
+  -- "agg" is a touch more specialized than Tutorial D's "agg op"s, but lists of
+  -- values are trivial to manipulate in Haskell:
+  do qtys <- agg qty sp
+     putStrLn $ show $ avg $ map (3*) qtys
+--
+  putStrLn "\n143"
+  do spx <- readRelvar sp
+     putStrLn $ show $ sum $ agg qty $ spx `restrict` (\[pun|sno|] -> sno == "S5")
+--
+  putStrLn "\n144-145"
+  putStrLn "1:"
+  do spx <- readRelvar sp
+     rPrint$ s `restrict` (\( image -> ii ) ->
+                            ( sum $ agg qty (ii spx) ) < 1000)
+  do spx <- readRelvar sp
+     rPrint$ s `restrict` (\[pun|sno|] ->
+                            ( sum $ agg qty $ spx `matching` ( relation [rTuple ((Label::Label "sno") .=. sno)] ) ) < 1000)
+  putStrLn "2:"
+  do spx <- readRelvar sp
+     rPrint$ s `restrict` (\( image -> ii ) -> ( count (ii spx) ) < 3)
+  putStrLn "3:"
+  -- Because QTY is defined to be an integer, Haskell requires a bit more
+  -- explicit plumbing to multiply it by 0.5 and to compare the result
+  do spx <- readRelvar sp
+     rPrint$ s `restrict` (\( image -> ii ) ->
+                           ( toRational $ minx ( agg qty (ii spx) ) 0 )
+                             <
+                             0.5 * ( toRational $ maxx ( agg qty (ii spx) ) 0 ))
+{-
+  -- Alternatively:
+  do spx <- readRelvar sp
+     rPrint$ s `restrict` (\( image -> ii ) ->
+                           2 * ( minx ( agg qty (ii spx) ) 0 )
+                             <
+                             ( maxx ( agg qty (ii spx) ) 0 ) )
+-}
+  putStrLn "4:"
+  -- See function "updates" below for 5.
+  -- TODO: Fix this after rename has been improved
+  do spx <- readRelvar sp
+     rPrint$ sp `restrict` (\( image -> ii ) ->
+                            count ( ii $ renameA (renameA spx (sno `as` sn)) (pno `as` pn) )
+                            > 2)
+-- See "updates" function below for example 5
+-- TODO: Summarization. Since it's a special case of extension, image relations,
+-- and aggregation it's not a major priority
+--
+  putStrLn "\n152"
+  rPrint$ group r1 (rHdr (pno)) (pnoRel .=.)
+  rPrint$ r4 `ungroup` (ü :: Label "pnoRel")
+  putStrLn$ show $ ( group r1 (rHdr (pno)) (pnoRel .=.) ) == relRearrange r4
+  putStrLn$ show $ r4 `ungroup` (ü :: Label "pnoRel") == relRearrange r1
+--
+  putStrLn "\n154 (using pt instead of rPrint here to show the attribute types)"
+  pt$ do spx <- readRelvar sp
+         extend s (\( image -> ii ) -> pq .=. (ii spx) .*. emptyRecord)
+--
+  putStrLn "\n155"
+  rPrint$ ( spq `ungroup` (ü :: Label "pq") ) `restrict` (\[pun|pno|] -> pno == "P2") `project` (rHdr (sno))
+  rPrint$ spq `restrict` (\[pun|sno|] -> sno == "S2") `ungroup` (ü :: Label "pq") `project` (rHdr (sno))
+  rPrint$ sp `restrict` (\[pun|pno|] -> pno == "P2") `project` (rHdr (sno))
+  rPrint$ sp `restrict` (\[pun|sno|] -> sno == "S2") `project` (rHdr (pno))
+-- TODO: putStrLn "\n156"; Insert and update examples in function "updates"
+-- below, requires spq as a relvar. See above for the query involving an image
+-- relation.
+  putStrLn "\n157"
+  rPrint$
+    do spx <- readRelvar sp
+       px  <- readRelvar p
+       let r1 = extendA s  (\( image -> ii ) -> x .=. (ii spx `project` (rHdr (pno))))
+           r2 = extendA r1 (\_               -> y .=. (px `project` (rHdr (pno))))
+        in
+           r2 `restrict` (\[pun|x y|] -> x == y)
+  -- TODO: Relation valued aggregate operators.
+--
+  putStrLn "\n158"
+  rPrint$
+    p `restrict` (\[pun|city|] -> city == "Paris")
+      `extendA` (\_ -> city .=. "Nice")
+      `extendA` (\[pun|weight|] -> _weight $ 2 * weight)
+  -- Equivalent query that does not rely on extend's behavior of replacing attributes:
+  rPrint$
+    let r1 = p `restrict` (\[pun|city|] -> city == "Paris")
+        r2 = r1 `extendA` (\_ -> nc .=. "Nice" ) `extendA` (\[pun|weight|] -> nw .=. weight * 2)
+        r3 = r2 `projectAllBut` (rHdr (city,weight))
+     in ( r3 `rename` nAs ((nc `as` city),(nw `as` weight)) )
+{-
+The examples on the bottom of page 158 and top of 159 would be expressed as
+follows in GHCi:
+
+*SuppliersPartsExample> let s1 = p `restrict` (\[pun|city|] -> city == "Paris" )
+*SuppliersPartsExample> let s2 = ( p `restrict` (\[pun|city|] -> city == "Paris" ) ) `extendA` (\_ -> city .=. "Nice" ) `extendA` (\[pun|weight|] -> (Label::Label "weight") .=. weight * 2)
+*SuppliersPartsExample> p ≔ ( p `minus` s1 ) `union` s2
+-}
+-- Pages 159-163: Recursion. TODO: On hold.
+--
+  putStrLn "\n163"
+-- TODO: rtlPrint/rtlPrintTyped (r-tuple-list-print), to give a tabular
+-- representation of a tuple list.
+  putStrLn $ show $ (s' `matching` sp') `orderOn` (\[pun|sno|] -> Asc sno)
+-- TODO: Exercises for chapter 7 on pages 164-167
+
+
+updates = do
+  putStrLn "145"
+  putStrLn "5, update of s"
+  putStrLn "Pre update"
+  rPrint$ s
+  do spx <- readRelvar sp
+     update s
+            (\( image -> ii ) -> ( sum $ agg qty (ii spx) ) < 1000)
+            (\[pun|status|] -> _status (floor $ 0.5 * toRational status) .*. emptyRecord)
+  putStrLn "Post update"
+  rPrint$ s
+
+shouldFail = do
+  putStrLn "117"
+  rPrint$ (s `project` rHdr city)
+          `dUnion`
+          (p `project` rHdr city)
+
+
+myFun spx ( image -> ii ) = ( sum $ agg qty (ii spx) ) < 1000
+
diff --git a/examples/Terminology.hs b/examples/Terminology.hs
new file mode 100644
--- /dev/null
+++ b/examples/Terminology.hs
@@ -0,0 +1,47 @@
+{-# LANGUAGE DataKinds #-}
+
+module Terminology where
+
+import HaskRel.RDBMS
+import Data.HList.CommonMain ( Tagged, Label (Label) )
+
+type Haskell = Tagged "haskell" String
+type RelModel = Tagged "relModel" String
+type SQL = Tagged "sql" String
+type HaskRel = Tagged "haskRel" String
+
+haskell = Label::Label "haskell"
+relModel = Label::Label "relModel"
+sql = Label::Label "sql"
+haskRel = Label::Label "haskRel"
+
+type Terms = Relation '[Haskell, RelModel, HaskRel, SQL]
+
+{-| Terms as they appear in Haskell, relational theory, HaskRel and SQL. Both
+terms defined in the various systems of computations and terms used in writings
+to describe it are included ("function" et. al. being an example of the latter),
+the the former capitalized and the latter in lower case. Haskell terms are given
+qualified when standing alone, and unqualified when used together. The RelModel
+attribute shows the terms as understood from SQL and the Relational Model, 2nd
+ed.
+
+Additionally, the when referring to the type itself of "Record a" and "Set (
+Record a )" the term "heading" is used in relational theory, and "row type" or
+"composite type" in SQL.
+-}
+terms = relation' [
+  ("Data.Tagged.Tagged", "attribute", "Attr", "field, column"),
+  ("Data.HList.Record.Record", "tuple", "RTuple", "row"),
+  ("Set (Record a)", "relation", "Relation a", "table"),
+  ("FilePath (Set (Record a))", "relvar", "Relvar a", "table"),
+  ("Data.HList.Record.Label", "attribute name", "Label", "field name, column name"),
+  ("Data.HList.Record.Labels", "attribute name set", "Labels", "list of field/column names"),
+  ("function, operator", "operator", "function", "operator, function, procedure, routine, method")]
+        :: Terms
+
+{- Other ideas:
+  ("let", "≝", "let", "N/A"),
+  ("let a in b", "WITH a : b ", "let a in b", "WITH a b"),
+  (".=.", ":= (attribute)", ".=.", "="),
+  ("N/A", ":= (relvar)", "assign, ≔", "N/A")
+-}
diff --git a/examples/algebraExample.sh b/examples/algebraExample.sh
new file mode 100644
--- /dev/null
+++ b/examples/algebraExample.sh
@@ -0,0 +1,2 @@
+# TODO: Make directory independent, cd must now be "HaskRel/examples"
+ghci -i../src -XDataKinds -XViewPatterns -XKindSignatures -XQuasiQuotes -XViewPatterns AlgebraExample $@
diff --git a/examples/suppliersPartsDB.sh b/examples/suppliersPartsDB.sh
new file mode 100644
--- /dev/null
+++ b/examples/suppliersPartsDB.sh
@@ -0,0 +1,2 @@
+# TODO: Make directory independent, cd must now be "HaskRel/examples"
+ghci -i../src -XDataKinds -XKindSignatures -XQuasiQuotes -XViewPatterns -XScopedTypeVariables SuppliersPartsExample $@
diff --git a/src/Database/HaskRel/FWTabulation.hs b/src/Database/HaskRel/FWTabulation.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/HaskRel/FWTabulation.hs
@@ -0,0 +1,137 @@
+{-|
+Module      : FWTabulation
+Description : Presentation of tables in a two-dimensional fixed-width font form.
+Copyright   : © Thor Michael Støre, 2015
+License     : GPL v2 without "any later version" clause
+Maintainer  : thormichael át gmail døt com
+Stability   : experimental
+
+Presentation of tables in a two-dimensional fixed-width font form.
+-}
+module Database.HaskRel.FWTabulation (
+  -- * Presentation functions
+  present1LineValue, presentNLineValue,
+  -- * Utility functions
+  maxLen, padTranspose ) where
+
+import Data.List ( intercalate )
+
+-- | Given two lists of orderables, produces a list of equal length where each element is that which is the maximum of those elements that are in the same position in the two input lists.
+maxLen :: Ord b => [b] -> [b] -> [b]
+maxLen = zipWith max
+
+
+buildOneColumn :: Int -> String -> String -> String
+buildOneColumn hPad a str = str ++ a ++ concat ( replicate ( hPad - length a ) " " )
+
+buildColumns :: [Int] -> [String] -> String
+buildColumns [] [] = ""
+buildColumns [p] [t] = buildOneColumn p t ""
+buildColumns (p:ps) (t:ts) = buildColumns' (p:ps) (t:ts) ""
+
+buildColumns [] [t] = buildOneColumn 0 t ""
+buildColumns [] (t:ts) = buildColumns' [] (t:ts) ""
+
+buildColumns [p] [] = buildOneColumn p "" "Internal Error: "
+buildColumns (p:ps) [] = buildColumns' (p:ps) [] ""
+
+buildColumns' :: [Int] -> [String] -> String -> String
+buildColumns' [] [] str = str
+buildColumns' [p] [t] str = buildOneColumn p t str
+buildColumns' (p:ps) (t:ts) str = buildColumns' ps ts $ buildOneColumn p t str ++ " │ "
+
+-- These error messages stem from before HList was used and a less disciplined form was used instead, they should be impossible to trigger today barring the introduction of bugs.
+-- These are pure presentation functions, so it's okay to just inform of the error rather than programmatically signaling it
+buildColumns' [] [t] str = str ++ "Internal Error: " ++ t
+buildColumns' [] (t:ts) str = str ++ "Internal Error: " ++ intercalate " │ " (t:ts)
+
+buildColumns' [p] [] str = str ++ "Internal Error: " ++ show p
+buildColumns' (p:ps) [] str = str ++ "Internal Error: " ++ intercalate " │ " ( map show $ p:ps )
+
+
+-- | Gets the maximum length of each column of a value consisting of a header and a single line
+colWidths ::
+  (Foldable t, Foldable t1) =>
+  [[t1 a1]] -> [t a] -> [Int]
+colWidths l hdr = foldl1 maxLen [ map length hdr, allColWidths l ]
+
+-- | Gets the width of the columns of a value in when presented in a columnar format.
+allColWidths :: Foldable t => [[t a]] -> [Int]
+allColWidths = map $ maximum . map length
+
+-- | Gets the maximum length of each column of a value consisting of a header and zero or more lines
+nColWidths :: (Foldable t, Foldable t1) => [[[t1 a1]]] -> [t a] -> [Int]
+nColWidths ll hdr = foldl1 maxLen $ map length hdr : mapListLen ll
+
+mapListLen :: Foldable t => [[[t a]]] -> [[Int]]
+mapListLen = map allColWidths
+
+-- See also: http://en.wikipedia.org/wiki/Box-drawing_character
+-- | Builds a one-line representation of a value, plus header
+present1LineValue :: [[String]] -> [String] -> [String]
+present1LineValue strRep header =
+  let hPad = colWidths strRep header
+   in
+  [ "┌─" ++ hPadTable hPad "─" "─┬─" ++ "─┐",
+    "│ " ++ buildColumns hPad header ++ " │",
+    "├─" ++ hPadTable hPad "─" "─┼─" ++ "─┤"]
+ ++ buildRow hPad strRep ++
+  [ "└─" ++ hPadTable hPad "─" "─┴─" ++ "─┘"]
+
+-- | Builds a multi-line representation of a value, plus header
+presentNLineValue :: [[[String]]] -> [String] -> [String]
+presentNLineValue strRepList' hdr =
+  let
+    hPad = nColWidths strRepList' hdr
+  in
+    [ "┌─" ++ hPadTable hPad "─" "─┬─" ++ "─┐",
+      "│ " ++ buildColumns hPad hdr ++ " │",
+-- Classic double-line for candidate key, doesn't always display correctly:
+      "╞═" ++ hPadTable hPad "═" "═╪═" ++ "═╡" ]
+-- Strong line for candidate key, also doesn't always display correctly:
+--      "┝━" ++ hPadTable hPad "━" "━┿━" ++ "━┥" ]
+-- No indication of candidate key, seems to work in more cases:
+--      "├─" ++ hPadTable hPad "─" "─┼─" ++ "─┤"]
+   ++ foldr (\a b -> buildRow hPad a ++ b ) [] strRepList' ++ 
+    [ "└─" ++ hPadTable hPad "─" "─┴─" ++ "─┘" ]
+
+buildRow :: [Int] -> [[String]] -> [String]
+buildRow hPad strRep = buildRow' hPad $ padTranspose strRep
+
+buildRow' :: [Int] -> [[String]] -> [String]
+buildRow' _ [] = ["│  │"]
+buildRow' hPad [strRep] = ["│ " ++ buildColumns hPad strRep ++ " │"]
+buildRow' hPad (strRep:strRepX) = ( "│ " ++ buildColumns hPad strRep ++ " │" ) : buildRow' hPad strRepX
+
+
+-- | Transposes a list of lists of lists, padding the lists of the second dimension with empty lists if they are shorter than the other rows.
+padTranspose :: [[[t]]] -> [[[t]]]
+padTranspose x = padTranspose' x ( maximum ( map length x ) - 1 )
+
+padTranspose' :: [[[t]]] -> Int -> [[[t]]]
+padTranspose' [] _ = []
+padTranspose' ([] : xss) l = padTranspose' xss ( l - 1 )
+padTranspose' ((x:xs) : xss) l = (x : map next xss) : padTranspose' (rPad l xs : map rest xss) ( l - 1 )
+
+--next :: (Monoid a) => [a] -> a
+-- | Gives the head of the argument, or the empty list if the argument is empty.
+next :: [[t]] -> [t]
+next [] = []
+next xs = head xs
+
+--rest :: (Monoid a) => [a] -> [a]
+-- | Gives the tail of the argument, or the empty list if the argument is empty.
+rest :: [t] -> [t]
+rest [] = []
+rest xs = tail xs
+
+rPad :: Int -> [[t]] -> [[t]]
+rPad m xs = xs ++ replicate ( m - length xs ) []
+
+hPadColumn :: Int -> [a] -> [a]
+hPadColumn x fillChar = concat ( replicate x fillChar )
+
+hPadTable :: [Int] -> String -> String -> String
+hPadTable [] _ _ = ""
+hPadTable [x] fillChar _ = hPadColumn x fillChar
+hPadTable (x:xs) fillChar divChar = hPadColumn x fillChar ++ divChar ++ hPadTable xs fillChar divChar
diff --git a/src/Database/HaskRel/HFWTabulation.hs b/src/Database/HaskRel/HFWTabulation.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/HaskRel/HFWTabulation.hs
@@ -0,0 +1,334 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses, UndecidableInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE DataKinds #-}
+
+-- TODO: Can this be rewritten to be less reliant on Data.Typeable? Should be possible to just use it for getting the field type names, and not for parsing the entire type.
+-- TODO: Check that nothing is missing from the export list; only HaskRel's dependencies are known to be covered.
+-- TODO: New functions that did a tiny bit more than the last ones have been added haphazardly, clean up this and the users of this.
+
+{-|
+Module      : HFWTabulation
+Description : Presentation of HList values in a two-dimensional fixed-width font form.
+Copyright   : © Thor Michael Støre, 2015
+License     : GPL v2 without "any later version" clause
+Maintainer  : thormichael át gmail døt com
+Stability   : experimental
+
+HList fixed-width tabular presentation. Presentation of HList values in a two-dimensional, tabular fixed-width font form with a header consisting of labels and optionally types. Only records are supported by this module, see `TIPFWTabulation` for support for TIPs.
+-}
+module Database.HaskRel.HFWTabulation (
+  HFWPresent ( hfwPrint, hfwPrintTyped, hfwPrintTypedTS ),
+  FWPresent ( fwPresent, fwPresentTyped ),
+  FWPresent' ( fwPresent', fwPresentTyped' ),
+  printHRecSetTab, printHRecSetTabTyped, printHRecSetTabTypedTS,
+  showHRecSetTab,
+  showTR, showTRTS, showHTypeTS, showHListSetType,
+  HFWTIPSet, HFWTIP, HFWRec, HFWString, HFWOther,
+  HListTypeSynonym ( hRecTS, hRecSetTS, hTIPTS, hTIPSetTS ), FWPPred,
+  HPresentRecAttr(HPresentRecAttr), HPresentTypedRecAttr(HPresentTypedRecAttr)
+  ) where
+
+import Data.HList.CommonMain
+
+import Data.Typeable
+
+import Data.Set ( Set, toList )
+import Data.List ( intercalate )
+
+import Database.HaskRel.FWTabulation
+
+
+-- Presentation of table heading
+
+-- data HFWTIPList -- <- TODO. Use ↑ to distinguish them from sets? Not really appropriate, it's not known to be ordered. [] in some fashion?
+data HFWTIPSet
+data HFWTIP
+-- data HFWRecList -- <- TODO
+data HFWRecSet
+data HFWRec
+data HFWString
+data HFWOther
+
+type family FWPPred a where
+--    FWPPred [ Record a ] = HFWRecList
+    FWPPred ( Set ( Record a ) ) = HFWRecSet
+    FWPPred ( Record a )         = HFWRec
+--    FWPPred [ ( TIP a ) ]    = HFWTIPList
+    FWPPred ( Set ( TIP a ) )    = HFWTIPSet
+    FWPPred ( TIP a )            = HFWTIP
+    FWPPred String               = HFWString
+    FWPPred a                    = HFWOther
+
+
+-- As having no type synonyms in effect
+data EmptyTS = EmptyTS
+
+-- | Type synoyms used when building the table header with type names
+class HListTypeSynonym s where
+  hRecTS :: s -> String
+  hRecSetTS :: s -> String
+  hTIPTS :: s -> String
+  hTIPSetTS :: s -> String
+
+-- TODO: This only supports showing a single type synonym, it doesn't support showing "Set ( TIP '[Foo] )", for instance. This is sufficient for HaskRel, which only uses full type synonyms, for instance "Relation '[Foo]".
+instance HListTypeSynonym EmptyTS where
+  hRecTS _ = "Record"
+  hRecSetTS _ = "Set-Record"
+  hTIPTS _ = "TIP"
+  hTIPSetTS _ = "Set-TIP"
+
+
+-- | Show a TypeRep
+showTR :: TypeRep -> String
+showTR = showTRTS EmptyTS
+
+-- TODO: Record presentation is copy'n'paste of TIP presentation, which gives the unfortunate 'Record '["foo"]'
+-- | Show a TypeRep, using the given type synonyms
+showTRTS :: HListTypeSynonym ts => ts -> TypeRep -> String
+showTRTS ts t
+  | t == stringType   = "String"
+  | tyCon == recTyCon = hRecTS ts ++ showHListType app
+  | tyCon == tipTyCon = hTIPTS ts ++ showHListType app
+  | tyCon == setTyCon && typeRepTyCon ( head app ) == recTyCon =
+      hRecSetTS ts ++ showHListType ( typeRepArgs $ head app )
+  | tyCon == setTyCon && typeRepTyCon ( head app ) == tipTyCon =
+      hTIPSetTS ts ++ showHListType ( typeRepArgs $ head app )
+  | otherwise         = show t
+  where
+    ( tyCon, app ) = splitTyConApp t
+    stringType = typeRep ( Proxy :: Proxy String )
+    -- The argument to Set could be anything that is an instance of Typeable
+    setTyCon = typeRepTyCon $ typeRep ( Proxy :: Proxy ( Set Int ) )
+    -- listTyCon = ...
+    recTyCon = typeRepTyCon $ typeRep ( Proxy :: Proxy ( Record '[] ) )
+    tipTyCon = typeRepTyCon $ typeRep ( Proxy :: Proxy ( TIP '[] ) )
+
+showHListSetType :: forall a (r :: [*] -> *) .
+    ( Typeable r, Typeable a ) =>
+    Set (r a) -> String
+showHListSetType = showHListType . typeRepArgs . head . typeRepArgs . typeOf
+
+showHListType :: [TypeRep] -> String
+showHListType = (++) " '" . show . hListTypeToTRList
+
+hListTypeToTRList :: [TypeRep] -> [TypeRep]
+hListTypeToTRList = parseHListType . typeRepArgs . head
+
+parseHListType :: [TypeRep] -> [TypeRep]
+parseHListType [] = []
+parseHListType [_] = error "Not a valid TIP/Record type" -- Always come in pairs. Will also fail here if it's not tagged
+parseHListType (tr:trx) = head ( typeRepArgs tr ) : parseHListType ( typeRepArgs $ head trx )
+
+
+-- Meta information
+
+tagFName :: TypeRep -> String
+tagFName = tail . init . show . head . typeRepArgs
+
+{-|
+>>> hRecFNames $ sno .=. "S1" .*. status .=. 10 .*. emptyRecord
+["sno","status"]
+-}
+hRecFNames :: Typeable a => a -> [String]
+hRecFNames = map tagFName . flatHRec
+
+tagQFName :: TypeRep -> String
+tagQFName = tagQFNameTS EmptyTS
+
+tagQFNameTS :: HListTypeSynonym ts => ts -> TypeRep -> String
+tagQFNameTS ts a = tagFName a ++ " :: " ++ showHTypeTS ts a
+
+{-|
+>>> hRecQFNames $ sno .=. "S1" .*. status .=. 10 .*. emptyRecord
+["sno :: String","status :: Integer"]
+-}
+hRecQFNames :: Typeable a => a -> [String]
+hRecQFNames = map tagQFName . flatHRec
+
+hRecQFNamesTS :: ( HListTypeSynonym ts, Typeable a ) => ts -> a -> [String]
+hRecQFNamesTS ts = map ( tagQFNameTS ts ) . flatHRec
+
+showHTypeTS :: HListTypeSynonym ts => ts -> TypeRep -> String
+showHTypeTS ts = showTRTS ts . head . tail . typeRepArgs
+
+
+{-
+>>> typeOf $ sno .=. "S1" .*. status .=. 10 .*. emptyRecord
+Record (: * (Tagged Symbol "sno" [Char]) (: * (Tagged Symbol "status" Integer) []))
+>>> flatHRec $ sno .=. "S1" .*. status .=. 10 .*. emptyRecord
+[Tagged Symbol "sno" [Char],Tagged Symbol "status" Integer]
+-}
+-- I did this before noticing hEnd, would that in the right location work just as well?
+-- TODO: Rewrite to use typeRep and Proxy. (This probably goes for other places too.)
+flatHRec :: Typeable a => a -> [TypeRep]
+flatHRec = flatHRec' . typeRepArgs . head . typeRepArgs . typeOf
+
+flatHRec' :: [TypeRep] -> [TypeRep]
+flatHRec' [] = []
+flatHRec' [m] = [m]
+flatHRec' (m:mx) = m : flatHRec' ( typeRepArgs $ head mx )
+
+
+-- Presentation
+
+class HFWPresent r where
+    hfwPrint :: r -> IO ()
+    hfwPrintTyped :: r -> IO ()
+    hfwPrintTyped = hfwPrintTypedTS EmptyTS
+    hfwPrintTypedTS :: HListTypeSynonym ts => ts -> r -> IO ()
+
+class Show a => FWPresent a where
+    fwPresent      :: a -> [String]
+    fwPresentTyped :: a -> [String]
+
+class Show a => FWPresent' flag a where
+    fwPresent'      :: flag -> a -> [String]
+    fwPresentTyped' :: flag -> a -> [String]
+
+
+-- Presentation of a non-HList value
+
+instance (FWPPred a ~ flag, FWPresent' flag a) => FWPresent a where
+    fwPresent      = fwPresent' ( undefined :: flag )
+    fwPresentTyped = fwPresentTyped' ( undefined :: flag )
+
+instance Show a => FWPresent' HFWOther a where
+    fwPresent' _ x      = [show x]
+    fwPresentTyped' _ x = [show x]
+
+instance FWPresent' HFWString String where
+    fwPresent' _ x      = [x]
+    fwPresentTyped' _ x = [x]
+
+
+-- Presentation of a single record
+
+buildHRec
+  :: (Typeable r, RecordValues r,
+      HFoldr (Mapcar HPresentRecAttr) [[String]] (RecordValuesR r) [[String]]) =>
+     Record r -> [String]
+buildHRec rrTup = present1LineValue ( listPresentRec rrTup ) ( hRecFNames rrTup )
+
+buildHRecTyped
+  :: (Typeable r, RecordValues r,
+      HFoldr (Mapcar HPresentTypedRecAttr) [[String]] (RecordValuesR r) [[String]]) =>
+     Record r -> [String]
+buildHRecTyped rrTup = present1LineValue ( listPresentTypedRec rrTup ) ( hRecQFNames rrTup )
+
+buildHRecTypedTS
+  :: (HListTypeSynonym ts, Typeable r, RecordValues r,
+      HFoldr (Mapcar HPresentTypedRecAttr) [[String]] (RecordValuesR r) [[String]]) =>
+     ts -> Record r -> [String]
+buildHRecTypedTS ts rrTup = present1LineValue ( listPresentTypedRec rrTup ) ( hRecQFNamesTS ts rrTup )
+
+listPresentRec :: (RecordValues r,
+      HFoldr (Mapcar HPresentRecAttr) [e] (RecordValuesR r) [e]) =>
+     Record r -> [e]
+listPresentRec = hMapOut HPresentRecAttr . recordValues
+
+listPresentTypedRec :: (RecordValues r,
+      HFoldr (Mapcar HPresentTypedRecAttr) [e] (RecordValuesR r) [e]) =>
+     Record r -> [e]
+listPresentTypedRec = hMapOut HPresentTypedRecAttr . recordValues
+
+
+data HPresentRecAttr = HPresentRecAttr
+instance ([String] ~ stringL, FWPresent' (FWPPred a) a) => 
+        ApplyAB HPresentRecAttr a stringL
+    where
+        applyAB _ = fwPresent
+
+data HPresentTypedRecAttr = HPresentTypedRecAttr
+instance ([String] ~ stringL, FWPresent' (FWPPred a) a) => 
+        ApplyAB HPresentTypedRecAttr a stringL
+    where
+        applyAB _ = fwPresentTyped
+
+
+instance (HFoldr (Mapcar HPresentRecAttr) [[String]] (RecordValuesR r) [[String]],
+          HFoldr (Mapcar HPresentTypedRecAttr) [[String]] (RecordValuesR r) [[String]],
+          Typeable r, RecordValues r
+          ) =>
+         HFWPresent ( Record r )
+    where
+        hfwPrint = putStrLn . intercalate "\n" . buildHRec
+        hfwPrintTyped = putStrLn . intercalate "\n" . buildHRecTyped
+        hfwPrintTypedTS ts = putStrLn . intercalate "\n" . buildHRecTypedTS ts
+
+
+instance ( HFoldr (Mapcar HPresentRecAttr) [[String]] (RecordValuesR r) [[String]],
+           HFoldr (Mapcar HPresentTypedRecAttr) [[String]] (RecordValuesR r) [[String]],
+           Typeable r, RecordValues r, ShowComponents r
+         ) =>
+        FWPresent' HFWRec ( Record r )
+  where
+    fwPresent' _      = buildHRec
+    fwPresentTyped' _ = buildHRecTyped
+
+-- Presentation of a set of records
+
+showHRecSetTab ::
+     (Typeable a, RecordValues a,
+      HFoldr (Mapcar HPresentRecAttr) [[String]] (RecordValuesR a) [[String]]) =>
+     Set (Record a) -> String
+showHRecSetTab = intercalate "\n" . buildHRecSet
+
+{-
+showHRecSetTabTyped = intercalate "\n" . buildHRecSetTyped
+showHRecSetTabTypedTS = intercalate "\n" . buildHRecSetTypedTS
+-}
+
+-- | Prints a set of HList records in a table format
+printHRecSetTab a = putStrLn $ intercalate "\n" $ buildHRecSet a
+-- | Prints a set of HList records in a table format, with types in the header
+printHRecSetTabTyped a = putStrLn $ intercalate "\n" $ buildHRecSetTyped a
+-- | Prints a set of HList records in a table format, with types that use the given type synonyms in the header
+printHRecSetTabTypedTS ts a = putStrLn $ intercalate "\n" $ buildHRecSetTypedTS ts a
+
+instance (Typeable a, RecordValues a,
+          HFoldr (Mapcar HPresentRecAttr) [[String]] (RecordValuesR a) [[String]],
+          HFoldr (Mapcar HPresentTypedRecAttr) [[String]] (RecordValuesR a) [[String]]) =>
+      HFWPresent ( Set ( Record a ) ) where
+      hfwPrint = printHRecSetTab
+      hfwPrintTyped = printHRecSetTabTyped
+      hfwPrintTypedTS = printHRecSetTabTypedTS
+
+instance (Typeable a, RecordValues a, ShowComponents a,
+          HFoldr (Mapcar HPresentRecAttr) [[String]] (RecordValuesR a) [[String]],
+          HFoldr (Mapcar HPresentTypedRecAttr) [[String]] (RecordValuesR a) [[String]]) =>
+        FWPresent' HFWRecSet ( Set ( Record a ) )
+  where
+    fwPresent' _      = buildHRecSet
+    fwPresentTyped' _ = buildHRecSetTyped
+
+unwrap :: x (Record a) -> Record a
+unwrap = undefined
+
+buildHRecSet ::
+     (Typeable a, RecordValues a,
+      HFoldr (Mapcar HPresentRecAttr) [[String]] (RecordValuesR a) [[String]]) =>
+     Set (Record a) -> [String]
+buildHRecSet rs =
+  presentNLineValue ( map listPresentRec $ toList rs ) ( hRecFNames $ unwrap rs )
+
+buildHRecSetTyped ::
+     (Typeable a, RecordValues a,
+      HFoldr (Mapcar HPresentTypedRecAttr) [[String]] (RecordValuesR a) [[String]]) =>
+     Set (Record a) -> [String]
+buildHRecSetTyped rs =
+  presentNLineValue ( map listPresentTypedRec $ toList rs ) ( hRecQFNames $ unwrap rs )
+
+buildHRecSetTypedTS
+  :: (Typeable a, RecordValues a,
+      HFoldr
+        (Mapcar HPresentTypedRecAttr)
+        [[String]]
+        (RecordValuesR a)
+        [[String]],
+      HListTypeSynonym ts) =>
+     ts -> Set (Record a) -> [String]
+buildHRecSetTypedTS ts rs =
+  presentNLineValue ( map listPresentTypedRec $ toList rs ) ( hRecQFNamesTS ts $ unwrap rs )
diff --git a/src/Database/HaskRel/Order.hs b/src/Database/HaskRel/Order.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/HaskRel/Order.hs
@@ -0,0 +1,54 @@
+{-# LANGUAGE FlexibleContexts #-}
+
+{-|
+Module      : Database.HaskRel.Order
+Description : Ordering functions
+Copyright   : © Thor Michael Støre, 2015
+License     : GPL v2 without "any later version" clause
+Maintainer  : thormichael át gmail døt com
+Stability   : experimental
+
+Ordering functions. This is not of the relational model.
+-}
+
+module Database.HaskRel.Order (
+  -- * Ordering functions.
+  orderBy, orderOn,
+  Asc(Asc), Desc(Desc)
+  ) where
+
+import Data.Set ( Set, toList )
+import qualified Data.Set
+import Data.List ( sortOn, sortBy )
+import Data.HList.CommonMain
+
+-- import Database.HaskRel.Relational.TIP.Definition
+-- import Data.Ord ( Down(Down) )
+
+{- Converts a relation to an ordered set of r-tuples, ordered ascendingly. Because Data.Set orders its elements (which is a no-no in relational theory and a quality we must disregard in the context of it), and as such functions as an ordered set, this will just rearrange the attributes.
+ordRTupSet ::
+     (Ord (HList l), TagUntagFD a ta, TagUntagFD a1 l,
+      HProject (HList a) (HList a1)) =>
+     Relation' ta -> Relation' l -> Relation' l
+ordRTupSet r _ = Data.Set.map hTIPRearrange r
+TODO: This is TIP specific, figure out if this is neccessary or beneficial at all.
+-}
+
+{-| Takes any set (including that of a relation) and results in a list of the
+elements it consists of ordered by the given predicate
+-}
+orderBy :: Set a -> (a -> a -> Ordering) -> [a]
+orderBy r p = sortBy p $ toList r
+
+{-| Takes any set (including that of a relation) and results in a list of the
+elements it consists of ordered on the given key function
+-}
+orderOn :: Ord b => Set a -> (a -> b) -> [a]
+orderOn r k = sortOn k $ toList r
+
+newtype Asc a = Asc a deriving (Show, Read, Eq, Ord)
+-- As with Data.Ord.Down
+newtype Desc a = Desc a deriving (Show, Read, Eq)
+
+instance Ord a => Ord (Desc a) where
+    compare (Desc x) (Desc y) = y `compare` x
diff --git a/src/Database/HaskRel/RDBMS.hs b/src/Database/HaskRel/RDBMS.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/HaskRel/RDBMS.hs
@@ -0,0 +1,38 @@
+
+{-|
+Module      : Database.HaskRel.RDBMS
+Description : A re-export of the modules that form the HList record based HaskRel library
+Copyright   : © Thor Michael Støre, 2015
+License     : GPL v2 without "any later version" clause
+Maintainer  : thormichael át gmail døt com
+Stability   : experimental
+
+Exports the pertinent parts of HaskRel building on HList records. This gives most features of the relational algebra, relation variable support, HList CommonMain, as well as certain non-relational features such as ordering.
+-}
+
+-- TODO: Should call this something else than RDBMS seeing as it's so far just a DBMS + relational algebra
+module Database.HaskRel.RDBMS (
+  module Data.HList.CommonMain,
+  -- * The relational model of database management: A subset thereof
+  module Database.HaskRel.Relational.Definition,
+  Relvar ( Relvar, relvarPath ), relvarType, readRelvar,
+  module Database.HaskRel.Relational.Expression,
+  module Database.HaskRel.Relational.Unicode,
+  -- * Non-relational features
+  module Database.HaskRel.Order,
+  module Database.HaskRel.Support ) where
+
+-- TODO: Only import relevant parts of HList. Variant, TIPs and TICs aren't required.
+import Data.HList.CommonMain
+import Data.Tagged (Tagged)
+
+-- The relational model, and features defined together with it
+import Database.HaskRel.Relational.Definition
+import Database.HaskRel.Relational.Variable ( Relvar (Relvar), relvarPath, relvarType, readRelvar )
+import Database.HaskRel.Relational.Expression
+import Database.HaskRel.Relational.Unicode
+
+-- Features not of the relational model
+import Database.HaskRel.Order
+import Database.HaskRel.Support
+
diff --git a/src/Database/HaskRel/Relational/Algebra.hs b/src/Database/HaskRel/Relational/Algebra.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/HaskRel/Relational/Algebra.hs
@@ -0,0 +1,862 @@
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeOperators #-}
+
+{-|
+Module      : Algebra
+Description : Relational algebra, including supporting functions
+Copyright   : © Thor Michael Støre, 2015
+License     : GPL v2 without "any later version" clause
+Maintainer  : thormichael át gmail døt com
+Stability   : experimental
+
+Relational algebra based on HList records.
+
+It is important to note that, in order to build a straight forward foundation, this module defines pure functions, viz. they only operate upon relational /values/, not relvars or the result of expressions involving relvars. See "Database.HaskRel.Relational.Expression" for functions that function as conveyed by the relational model, which are the ones that are intended to be used directly.
+
+All the examples in "Database.HaskRel.Relational.Expression" are defined in terms of the relvars s, p and sp; to run the examples in that module with the functions of this module one can use the relation values s', p' and sp' instead. The script examples\/algebraExample.sh starts a GHCi session with the imports and pragmas required to run these examples.
+-}
+module Database.HaskRel.Relational.Algebra (
+  -- * Operators of the relational algebra
+  rename, extend, restrict, project, projectAllBut,
+  naturalJoin, nJoin, times, matching, semiJoin, notMatching, semiDiff,
+  union, dUnion, intersect, minus, xUnion, group, groupAllBut, ungroup,
+  -- * Somewhat deprecated operators of the relational algebra
+  summarize,
+  -- * Additional operators with relational closure
+  interJoin, iJoin, dExtend, aSummarize,
+  imageExtendL, minus_,
+  -- ** Alternative, concise functions
+  extendA, dExtendA, renameA,
+  -- * Supporting functions
+  isProperSubsetOf, isSubsetOf, image, count, isEmpty,
+  -- * Other useful, non-relational associated functions
+  rafoldr, rafoldrU, agg, aggU, relRearrange,
+  -- * Instances
+  NotEmpty, Relabel
+   ) where
+
+-- TODO: See also Database.HaskRel.Relational.TIP.Algebra for TODOs.
+
+import Data.Set ( Set, fromList, toList, size, intersection, difference )
+import qualified Data.Set
+
+import Database.HaskRel.HFWTabulation ( showHRecSetTab, HPresentRecAttr )
+import Database.HaskRel.Relational.Definition ( Relation, unordRecEq, relRearrange )
+
+import Data.HList.CommonMain
+
+import Data.Typeable
+
+
+
+data Relabel tr = Relabel tr
+
+instance (HasFieldM l r v, Label dl ~ (DemoteMaybe (Label l) v),
+          b ~ Tagged dl a) =>
+     ApplyAB (Relabel r) (Tagged l a) b
+  where
+     applyAB _ (Tagged a) = Tagged a
+
+{-| Rename of multiple labels, preserving original order.
+
+>>> let aRecord = ((Tagged 1 :: Tagged "g" Int) .*. (Tagged 2 :: Tagged "a" Int) .*. (Tagged 3 :: Tagged "i" Int) .*. (Tagged 4 :: Tagged "c" Int) .*. (Tagged 5 :: Tagged "e" Int) .*. emptyRecord)
+>>> aRecord
+Record{g=1,a=2,i=3,c=4,e=5}
+>>> rhRenameLabels ((Label::Label "c") .=. (Label::Label "d") .*. (Label::Label "a") .=. (Label::Label "b") .*. emptyRecord) aRecord
+Record{g=1,b=2,i=3,d=4,e=5}
+-}
+rhRenameLabels
+  :: (HLabelSet (LabelsOf r), HMapAux HList (Relabel tr) a r,
+      SameLength' r a, SameLength' a r, HAllTaggedLV r) =>
+     tr -> Record a -> Record r
+rhRenameLabels a (Record r) = mkRecord $ hMap (Relabel a) r
+
+{-
+-- | Alternative implementation of 'rhRenameLabels', building on 'relabeled'.
+rhRenameLabels'
+  :: (RecordValues a, RecordValues a1, HLabelSet (LabelsOf a),
+      HMapAux HList TaggedFn (RecordValuesR a) a1,
+      HMapAux HList TaggedFn (RecordValuesR a1) a,
+      HMapAux HList (Relabel tr) a1 a, SameLength' a a1,
+      SameLength' a (RecordValuesR a1), SameLength' a1 a,
+      SameLength' a1 (RecordValuesR a), SameLength' (RecordValuesR a) a1,
+      SameLength' (RecordValuesR a1) a, HAllTaggedLV a,
+      RecordValuesR a1 ~ RecordValuesR a) =>
+     tr -> Record a1 -> Record a
+rhRenameLabels' _ r = r ^. relabeled
+-}
+
+{-| Rename multiple attributes of a relation.
+
+>>> let pnu = Label :: Label "pnu"
+>>> let colour = Label :: Label "colour"
+>>> rPrint$ p' `rename` nAs( pno `as` pnu, color `as` colour )
+┌─────┬───────┬────────┬────────┬────────┐
+│ pnu │ pName │ colour │ weight │ city   │
+╞═════╪═══════╪════════╪════════╪════════╡
+│ P1  │ Nut   │ Red    │ 12 % 1 │ London │
+...
+-}
+rename
+  :: (Ord (HList r), HLabelSet (LabelsOf r),
+      HMapAux HList (Relabel tr) a r, SameLength' r a, SameLength' a r,
+      HAllTaggedLV r) =>
+     Relation a -> tr -> Relation r
+rename r l = Data.Set.map (rhRenameLabels l) r
+
+-- | Renames a single attribute. See 'Database.HaskRel.Relational.Expression.renameA'
+renameA
+  :: forall l1 v1 r v' v l . (Ord (HExtendR (Tagged l1 v1) (r v')), HasField l (r v) v1,
+      HExtend (Tagged l1 v1) (r v'), HDeleteAtLabel r l v v') =>
+     Set (r v) -> Tagged l (Label l1) -> Set (HExtendR (Tagged l1 v1) (r v'))
+renameA r frto = Data.Set.map (hRenameLabel (Label::Label l) (untag frto)) r
+
+
+{- | Extends the given relation with the r-tuple resulting from the second argument. Existing attributes with the same name will be replaced.
+
+See 'Database.HaskRel.Relational.Expression.extend'.
+-}
+extend
+  :: (Ord (HList (HAppendListR r r'1)),
+      HLabelSet (LabelsOf (HAppendListR r r'1)),
+      HDeleteLabels (LabelsOf r) r' r'1, HAppendList r r'1,
+      HAllTaggedLV (HAppendListR r r'1)) =>
+     Relation r' -> (Record r' -> Record r) -> Relation (HAppendListR r r'1)
+extend r f = Data.Set.map (\t -> f t .<++. t ) r
+
+{- | Extends the given relation with the attribute resulting from the second argument. If an attribute with the same name exists then it will be replaced. This allows for the function of the second argument to be simpler.
+
+See 'Database.HaskRel.Relational.Expression.extendA'.
+-}
+extendA :: forall r l e v v'.
+     (Ord (HExtendR (Tagged l e) (r v')), HExtend (Tagged l e) (r v'),
+      HDeleteAtLabel r l v v') =>
+     Set (r v) -> (r v -> Tagged l e) -> Set (HExtendR (Tagged l e) (r v'))
+extendA r f = Data.Set.map (\t -> f t .*. hDeleteAtLabel (Label::Label l) t) r
+-- TODO: An attempt to define a class with instances for what is now extend and extendA resulted in something that broke inference. Try again? Is it also possible make extendA a class, with an instance that uses .*. without hDeleteByLabel, and one that uses .@.? I can't see a way to. Probably better to make a quasiquoter, as mentioned in Expression.hs.
+
+
+{- | Disjoint extension. Extends the given relation with the result of the second argument, as 'extend', but without deleting any that exist.
+
+See 'Database.HaskRel.Relational.Expression.dExtend'.
+-}
+dExtend
+  :: (Ord (HList (HAppendListR r r'1)),
+      HLabelSet (LabelsOf (HAppendListR r r'1)),
+      HDeleteLabels (LabelsOf r) r' r'1, HAppendList r r'1,
+      HAllTaggedLV (HAppendListR r r'1),
+      HRLabelSet (HAppendListR r' r) -- Added to enforce disjoint structures
+      ) =>
+     Relation r' -> (Record r' -> Record r) -> Relation (HAppendListR r r'1)
+dExtend = extend
+
+{- |
+Disjoint extension of a single attribute. Extends the given relation with the result of the second argument, as 'extend', but without deleting any that exist. @l@ cannot already have any attribute @e@.
+
+See 'Database.HaskRel.Relational.Expression.dExtendA'.
+-}
+dExtendA :: (Ord (HExtendR e l), HExtend e l) =>
+     Set l -> (l -> e) -> Set (HExtendR e l)
+dExtendA r f = Data.Set.map (\t -> f t .*. t) r
+
+
+-- TODO: imageExtend: Use type level concatenation to build a label from the labels of the body
+{-
+type family (++) (as :: [k]) (bs :: [k]) :: [k] where
+  (++) a '[] = a
+  (++) '[] b = b
+  (++) (a ': as) bs = a ': (as ++ bs)
+-}
+
+{- | Extends the first given relation with an attribute resulting from imaging each tuple of said relation against the second given relation. This gives a superset of the information given by SQL @RIGHT OUTER JOIN@.
+
+See 'Database.HaskRel.Relational.Expression.imageExtendL'.
+-}
+imageExtendL
+  :: (Eq (HList l), Ord (HList l1), Ord (HList r'),
+      HLabelSet (LabelsOf l), HLabelSet (Label t ': LabelsOf l1),
+      HDeleteLabels (LabelsOf l1) r r',
+      H2ProjectByLabels (LabelsOf l) r l b,
+      H2ProjectByLabels (LabelsOf r) l1 l b1, HAllTaggedLV l1,
+      HAllTaggedLV l) =>
+     Set (Record l1)
+     -> Relation r
+     -> Label t
+     -> Set (Record (Tagged t (Relation r') ': l1))
+imageExtendL r1 r2 l = dExtendA r1 (\t -> l .=. t `image` r2)
+
+
+{- | Restricts the given relation according to the given predicate. Note that this is the well known 'WHERE' operator of both SQL and Tutorial D, but since "where" is a reserved keyword in Haskell it is named "restrict".
+
+See 'Database.HaskRel.Relational.Expression.restrict'.
+-}
+restrict :: Set a -> (a -> Bool) -> Set a
+restrict r f = Data.Set.filter f r
+
+
+-- TODO: Fail if any element of the second argument is not part of the first.
+
+{- | Projects the given relation on the given heading.
+
+See 'Database.HaskRel.Relational.Expression.project'.
+-}
+project
+  :: (Ord (HList a), HLabelSet (LabelsOf a),
+      H2ProjectByLabels ls t a b, HAllTaggedLV a) =>
+     Relation t -> proxy ls -> Relation a
+project r h = Data.Set.map ( hProjectByLabels h ) r
+
+{- | Projects the given relation on the heading of said given relation minus the given heading.
+
+See 'Database.HaskRel.Relational.Expression.projectAllBut'.
+-}
+projectAllBut
+  :: (Ord (HList r'), HDeleteLabels ks r r') =>
+     Relation r -> proxy ks -> Relation r'
+projectAllBut r a = Data.Set.map ( hDeleteLabels a ) r
+
+
+{- | Performs a union of the given relations.
+
+See 'Database.HaskRel.Relational.Expression.union'.
+-}
+union
+  :: (Ord (HList l), HRearrange3 (LabelsOf l) r l,
+      HLabelSet (LabelsOf l), SameLength' r l,
+      SameLength' r (LabelsOf l), SameLength' l r,
+      SameLength' (LabelsOf l) r) =>
+     Relation l -> Relation r -> Relation l
+union r1 r2 = Data.Set.union r1 ( relRearrange r2 )
+
+
+-- TODO: This should not just cause "error". Perhaps an Either String (Relation a) or Either (Relation ?) (Relation a) instead of causing an error. Will have to amend at least HFWPresent if so.
+{- | Performs a disjoint union between the two relvars. This is a union of disjoint relations, where a runtime error is raised if the operands are not disjoint.
+
+See 'Database.HaskRel.Relational.Expression.dUnion'.
+-}
+dUnion
+  :: (Ord (HList a), Typeable a, RecordValues a,
+      HRearrange3 (LabelsOf a) r a, HLabelSet (LabelsOf a),
+      HFoldr (Mapcar HPresentRecAttr) [[String]] (RecordValuesR a) [[String]],
+      SameLength' a r, SameLength' r a, SameLength' r (LabelsOf a),
+      SameLength' (LabelsOf a) r) =>
+     Relation a -> Relation r -> Relation a
+dUnion l r =
+  let u = Data.Set.union l $ relRearrange r
+   in if size l + size r > size u
+        then error $ "Arguments to dUnion are not disjoint, intersection:\n" ++ 
+                     showHRecSetTab ( Data.Set.intersection l $ relRearrange r )
+        else u
+
+
+{-| The intersection of two relations.
+
+Note how the name is different from Data.Set, where the comparable function is named "intersection". This is due to it being referred to as "intersect" in material describing the relational model; specifically named \"INTERSECT\" in Tutorial D.
+
+See 'Database.HaskRel.Relational.Expression.intersect'.
+-}
+intersect
+  :: (Ord (HList l), HRearrange3 (LabelsOf l) r l,
+      HLabelSet (LabelsOf l), SameLength' r l,
+      SameLength' r (LabelsOf l), SameLength' l r,
+      SameLength' (LabelsOf l) r) =>
+     Relation l -> Relation r -> Relation l
+intersect l r = intersection l $ relRearrange r
+
+{-| The difference of two relations.
+
+The "minus" term is used in material describing relational theory; specifically Tutorial D names the operator \"MINUS\".
+
+See 'Database.HaskRel.Relational.Expression.minus'.
+-}
+minus
+  :: (Ord (HList l), HRearrange3 (LabelsOf l) r l,
+      HLabelSet (LabelsOf l), SameLength' r l,
+      SameLength' r (LabelsOf l), SameLength' l r,
+      SameLength' (LabelsOf l) r) =>
+     Relation l -> Relation r -> Relation l
+minus l r = difference l $ relRearrange r
+
+{-| The difference of two relations. This differs from 'minus' in that the attribute order of the second argument takes precedence, which is neccessary to swap precedence since 'minus' is non-commutative. This function is as such equal to 'minus' as far as relational theory is concerned, the difference is on a lower level of abstraction.
+-}
+minus_
+  :: (Ord (HList l), HRearrange3 (LabelsOf l) r l,
+      HLabelSet (LabelsOf l), SameLength' r l,
+      SameLength' r (LabelsOf l), SameLength' l r,
+      SameLength' (LabelsOf l) r) =>
+     Relation r -> Relation l -> Relation l
+minus_ = difference . relRearrange
+-- TODO: Swapped versions of all r-dyadic, commutative functions.
+
+
+{- | Exclusive union, aka. symmetric difference.
+
+See 'Database.HaskRel.Relational.Expression.xUnion'.
+-}
+xUnion
+  :: (Ord (HList r1), HRearrange3 (LabelsOf r1) r r1,
+      HRearrange3 (LabelsOf r1) r1 r1, HLabelSet (LabelsOf r1),
+      SameLength' r r1, SameLength' r (LabelsOf r1), SameLength' r1 r,
+      SameLength' r1 r1, SameLength' r1 (LabelsOf r1),
+      SameLength' (LabelsOf r1) r, SameLength' (LabelsOf r1) r1) =>
+     Relation r1 -> Relation r -> Relation r1
+xUnion l r =
+    let r1 = relRearrange r
+     in Data.Set.union l r1 `minus` intersection l r1
+
+
+{- | Performs a natural join of the two given relations.
+
+See 'Database.HaskRel.Relational.Expression.naturalJoin'.
+-}
+naturalJoin
+  :: (Eq (HList l), Ord (HList (HAppendListR t1 t2)),
+      HRearrange3 (LabelsOf l) r l, HLabelSet (LabelsOf l),
+      HLabelSet (LabelsOf t2), HLabelSet (LabelsOf r),
+      HLabelSet (LabelsOf (HAppendListR t1 t2)),
+      H2ProjectByLabels (LabelsOf t1) t l t2,
+      H2ProjectByLabels (LabelsOf t) t1 r b, HAppendList t1 t2,
+      SameLength' l r, SameLength' r l, SameLength' r (LabelsOf l),
+      SameLength' (LabelsOf l) r, HAllTaggedLV t2, HAllTaggedLV l,
+      HAllTaggedLV r, HAllTaggedLV (HAppendListR t1 t2)) =>
+     Relation t1
+     -> Relation t -> Relation (HAppendListR t1 t2)
+naturalJoin r1 r2 = fromList $ Data.Set.foldr (\t1 b -> joinTOnR t1 r2 ++ b ) [] r1
+
+{- | Alias of 'naturalJoin'.
+
+See 'Database.HaskRel.Relational.Expression.nJoin'.
+-}
+nJoin
+  :: (Eq (HList l), Ord (HList (HAppendListR t1 t2)),
+      HRearrange3 (LabelsOf l) r l, HLabelSet (LabelsOf l),
+      HLabelSet (LabelsOf t2), HLabelSet (LabelsOf r),
+      HLabelSet (LabelsOf (HAppendListR t1 t2)),
+      H2ProjectByLabels (LabelsOf t1) t l t2,
+      H2ProjectByLabels (LabelsOf t) t1 r b, HAppendList t1 t2,
+      SameLength' l r, SameLength' r l, SameLength' r (LabelsOf l),
+      SameLength' (LabelsOf l) r, HAllTaggedLV t2, HAllTaggedLV l,
+      HAllTaggedLV r, HAllTaggedLV (HAppendListR t1 t2)) =>
+     Relation t1 -> Relation t -> Relation (HAppendListR t1 t2)
+nJoin = naturalJoin
+
+joinTOnR
+  :: (Eq (HList l), HRearrange3 (LabelsOf l) r l,
+      HLabelSet (LabelsOf l), HLabelSet (LabelsOf t2),
+      HLabelSet (LabelsOf r), HLabelSet (LabelsOf (HAppendListR t1 t2)),
+      H2ProjectByLabels (LabelsOf t1) t l t2,
+      H2ProjectByLabels (LabelsOf t) t1 r b, HAppendList t1 t2,
+      SameLength' l r, SameLength' r l, SameLength' r (LabelsOf l),
+      SameLength' (LabelsOf l) r, HAllTaggedLV t2, HAllTaggedLV l,
+      HAllTaggedLV r, HAllTaggedLV (HAppendListR t1 t2)) =>
+     Record t1 -> Relation t -> [Record (HAppendListR t1 t2)]
+joinTOnR t1 r2 = Data.Set.foldr (tupJoin t1) [] r2
+  where
+    tupJoin t1' t2' b =
+      let
+        (p',cP) = hProjectByLabels2 ( labelsOf t1' ) t2'
+      in
+        if p' `unordRecEq` hProjectByLabels ( labelsOf t2' ) t1'
+        then hAppend t1' cP : b
+        else b
+
+{- | The cartesian product of two relations. A specialized natural join; the natural join between two relations with disjoint headings.
+
+See 'Database.HaskRel.Relational.Expression.times'.
+-}
+times
+  :: (HRLabelSet (HAppendListR t r), -- This is added, to ensure that t and t1 are disjoint.
+      Eq (HList l), Ord (HList (HAppendListR t1 t2)),
+      HRearrange3 (LabelsOf l) r l, HLabelSet (LabelsOf l),
+      HLabelSet (LabelsOf t2), HLabelSet (LabelsOf r),
+      HLabelSet (LabelsOf (HAppendListR t1 t2)),
+      H2ProjectByLabels (LabelsOf t1) t l t2,
+      H2ProjectByLabels (LabelsOf t) t1 r b, HAppendList t1 t2,
+      SameLength' l r, SameLength' r l, SameLength' r (LabelsOf l),
+      SameLength' (LabelsOf l) r, HAllTaggedLV t2, HAllTaggedLV l,
+      HAllTaggedLV r, HAllTaggedLV (HAppendListR t1 t2)) =>
+     Relation t1
+     -> Relation t -> Relation (HAppendListR t1 t2)
+times = naturalJoin
+
+
+-- TODO: Get this working, now it just ends up with overlapping error instead of the Fail IsEmpty
+data IsEmpty
+
+-- | Failure class restricting a type-level operation to a non-empty result.
+class NotEmpty ( l :: [*] )
+instance NotEmpty l -- Is there any way to match on "anything that is not '[]"?
+instance ( Fail IsEmpty ) => NotEmpty '[]
+
+-- Finding out that when : is induced one must simply use ': instead was frustrating
+
+{-| Performs a natural join between two relations with intersecting headings. A specialized natural join.
+
+A join upon relations r1, r2 where the intersection of the heading of r1 and of r2 is not empty; the headings are not disjoint. This is the complement of 'times' that together with it forms a natural join; all that would be disallowed for @times@ is allowed here and vice-versa. The name is what I quickly settled on, suggestions for a better one would be welcome. (Attribute-Intersecting Natural Join is another candidate.)
+
+This function doesn't have a specific identity value, although it holds that @r \`interJoin\` r = r@
+
+See 'Database.HaskRel.Relational.Expression.interJoin'.
+-}
+interJoin
+  :: (HTIntersect (LabelsOf r) (LabelsOf t) i, NotEmpty i, -- i must not be '[]
+      Eq (HList l), Ord (HList (HAppendListR t1 t2)),
+      HRearrange3 (LabelsOf l) r l, HLabelSet (LabelsOf l),
+      HLabelSet (LabelsOf t2), HLabelSet (LabelsOf r),
+      HLabelSet (LabelsOf (HAppendListR t1 t2)),
+      H2ProjectByLabels (LabelsOf t1) t l t2,
+      H2ProjectByLabels (LabelsOf t) t1 r b, HAppendList t1 t2,
+      SameLength' l r, SameLength' r l, SameLength' r (LabelsOf l),
+      SameLength' (LabelsOf l) r, HAllTaggedLV t2, HAllTaggedLV l,
+      HAllTaggedLV r, HAllTaggedLV (HAppendListR t1 t2)) =>
+     Relation t1 -> Relation t -> Relation (HAppendListR t1 t2)
+interJoin = naturalJoin
+
+-- | Alias of 'interJoin'. See 'Database.HaskRel.Relational.Expression.iJoin'.
+iJoin
+  :: (Eq (HList l), Ord (HList (HAppendListR t1 t2)),
+      HRearrange3 (LabelsOf l) r l, HLabelSet (LabelsOf l),
+      HLabelSet (LabelsOf r), HLabelSet (LabelsOf t2),
+      HLabelSet (LabelsOf (HAppendListR t1 t2)),
+      H2ProjectByLabels (LabelsOf t) t1 r b,
+      H2ProjectByLabels (LabelsOf t1) t l t2,
+      HTIntersect (LabelsOf r) (LabelsOf t) i, HAppendList t1 t2,
+      SameLength' r l, SameLength' r (LabelsOf l), SameLength' l r,
+      SameLength' (LabelsOf l) r, HAllTaggedLV t2, HAllTaggedLV r,
+      HAllTaggedLV l, HAllTaggedLV (HAppendListR t1 t2), NotEmpty i) =>
+     Relation t1 -> Relation t -> Relation (HAppendListR t1 t2)
+iJoin = interJoin
+
+
+{- | Performs a semi-join of the first given relation against the second given relation.
+
+See 'Database.HaskRel.Relational.Expression.matching'.
+-}
+matching
+  :: (Eq (HList l), Ord (HList t), HRearrange3 (LabelsOf l) r l,
+      HLabelSet (LabelsOf l), HLabelSet (LabelsOf r),
+      H2ProjectByLabels (LabelsOf t) l1 l b,
+      H2ProjectByLabels (LabelsOf l1) t r b1, SameLength' l r,
+      SameLength' r l, SameLength' r (LabelsOf l),
+      SameLength' (LabelsOf l) r, HAllTaggedLV l, HAllTaggedLV r) =>
+     Relation t -> Relation l1 -> Relation t
+matching = semiJoin
+
+-- | Alias of 'matching'. See 'Database.HaskRel.Relational.Expression.semiJoin'.
+semiJoin
+  :: (Eq (HList l), Ord (HList t), HRearrange3 (LabelsOf l) r l,
+      HLabelSet (LabelsOf l), HLabelSet (LabelsOf r),
+      H2ProjectByLabels (LabelsOf t) l1 l b,
+      H2ProjectByLabels (LabelsOf l1) t r b1, SameLength' l r,
+      SameLength' r l, SameLength' r (LabelsOf l),
+      SameLength' (LabelsOf l) r, HAllTaggedLV l, HAllTaggedLV r) =>
+     Relation t -> Relation l1 -> Relation t
+semiJoin r1 r2 = fromList $ Data.Set.foldr (\t1 b -> semiJoinTOnR t1 ( toList r2 ) ++ b) [] r1
+
+semiJoinTOnR
+  :: (Eq (HList l), HRearrange3 (LabelsOf l) r l,
+      HLabelSet (LabelsOf l), HLabelSet (LabelsOf r),
+      H2ProjectByLabels (LabelsOf t) l1 l b,
+      H2ProjectByLabels (LabelsOf l1) t r b1, SameLength' l r,
+      SameLength' r l, SameLength' r (LabelsOf l),
+      SameLength' (LabelsOf l) r, HAllTaggedLV l, HAllTaggedLV r) =>
+     Record t -> [Record l1] -> [Record t]
+semiJoinTOnR _ [] = []
+semiJoinTOnR t1 [t2] =
+    if tIntersectEq t1 t2 then [t1]
+                          else []
+semiJoinTOnR t1 (t2:r2) =
+    if tIntersectEq t1 t2 then [t1]
+                          else semiJoinTOnR t1 r2
+
+tIntersectEq
+  :: (Eq (HList l), HRearrange3 (LabelsOf l) r l,
+      HLabelSet (LabelsOf l), HLabelSet (LabelsOf r),
+      H2ProjectByLabels (LabelsOf t) l1 l b,
+      H2ProjectByLabels (LabelsOf l1) t r b1, SameLength' l r,
+      SameLength' r l, SameLength' r (LabelsOf l),
+      SameLength' (LabelsOf l) r, HAllTaggedLV l, HAllTaggedLV r) =>
+     Record t -> Record l1 -> Bool
+tIntersectEq t1 t2 = hProjectByLabels ( labelsOf t1 ) t2 `unordRecEq` hProjectByLabels ( labelsOf t2 ) t1
+
+{- | Performs a semi-difference of the first given relation against the second given relation.
+
+Aka. antijoin:
+
+/Also known, a trifle inappropriately, as antijoin./
+
+   - Chris Date 2011, SQL and Relational Theory 2nd ed. p. 133
+
+See 'Database.HaskRel.Relational.Expression.notMatching'.
+-}
+notMatching
+  :: (Eq (HList l), Ord (HList t), HRearrange3 (LabelsOf l) r l,
+      HLabelSet (LabelsOf l), HLabelSet (LabelsOf r),
+      H2ProjectByLabels (LabelsOf t) l1 l b,
+      H2ProjectByLabels (LabelsOf l1) t r b1, SameLength' l r,
+      SameLength' r l, SameLength' r (LabelsOf l),
+      SameLength' (LabelsOf l) r, HAllTaggedLV l, HAllTaggedLV r) =>
+     Relation t -> Relation l1 -> Relation t
+notMatching = semiDiff
+
+-- | Alias of 'notMatching'. See 'Database.HaskRel.Relational.Expression.semiDiff'.
+semiDiff
+  :: (Eq (HList l), Ord (HList t), HRearrange3 (LabelsOf l) r l,
+      HLabelSet (LabelsOf l), HLabelSet (LabelsOf r),
+      H2ProjectByLabels (LabelsOf t) l1 l b,
+      H2ProjectByLabels (LabelsOf l1) t r b1, SameLength' l r,
+      SameLength' r l, SameLength' r (LabelsOf l),
+      SameLength' (LabelsOf l) r, HAllTaggedLV l, HAllTaggedLV r) =>
+     Relation t -> Relation l1 -> Relation t
+semiDiff r1 r2 = 
+    let tl2 = toList r2
+     in fromList $ Data.Set.foldr (\t1 b -> semiDiffTOnR t1 tl2 ++ b) [] r1
+
+semiDiffTOnR
+  :: (Eq (HList l), HRearrange3 (LabelsOf l) r l,
+      HLabelSet (LabelsOf l), HLabelSet (LabelsOf r),
+      H2ProjectByLabels (LabelsOf t) l1 l b,
+      H2ProjectByLabels (LabelsOf l1) t r b1, SameLength' l r,
+      SameLength' r l, SameLength' r (LabelsOf l),
+      SameLength' (LabelsOf l) r, HAllTaggedLV l, HAllTaggedLV r) =>
+     Record t -> [Record l1] -> [Record t]
+semiDiffTOnR t1 [] = [t1]
+semiDiffTOnR t1 [t2] =
+    if tIntersectEq t1 t2 then []
+                          else [t1]
+semiDiffTOnR t1 (t2:r2) =
+    if tIntersectEq t1 t2 then []
+                          else semiDiffTOnR t1 r2
+
+
+
+{- Image Relations
+Definition: Let relations r1 and r2 be joinable (i.e., such that attributes with the same name are of the same type); let t1 be a tuple of r1; let t2 be a tuple of r2 that has the same values for those common attributes as tuple t1 does; let relation r3 be that restriction of r2 that contains all and only such tuples t2; and let relation r4 be the projection of r3 on all but those common attributes. Then r4 is the image relation (with respect to r2) corresponding to t1.
+ - Chris J. Date, SQL and Relational Theory 2nd ed. p 136
+-}
+
+-- Project tuple on relation heading
+projectTOnR :: forall a b ls t proxy .
+     (HLabelSet (LabelsOf a), H2ProjectByLabels ( LabelsOf ls ) t a b,
+      HAllTaggedLV a) =>
+     Record t -> Relation ls -> Record a
+projectTOnR t _ = hProjectByLabels ( undefined :: Proxy ( LabelsOf ls ) ) t
+
+-- Specialization of restriction that takes a relation and a tuple whose heading
+-- is a (not neccesarily proper) subset of the heading of the relation, and
+-- restricts the relation by the intersection of attributes of the relation and
+-- tuple.
+restrictByRTuple
+  :: (Eq (HList l), HLabelSet (LabelsOf l),
+      H2ProjectByLabels (LabelsOf l) t l b, HAllTaggedLV l) =>
+     Relation t -> Record l -> Relation t
+restrictByRTuple r t = Data.Set.filter ( ( t == ) . hProjectByLabels ( labelsOf t ) ) r
+
+-- TODO: It would possibly be more performant and still correct to use partition
+-- instead of filter, and feed the remainder part of the result of that back into
+-- this function as parameter r.
+
+
+{-| The image of a relation corresponding to an r-tuple.
+
+An application of the first argument only, an r-tuple, to this function yields what is known as the @!!@ operator in Tutorial D.
+
+>>> let qtySum = Label::Label "qtySum"
+>>> :{
+    rPrint$ s'
+            `project` (rHdr (sno))
+            `extendA` (\ (image -> ii) ->
+                            qtySum .=.
+                                ( sum $ aggU $ ii ( sp' `project` (rHdr (sno,qty)) ) ) )
+ :}
+
+See 'Database.HaskRel.Relational.Expression.image'.
+-}
+image
+  :: (Eq (HList l), Ord (HList r'), HLabelSet (LabelsOf l),
+      HDeleteLabels (LabelsOf l1) r r',
+      H2ProjectByLabels (LabelsOf l) r l b,
+      H2ProjectByLabels (LabelsOf r) l1 l b1, HAllTaggedLV l) =>
+     Record l1 -> Relation r -> Relation r'
+image t r = projectAllBut (restrictByRTuple r $ projectTOnR t r) (labelsOf t)
+
+
+{-
+
+In the last example query for `image`, if one replaces the first relvar, "s", with relvar "sp" then the meaning of the query changes to:
+"Get the quantities of items in stock for all suppliers that supply any products."
+
+This form of semi aggregation, basically splitting a relation into two and aggregating one half, is common enough to warrant a specialized function.
+
+
+-}
+
+extendAByImage
+  :: (Eq (HList l), Ord v, Ord (HList l1), Ord (HList r'),
+      HLabelSet (LabelsOf l), HLabelSet (Label t ': LabelsOf l1),
+      HDeleteLabels (LabelsOf l1) r r',
+      H2ProjectByLabels (LabelsOf l) r l b,
+      H2ProjectByLabels (LabelsOf r) l1 l b1, HAllTaggedLV l1,
+      HAllTaggedLV l) =>
+     Relation r -> Relation l1
+     -> (Relation r' -> Tagged t v) -> Relation (Tagged t v ': l1)
+extendAByImage rel relP fOut = dExtendA relP $ fOut . ( `image` rel )
+
+-- TODO: group/groupAllBut can most likely be optimized by folding over them in a manner equivalent to this (somewhat) relational approach.
+
+{-| Groups the given attributes of the given relation into a given new relation valued attribute.
+
+As the Tutorial D GROUP operator, not SQL GROUP BY.
+
+See 'Database.HaskRel.Relational.Expression.group'.
+-}
+group
+  :: (Eq (HList l), Ord v, Ord (HList l1), Ord (HList r'),
+      HLabelSet (LabelsOf l), HLabelSet (Label t ': LabelsOf l1),
+      HDeleteLabels ks r l1, HDeleteLabels (LabelsOf l1) r r',
+      H2ProjectByLabels (LabelsOf l) r l b,
+      H2ProjectByLabels (LabelsOf r) l1 l b1, HAllTaggedLV l1,
+      HAllTaggedLV l) =>
+     Relation r
+     -> proxy ks -> (Relation r' -> Tagged t v) -> Relation (Tagged t v ': l1)
+group rel attsIn = extendAByImage rel $ rel `projectAllBut` attsIn
+
+-- TODO: That "group" supports both grouping into an RVA and grouping like group by is a bit of a design accident, consider making group only accept a label, and having a function that generalizes group that takes a function as group does now. Further consider a method that just takes a relation and a function, deriving the labels from the function result (I tried to do this but ran into issues).
+
+{- | Groups the given relation on all but the given attributes into a given new attribute.
+
+See 'Database.HaskRel.Relational.Expression.groupAllBut'.
+-}
+groupAllBut
+  :: (Eq (HList l), Ord v, Ord (HList l1), Ord (HList r'),
+      HLabelSet (LabelsOf l), HLabelSet (LabelsOf l1),
+      HLabelSet (Label t ': LabelsOf l1),
+      HDeleteLabels (LabelsOf l1) t1 r', H2ProjectByLabels ls t1 l1 b2,
+      H2ProjectByLabels (LabelsOf l) t1 l b,
+      H2ProjectByLabels (LabelsOf t1) l1 l b1, HAllTaggedLV l1,
+      HAllTaggedLV l) =>
+     Relation t1
+     -> proxy ls -> (Relation r' -> Tagged t v) -> Relation (Tagged t v ': l1)
+groupAllBut rel attsIn = extendAByImage rel $ rel `project` attsIn
+
+{-| Ungroups the given attribute of the given relation.
+
+>>> let pq = (Label :: Label "pq")
+>>> sp' == ungroup ( group sp' (rHdr (pno,qty)) (pq .=.)) pq
+True
+
+Note the difference to 'Database.HaskRel.Relational.Expression.ungroup', which requires 'Database.HaskRel.Relational.Expression.rEq' for relational comparison.
+-}
+ungroup
+  :: (Eq (HList l), Ord (HList (HAppendListR t1 t2)),
+      HasField l1 (Record v) (Relation t), HRearrange3 (LabelsOf l) r l,
+      HLabelSet (LabelsOf l), HLabelSet (LabelsOf t2),
+      HLabelSet (LabelsOf r), HLabelSet (LabelsOf (HAppendListR t1 t2)),
+      H2ProjectByLabels (LabelsOf t1) t l t2,
+      H2ProjectByLabels (LabelsOf t) t1 r b,
+      H2ProjectByLabels '[Label l1] v t3 t1, HAppendList t1 t2,
+      SameLength' l r, SameLength' r l, SameLength' r (LabelsOf l),
+      SameLength' (LabelsOf l) r, HAllTaggedLV t2, HAllTaggedLV l,
+      HAllTaggedLV r, HAllTaggedLV (HAppendListR t1 t2)) =>
+     Relation v -> Label l1 -> Relation (HAppendListR t1 t2)
+ungroup r a = fromList $ Data.Set.foldr f [] r
+  where f t b = joinTOnR (hDeleteAtLabel a t) (t .!. a) ++ b
+
+
+extendByImage
+  :: (Eq (HList l), Ord (HList r'2),
+      Ord (HList (HAppendListR r r'1)),
+      HLabelSet (LabelsOf (HAppendListR r r'1)),
+      HLabelSet (LabelsOf (HAppendListR r' r)), HLabelSet (LabelsOf l),
+      HDeleteLabels (LabelsOf r) r' r'1,
+      HDeleteLabels (LabelsOf r') r1 r'2,
+      H2ProjectByLabels (LabelsOf l) r1 l b,
+      H2ProjectByLabels (LabelsOf r1) r' l b1, HAppendList r r'1,
+      HAllTaggedLV l, HAllTaggedLV (HAppendListR r r'1),
+      HAllTaggedLV (HAppendListR r' r)) =>
+     Relation r1
+     -> Relation r'
+     -> (Relation r'2 -> Record r)
+     -> Relation (HAppendListR r r'1)
+extendByImage rel relP fOut = dExtend relP $ fOut . ( `image` rel )
+
+{- | Summarize.
+
+See 'Database.HaskRel.Relational.Expression.summarize'.
+-}
+summarize
+  :: (Eq (HList l), Ord (HList r'), Ord (HList r'2),
+      Ord (HList (HAppendListR r r'1)),
+      HLabelSet (LabelsOf (HAppendListR r r'1)),
+      HLabelSet (LabelsOf (HAppendListR r' r)), HLabelSet (LabelsOf l),
+      HDeleteLabels ks r2 r', HDeleteLabels (LabelsOf r) r' r'1,
+      HDeleteLabels (LabelsOf r') r1 r'2,
+      H2ProjectByLabels (LabelsOf l) r1 l b,
+      H2ProjectByLabels (LabelsOf r1) r' l b1, HAppendList r r'1,
+      HAllTaggedLV l, HAllTaggedLV (HAppendListR r r'1),
+      HAllTaggedLV (HAppendListR r' r)) =>
+     Relation r1
+     -> Relation r2
+     -> proxy ks
+     -> (Relation r'2 -> Record r)
+     -> Relation (HAppendListR r r'1)
+summarize relA relB attsIn f = extendByImage relA ( relB `projectAllBut` attsIn ) f
+
+{- | Auto-summarization. A specialization of 'summarize' with the same source and destination relation.
+
+See 'Database.HaskRel.Relational.Expression.aSummarize'.
+-}
+aSummarize
+  :: (Eq (HList l), Ord (HList r'), Ord (HList r'2),
+      Ord (HList (HAppendListR r r'1)),
+      HLabelSet (LabelsOf (HAppendListR r r'1)),
+      HLabelSet (LabelsOf (HAppendListR r' r)), HLabelSet (LabelsOf l),
+      HDeleteLabels ks r1 r', HDeleteLabels (LabelsOf r) r' r'1,
+      HDeleteLabels (LabelsOf r') r1 r'2,
+      H2ProjectByLabels (LabelsOf l) r1 l b,
+      H2ProjectByLabels (LabelsOf r1) r' l b1, HAppendList r r'1,
+      HAllTaggedLV l, HAllTaggedLV (HAppendListR r r'1),
+      HAllTaggedLV (HAppendListR r' r)) =>
+     Relation r1
+     -> proxy ks
+     -> (Relation r'2 -> Record r)
+     -> Relation (HAppendListR r r'1)
+aSummarize rel attsIn f = extendByImage rel ( rel `projectAllBut` attsIn ) f
+
+{-
+-- TODO: Needs work: >>> pt$ summarize' sp' (s' `project` (undefined :: Labels '["sno"])) (\ (r :: Relation '[QTY, PNO]) -> qty .=. sum ( agg qty r ) .*. emptyRecord)   ==> Boom!
+-- Although regular summarize suffers from the same issue, so it might not be a fixable issue:
+-- pt$ summarize sp' (s' `project` (undefined :: Labels '["sno"])) (undefined :: Labels '["qty"]) (\(r :: Relation '[QTY,PNO]) -> qty .=. sum ( agg qty r ) .*. emptyRecord)
+-- Boom!
+
+{- | Summarize on the arguments of the function.
+
+See 'Database.HaskRel.Relational.Expression.summarize''.
+-}
+summarize'
+  :: (Eq (HList l), Ord (HList r'), Ord (HList r'2),
+      Ord (HList (HAppendListR r r'1)),
+      HLabelSet (LabelsOf (HAppendListR r r'1)),
+      HLabelSet (LabelsOf (HAppendListR r' r)), HLabelSet (LabelsOf l),
+      HDeleteLabels (LabelsOf r'2) r2 r',
+      HDeleteLabels (LabelsOf r) r' r'1,
+      HDeleteLabels (LabelsOf r') r1 r'2,
+      H2ProjectByLabels (LabelsOf l) r1 l b,
+      H2ProjectByLabels (LabelsOf r1) r' l b1, HAppendList r r'1,
+      HAllTaggedLV l, HAllTaggedLV (HAppendListR r r'1),
+      HAllTaggedLV (HAppendListR r' r)) =>
+     Relation r1
+     -> Relation r2
+     -> (Relation r'2 -> Record r)
+     -> Relation (HAppendListR r r'1)
+summarize' relA relB f = extendByImage relA ( relB `projectAllBut` ( labelsOfRArgs f ) ) f
+
+{- | Auto-summarization on the argument types of the function.
+
+See 'Database.HaskRel.Relational.Expression.aSummarize''.
+-}
+aSummarize'
+  :: (Eq (HList l), Ord (HList r'), Ord (HList r'2),
+      Ord (HList (HAppendListR r r'1)),
+      HLabelSet (LabelsOf (HAppendListR r r'1)),
+      HLabelSet (LabelsOf (HAppendListR r' r)), HLabelSet (LabelsOf l),
+      HDeleteLabels (LabelsOf r'2) r1 r',
+      HDeleteLabels (LabelsOf r) r' r'1,
+      HDeleteLabels (LabelsOf r') r1 r'2,
+      H2ProjectByLabels (LabelsOf l) r1 l b,
+      H2ProjectByLabels (LabelsOf r1) r' l b1, HAppendList r r'1,
+      HAllTaggedLV l, HAllTaggedLV (HAppendListR r r'1),
+      HAllTaggedLV (HAppendListR r' r)) =>
+     Relation r1
+     -> (Relation r'2 -> Record r) -> Relation (HAppendListR r r'1)
+aSummarize' rel f = extendByImage rel ( rel `projectAllBut` ( labelsOfRArgs f ) ) f
+
+labelsOfRArgs :: (Relation l -> x) -> Proxy (LabelsOf l)
+labelsOfRArgs f = undefined
+-}
+
+
+
+-- Supporting, non-relational functions:
+
+-- | Gives the cardinality of the argument.
+count :: Set a -> Int
+count = Data.Set.size
+
+-- | Gives whether the given argument is empty or not.
+isEmpty :: Set a -> Bool
+isEmpty = Data.Set.null
+
+{- | Tests whether the second argument is a proper subset of the first.
+
+See 'Database.HaskRel.Relational.Expression.isProperSubsetOf'.
+-}
+isProperSubsetOf
+  :: (Ord (HList l), HRearrange3 (LabelsOf l) r l,
+      HLabelSet (LabelsOf l), SameLength' r l,
+      SameLength' r (LabelsOf l), SameLength' l r,
+      SameLength' (LabelsOf l) r) =>
+     Relation l -> Relation r -> Bool
+isProperSubsetOf l r = Data.Set.isProperSubsetOf l ( relRearrange r )
+
+{- | Tests whether the second argument is a subset of the first.
+
+See 'Database.HaskRel.Relational.Expression.isSubsetOf'.
+-}
+isSubsetOf
+  :: (Ord (HList l), HRearrange3 (LabelsOf l) r l,
+      HLabelSet (LabelsOf l), SameLength' r l,
+      SameLength' r (LabelsOf l), SameLength' l r,
+      SameLength' (LabelsOf l) r) =>
+     Relation l -> Relation r -> Bool
+isSubsetOf l r = Data.Set.isSubsetOf l ( relRearrange r )
+
+{- | Right-fold of an attribute of a relation (although a "right" fold doesn't make sense in the context of the relational model). Note that the value of the third argument, 'att', is not used and may be "undefined".
+
+See 'Database.HaskRel.Relational.Expression.rafoldr'.
+-}
+rafoldr
+  :: (Foldable t, HasField l a b1) =>
+     (b1 -> b -> b) -> b -> Label l -> t a -> b
+rafoldr f b a r = foldr ( f . (.!. a) ) b r
+
+
+{- | Attribute value aggregation, a specialization of 'rafoldr' that aggregates the values of a single attribute into a list of the values the attribute type wraps.
+
+Note that the value of the first argument, 'att', is not used and may be "undefined".
+
+>>> sum $ agg qty sp'
+3100
+
+See 'Database.HaskRel.Relational.Expression.agg'.
+-}
+agg :: (Foldable t, HasField l a a1) => Label l -> t a -> [a1]
+agg = rafoldr (:) []
+
+
+unwrapUnary :: Record '[Tagged t t1] -> t1
+unwrapUnary ( Record (Tagged v `HCons` HNil) ) = v
+
+{- | Right-fold of the attribute of a unary relation.
+
+See 'Database.HaskRel.Relational.Expression.rafoldrU'.
+-}
+rafoldrU :: Foldable t => (b1 -> b -> b) -> b -> t (Record '[Tagged t1 b1]) -> b
+rafoldrU f b r = foldr ( f . unwrapUnary ) b r
+
+{- | Aggregation of the single attribute of a unary relation. A specialization of 'agg', and thus in turn of 'rafoldr', that aggregates the single attribute of a unary relation, without requiring the name of that attribute.
+
+>>> sum $ aggU $ sp' `project` (rHdr (qty))
+1000
+
+See 'Database.HaskRel.Relational.Expression.aggU'.
+-}
+aggU :: Foldable t => t (Record '[Tagged t1 a]) -> [a]
+aggU = rafoldrU (:) []
diff --git a/src/Database/HaskRel/Relational/Assignment.hs b/src/Database/HaskRel/Relational/Assignment.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/HaskRel/Relational/Assignment.hs
@@ -0,0 +1,372 @@
+{-# LANGUAGE TypeFamilies, FlexibleContexts, ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
+
+-- TODO: dInsert and iDelete should not just invoke "error", but a proper fix is most likely to define a relational transaction that supports this correctly 
+
+{-| 
+Module      : Database.HaskRel.Relational.Assignment
+Description : Relational assignment
+Copyright   : © Thor Michael Støre, 2015
+License     : GPL v2 without "any later version" clause
+Maintainer  : thormichael át gmail døt com
+Stability   : experimental
+
+Relational assignment and specalizations thereof. As with "Database.HaskRel.Relational.Algebra" this does not support relational expressions building on relvars, but defers that to "Database.HaskRel.Relational.Expression".
+-}
+module Database.HaskRel.Relational.Assignment (
+  -- * The primitive assignment function
+  assign,
+  -- * Specialized assignment functions
+  insert, dInsert, update, updateAll, delete, iDelete, deleteP,
+  -- * Further specialized and simplified forms of update
+  updateA, updateAllA
+  ) where
+
+import Control.Monad ( unless )
+
+import Data.HList.CommonMain
+
+import Data.Set ( Set, filter, difference, fromList, size )
+import qualified Data.Set ( map, foldr )
+
+import Data.Typeable ( Typeable )
+
+import System.Directory ( renameFile )
+
+import Database.HaskRel.Relational.Definition ( Relation, RTuple, bodyAsList, relRearrange' )
+import Database.HaskRel.HFWTabulation ( HPresentRecAttr, showHRecSetTab )
+
+import Database.HaskRel.Relational.Algebra ( intersect, minus, minus_ )
+import Database.HaskRel.Relational.Variable
+
+
+rewriteRelvar
+  :: (Show (HList (RecordValuesR r)), RecordValues r) =>
+     Relvar a -> Relation r -> IO ()
+rewriteRelvar rv updated =
+  do writeRelvarBody ( relvarPath rv ++ ".new" ) ( bodyAsList updated )
+     renameFile ( relvarPath rv ++ ".new" ) ( relvarPath rv )
+
+
+-- == Relation variable update operations == --
+
+-- | Writes a relation value to a relvar file, replacing the existing value.
+assign
+  :: (Ord (HList a), Show (HList (RecordValuesR a)), RecordValues a,
+      HRearrange3 (LabelsOf a) r a, HLabelSet (LabelsOf a),
+      SameLength' r a, SameLength' r (LabelsOf a), SameLength' a r,
+      SameLength' (LabelsOf a) r) =>
+     Relvar a -> Relation r -> IO ()
+assign rv r = do rewriteRelvar rv ( relRearrange' r $ relvarType rv )
+                 putStrLn $ "Value assigned to " ++ relvarPath rv
+
+
+appendRelvar :: (Show (t a), Foldable t) => Relvar t1 -> t a -> Bool -> IO ()
+appendRelvar rv hll empty =
+    let prefix = if empty then "" else ","
+     in unless (null hll)
+            $ appendFile (relvarPath rv) $ prefix ++ init ( tail $ show hll )
+
+-- == Inserts
+
+{-|
+Inserts a relation into a relvar. This differs from SQL's INSERT; the relvar is updated to the union of the relvar and the relation value given as arguments.
+
+See `Database.HaskRel.Relational.Expression.insert`.
+-}
+insert
+  :: (Ord (HList a), Read (HList (RecordValuesR a)),
+      Show (HList (RecordValuesR a)), RecordValues a,
+      HRearrange3 (LabelsOf a) r a, HLabelSet (LabelsOf a),
+      HMapAux HList TaggedFn (RecordValuesR a) a, SameLength' r a,
+      SameLength' r (LabelsOf a), SameLength' a r,
+      SameLength' (LabelsOf a) r) =>
+     Relvar a -> Relation r -> IO ()
+insert rv r = do
+    rv' <- readRelvar rv
+    let diff = ( r `minus_` rv' )
+        in do appendRelvar rv ( bodyAsList diff ) ( null rv' )
+              putStrLn $ "Inserted " ++ show ( size diff ) ++ " of " ++
+                         show ( size r ) ++ " tuples into " ++ relvarPath rv
+-- Note: "minus_" is used in place of "minus" to rearrange the relation to the relvar, and not vice-versa, as it must be.
+
+
+{-| Disjoint insert. Closer to SQL INSERT, except that this will never insert a
+duplicate tuple.
+
+See `Database.HaskRel.Relational.Expression.dInsert`.
+-}
+dInsert
+  :: (Ord (HList t), Read (HList (RecordValuesR t)),
+      Show (HList (RecordValuesR r)), Typeable t, RecordValues r,
+      RecordValues t, HRearrange3 (LabelsOf t) r t,
+      HLabelSet (LabelsOf t), HMapAux HList TaggedFn (RecordValuesR t) t,
+      HFoldr (Mapcar HPresentRecAttr) [[String]] (RecordValuesR t) [[String]],
+      SameLength' r t, SameLength' r (LabelsOf t), SameLength' t r,
+      SameLength' (LabelsOf t) r) =>
+     Relvar t -> Relation r -> IO ()
+dInsert rv r = do
+    rv' <- readRelvar rv
+    let inter = ( rv' `intersect` r )
+        in
+      if not ( null inter )
+         then error $ "Unique constraint violation, tuples already present in " ++ relvarPath rv ++ ":\n" ++ showHRecSetTab inter
+         else 
+           do appendRelvar rv ( bodyAsList r ) ( null rv' )
+              putStrLn $ "Inserted " ++ show ( size r ) ++ " tuples into " ++ relvarPath rv
+
+-- == Updates
+
+-- Warning: Doesn't infer the way I'd like it to.
+funSelfUpdate
+  :: (HRearrange3 (LabelsOf r') (HAppendListR r r'2) r',
+      HLabelSet (LabelsOf r'), HLabelSet (LabelsOf (HAppendListR r r'2)),
+      HDeleteLabels (LabelsOf r) r' r'2, HAppendList r r'2,
+      SameLength' r' (HAppendListR r r'2),
+      SameLength' (LabelsOf r') (HAppendListR r r'2),
+      SameLength' (HAppendListR r r'2) r',
+      SameLength' (HAppendListR r r'2) (LabelsOf r'),
+      HAllTaggedLV (HAppendListR r r'2)) =>
+     (Record r' -> Record r) -> Record r' -> Record r'
+funSelfUpdate f t = hRearrange ( labelsOf t ) ( f t .<++. t )
+
+update'
+  :: (Num t, Num t1, Ord (HList r'),
+      HRearrange3 (LabelsOf r') (HAppendListR r r'2) r',
+      HLabelSet (LabelsOf r'), HLabelSet (LabelsOf (HAppendListR r r'2)),
+      HDeleteLabels (LabelsOf r) r' r'2, HAppendList r r'2,
+      SameLength' r' (HAppendListR r r'2),
+      SameLength' (LabelsOf r') (HAppendListR r r'2),
+      SameLength' (HAppendListR r r'2) r',
+      SameLength' (HAppendListR r r'2) (LabelsOf r'),
+      HAllTaggedLV (HAppendListR r r'2)) =>
+     Set (Record r')
+     -> (Record r' -> Bool)
+     -> (Record r' -> Record r)
+     -> (t, t1, Set (Record r'))
+update' r p f = update'' r p (funSelfUpdate f)
+
+updateA'
+  :: (Num t, Num t1, Ord (record r), HUpdateAtLabel record l v r r,
+      SameLength' r r) =>
+     Set (record r) -> (record r -> Bool) -> (record r -> Tagged l v)
+     -> (t, t1, Set (record r))
+updateA' r p f = update'' r p (\t -> f t .<. t)
+
+update'' :: (Num t, Num t1, Ord a) =>
+     Set a -> (a -> Bool) -> (a -> a) -> (t, t1, Set a)
+update'' r p f = 
+    let (a,b,c) = Data.Set.foldr
+                      (\t (a',b',c') ->
+                          if p t then ( a' + 1, b' + 1, f t : c' )
+                                 else ( a', b' + 1, t : c' ) )
+                      (0,0,[])
+                      r
+        in (a, b, fromList c)
+
+updateAll'
+  :: (Num t, Ord (HList r'),
+      HRearrange3 (LabelsOf r') (HAppendListR r r'2) r',
+      HLabelSet (LabelsOf r'), HLabelSet (LabelsOf (HAppendListR r r'2)),
+      HDeleteLabels (LabelsOf r) r' r'2, HAppendList r r'2,
+      SameLength' r' (HAppendListR r r'2),
+      SameLength' (LabelsOf r') (HAppendListR r r'2),
+      SameLength' (HAppendListR r r'2) r',
+      SameLength' (HAppendListR r r'2) (LabelsOf r'),
+      HAllTaggedLV (HAppendListR r r'2)) =>
+     Set (Record r') -> (Record r' -> Record r) -> (t, Set (Record r'))
+updateAll' r f = updateAll'' r (funSelfUpdate f)
+
+updateAllA'
+  :: (Num t, Ord (record r), HUpdateAtLabel record l v r r,
+      SameLength' r r) =>
+     Set (record r) -> (record r -> Tagged l v) -> (t, Set (record r))
+updateAllA' r f = updateAll'' r (\t -> f t .<. t)
+
+updateAll'' :: (Num t, Ord a1) => Set a -> (a -> a1) -> (t, Set a1)
+updateAll'' r f = 
+    let (a,b) = Data.Set.foldr (\t (a',b') -> ( a' + 1, f t : b' ) ) (0,[]) r
+        in (a, fromList b)
+
+
+doUpdate
+  :: (Show a, Show a1, Show (HList (RecordValuesR r)),
+      RecordValues r) =>
+     Relvar a2 -> (a, a1, Relation r) -> IO ()
+doUpdate rv ( updCount, totCount, updated ) =
+  do rewriteRelvar rv updated
+     putStrLn $ "Updated " ++ show updCount ++ " of " ++ show totCount ++ " tuples in " ++ relvarPath rv
+
+
+{-| Updates tuples of a relvar that match the given predicate. As SQL UPDATE.
+
+>>> update sp (\ [pun|pno|] -> pno == "P2" || pno == "P3" ) (\ [pun|qty|] -> _qty ( qty - 25 ) .*. emptyRecord)
+Updated 5 of 12 tuples in SuppliersPartsDB/SP.rv
+*SuppliersPartsExample> rPrint$ sp
+┌─────┬─────┬─────┐
+│ sno │ pno │ qty │
+╞═════╪═════╪═════╡
+│ S1  │ P1  │ 300 │
+│ S1  │ P2  │ 175 │
+│ S1  │ P3  │ 375 │
+│ S1  │ P4  │ 200 │
+...
+
+Note how the cardinality of the relvar will be equal or lower after an update:
+
+>>> assign sp sp'
+Value assigned to SuppliersPartsDB/SP.rv
+>>> count sp
+12
+>>> update sp (\[pun|pno|] -> pno == "P1" || pno == "P2" || pno == "P3") (\_ -> _pno "P1" .*. _qty 50 .*. emptyRecord)
+Updated 7 of 12 tuples in SuppliersPartsDB/SP.rv
+>>> count sp
+9
+-}
+-- TODO: Fix update count message to reflect the situation in the last example above, although this is tricky as this is most likely something that belongs naturally in the set level functions. Note however that it is not feasable to give update counts at all in RDBSMs, as keeping exact track of the cardinality of relvars constitutes an overhead that is in many cases unacceptable, and doesn't provide information that is as useful as a naïve mind might think anyhow.
+update
+  :: (Ord (HList a), Read (HList (RecordValuesR a)),
+      Show (HList (RecordValuesR a)), RecordValues a,
+      HRearrange3 (LabelsOf a) (HAppendListR r r'2) a,
+      HLabelSet (LabelsOf a), HLabelSet (LabelsOf (HAppendListR r r'2)),
+      HDeleteLabels (LabelsOf r) a r'2,
+      HMapAux HList TaggedFn (RecordValuesR a) a, HAppendList r r'2,
+      SameLength' a (HAppendListR r r'2),
+      SameLength' (LabelsOf a) (HAppendListR r r'2),
+      SameLength' (HAppendListR r r'2) a,
+      SameLength' (HAppendListR r r'2) (LabelsOf a),
+      HAllTaggedLV (HAppendListR r r'2)) =>
+     Relvar a -> (Record a -> Bool) -> (Record a -> Record r) -> IO ()
+update rv p f = do
+    rv' <- readRelvar rv
+    doUpdate rv ( update' rv' p f )
+
+
+{-| Updates all tuples of a relvar. The second argument is a function that results in an attribute, making for a simpler function than for `update`.
+
+>>> updateA sp (\ [pun|pno|] -> pno == "P2" || pno == "P3" ) (\ [pun|qty|] -> _qty $ qty - 25)
+Updated 5 of 12 tuples in SuppliersPartsDB/SP.rv
+-}
+-- TODO: Can't get the type signature to compile, HUpdateAtLabel2 isn't exported from Data.HList.Record
+updateA rv p f = do
+    rv' <- readRelvar rv
+    doUpdate rv ( updateA' rv' p f )
+
+
+doUpdateAll
+  :: (Show a, Show (HList (RecordValuesR r)), RecordValues r) =>
+     Relvar a1 -> (a, Relation r) -> IO ()
+doUpdateAll rv ( count, updated ) =
+  do rewriteRelvar rv updated
+     putStrLn $ "Updated " ++ show count ++ " tuples in " ++ relvarPath rv
+
+{-| Updates tuples of a relvar that match the given predicate.
+
+In SQL and Tutorial D both the predicate of @UPDATE@ is an optional clause, but optional clauses isn't idiomatic Haskell, hence this separate updateAll function.
+
+>>> updateAll sp (\ [pun|qty pno|] -> _qty ( qty - 25 ) .*. _pno ( pno ++ "X" ) .*. emptyRecord)
+Updated 12 tuples in SuppliersPartsDB/SP.rv
+*SuppliersPartsExample> pt sp
+┌───────────────┬───────────────┬────────────────┐
+│ sno :: String │ pno :: String │ qty :: Integer │
+╞═══════════════╪═══════════════╪════════════════╡
+│ S1            │ P1X           │ 275            │
+...
+-}
+updateAll
+  :: (Ord (HList a), Read (HList (RecordValuesR a)),
+      Show (HList (RecordValuesR a)), RecordValues a,
+      HRearrange3 (LabelsOf a) (HAppendListR r r'2) a,
+      HLabelSet (LabelsOf a), HLabelSet (LabelsOf (HAppendListR r r'2)),
+      HDeleteLabels (LabelsOf r) a r'2,
+      HMapAux HList TaggedFn (RecordValuesR a) a, HAppendList r r'2,
+      SameLength' a (HAppendListR r r'2),
+      SameLength' (LabelsOf a) (HAppendListR r r'2),
+      SameLength' (HAppendListR r r'2) a,
+      SameLength' (HAppendListR r r'2) (LabelsOf a),
+      HAllTaggedLV (HAppendListR r r'2)) =>
+     Relvar a -> (Record a -> Record r) -> IO ()
+updateAll rv f = do
+    rv' <- readRelvar rv
+    doUpdateAll rv (updateAll' rv' f)
+
+{-| Updates all tuples of a relvar. The second argument is a function that results in an attribute, making for a simpler function than for `updateAll`.
+
+>>> updateAllA sp (\ [pun|qty|] -> _qty $ qty - 50)
+Updated 12 tuples in SuppliersPartsDB/SP.rv
+>>> rPrint$ sp
+┌───────────────┬───────────────┬────────────────┐
+│ sno :: String │ pno :: String │ qty :: Integer │
+╞═══════════════╪═══════════════╪════════════════╡
+│ S1            │ P1            │ 250            │
+...
+-}
+-- TODO: Can't get the type signature to compile, HUpdateAtLabel2 isn't visible from Data.HList.Record
+updateAllA rv f = do
+    rv' <- readRelvar rv
+    doUpdateAll rv (updateAllA' rv' f)
+
+-- == Deletes
+
+doDelete rv filtered nDeleted =
+  do writeRelvarBody ( relvarPath rv ++ ".new" ) ( bodyAsList filtered )
+     renameFile ( relvarPath rv ++ ".new" ) ( relvarPath rv )
+     putStrLn $ "Deleted " ++ nDeleted ++ " tuples from " ++ relvarPath rv
+
+{-| Deletes a specified subset of a relvar. Note that this is not SQL DELETE, but instead a generalization thereof.
+
+See `Database.HaskRel.Relational.Expression.delete`.
+-}
+delete
+  :: (Ord (HList t), Read (HList (RecordValuesR t)),
+      Show (HList (RecordValuesR t)), RecordValues t,
+      HMapAux HList TaggedFn (RecordValuesR t) t) =>
+     Relvar t -> Relation t -> IO ()
+delete rv r = do
+    rv' <- readRelvar rv
+    let filtered = Data.Set.difference rv' r
+        in doDelete rv filtered ( show $ size rv' - size filtered )
+
+{-|
+Performs an inclusive delete against a relvar. Also not SQL DELETE. This will fail if the second argument is not a subset of the relation value identified by the relation variable reference.
+
+See `Database.HaskRel.Relational.Expression.iDelete`.
+-}
+iDelete
+  :: (Ord (HList a), Ord (HList t), Read (HList (RecordValuesR t)),
+      Show (HList (RecordValuesR t)), Typeable a, RecordValues a,
+      RecordValues t, HRearrange3 (LabelsOf t) a t,
+      HRearrange3 (LabelsOf a) t a, HLabelSet (LabelsOf t),
+      HLabelSet (LabelsOf a), HMapAux HList TaggedFn (RecordValuesR t) t,
+      HFoldr (Mapcar HPresentRecAttr) [[String]] (RecordValuesR a) [[String]],
+      SameLength' a t, SameLength' a (LabelsOf t), SameLength' t a,
+      SameLength' t (LabelsOf a), SameLength' (LabelsOf t) a,
+      SameLength' (LabelsOf a) t) =>
+     Relvar t -> Relation a -> IO ()
+iDelete rv r = do
+    rv' <- readRelvar rv
+    let filtered = rv' `minus` r
+        in if size filtered > ( size rv' - size r )
+           then error $ "Tuples not found in relvar " ++ relvarPath rv ++ ":\n" ++ showHRecSetTab ( r `minus` rv' )
+           else doDelete rv filtered ( show $ size rv' - size filtered )
+
+{- | Delete by predicate, as SQL DELETE.
+
+>>> let newProd = relation [rTuple (pno .=. "P7", pName .=. "Baloon", color .=. "Red", weight .=. (-5 :: Rational), city .=. "Berlin")]
+>>> insert p newProd
+Inserted 1 of 1 tuples into SuppliersPartsDB/P.rv
+>>> deleteP p (\ [pun|pno|] -> pno == "P7" )
+Deleted 1 tuples from SuppliersPartsDB/P.rv
+-}
+deleteP
+  :: (Ord (HList t), Read (HList (RecordValuesR t)),
+      Show (HList (RecordValuesR t)), RecordValues t,
+      HMapAux HList TaggedFn (RecordValuesR t) t) =>
+     Relvar t -> (RTuple t -> Bool) -> IO ()
+deleteP rv p = do
+    rv' <- readRelvar rv
+    let filtered = Data.Set.filter ( not . p ) rv'
+        in doDelete rv filtered ( show $ size rv' - size filtered )
+
+-- An iDeleteP function could also be defined, but its utility would be marginal.
+
diff --git a/src/Database/HaskRel/Relational/Definition.hs b/src/Database/HaskRel/Relational/Definition.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/HaskRel/Relational/Definition.hs
@@ -0,0 +1,337 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-|
+Module      : Definition
+Description : Definition and presentation of relational objects in terms of Haskell and HList records
+Copyright   : © Thor Michael Støre, 2015
+License     : GPL v2 without "any later version" clause
+Maintainer  : thormichael át gmail døt com
+Stability   : experimental
+
+Definition and presentation of relational objects in terms of Haskell and HList records, and certain implementation level supporting functions.
+
+Naming convention of the relational model is, to a degree, adopted to clarify how it is mirrored into Haskell. With these aliases in place the following are equivalent:
+
+>>> :t fromList [] :: Set (Record '[Tagged "sno" String, Tagged "status" Int])
+
+>>> :t relation [] :: Relation '[Attr "sno" String, Attr "status" Int]
+-}
+
+module Database.HaskRel.Relational.Definition (
+  -- * Definition
+  Attr, RTuple, Relation,
+  -- ** Labels
+  {-| To be in line with the naming convention of the relational model, the @Label@ type could be referred to as an "attribute name", and the @Labels@ type as "attribute names", but since this would not clarify the matter significantly HaskRel re-exports them as-is.
+
+It is important to note how labels may either be pre-defined, or used ad-hoc:
+
+>>> let qty = Label :: Label "qty"
+>>> sum $ agg qty sp'
+3100
+>>> sum $ agg ( Label :: Label "qty" ) sp'
+3100
+  -}
+  Label(Label), Labels,
+  -- * Construction
+  {- | These functions are based on common HList operations, and given aliases that are in line with relational theory. As mentioned for each function they only support 0 to 6-tuples, which is of course a drawback. For r-tuples of other degrees the basic HList approaches to record construction may be used:
+
+>>> let sno = Label :: Label "sno"
+... etc ...
+>>> pt$ sno .=. "S1" .*. sName .=. "Smith" .*. status .=. (20::Integer) .*. city .=. "London" .*. pName .=. "Ratchet" .*. color .=. "Mauve" .*. pno .=. "P9" .*. emptyRecord
+...
+>>> type SNO = Tagged "sno" String
+... etc ...
+>>> pt$ (hEndR $ hBuild "S1" "Smith" 20 "London" "Ratchet" "Mauve" "P9" :: Record '[SNO,SName,Status,City,PName,Color,PNO])
+...
+
+Same result.
+  -}
+  rTuple, rTuple', relation, relation',
+  rHdr, as, nAs,
+  -- * Constants
+  tableDum, tableDee, empty,
+  -- * Support
+  unordRecEq, bodyAsList, relRearrange, relRearrange',
+  -- * Presentation
+  HaskRelTS(HaskRelTS), HListTypeSynonym,
+  rPrint, rPrintTyped, p, pt, rShowType, showRelTab
+    ) where
+
+import Data.Set ( Set, fromList, foldr )
+import qualified Data.Set ( map, empty )
+
+import Data.HList.CommonMain
+
+import Database.HaskRel.HFWTabulation
+import Data.Typeable
+
+
+-- == Definition
+
+-- | A shorthand for "attribute", and a synonym of @Data.Tagged@.
+type Attr = Tagged
+
+-- | A "tuple as defined by the relational model", synonym for @Data.HList.Record@.
+type RTuple = Record
+
+-- | A synonym for @Set ( RTuple a )@.
+type Relation a = Set ( RTuple a )
+
+-- | A shorthand for "relational header", and a synonym of @Data.HList.Record.Labels@. The header of either an r-tuple or a relation in relational theory.
+type RHdr a = Labels a
+
+{-
+Though to make it more concise I'd love to express it something like:
+ :: Relation' '[("sno", String), ("status", Int)]
+-}
+
+-- == Construction.
+
+-- Instances that allow hToTuple and hFromTuple for unary records and labels
+instance HTuple '[Label a] (Label a) where
+    hToTuple (a `HCons` HNil) = a
+    hFromTuple a = a `HCons` HNil
+
+instance HTuple '[Tagged a a'] (Tagged a a') where
+    hToTuple (a `HCons` HNil) = a
+    hFromTuple a = a `HCons` HNil
+
+{-| Constructs an r-tuple from tagged values. Supports only 0 to 6-tuples.
+
+>>> pt$ rTuple (sno .=. "S1", sName .=. "Smith", status .=. (20::Integer), city .=. "London")
+┌───────────────┬─────────────────┬───────────────────┬────────────────┐
+│ sno :: String │ sName :: String │ status :: Integer │ city :: String │
+├───────────────┼─────────────────┼───────────────────┼────────────────┤
+│ S1            │ Smith           │ 20                │ London         │
+└───────────────┴─────────────────┴───────────────────┴────────────────┘
+-}
+rTuple :: (HLabelSet (LabelsOf r), HTuple r t, HAllTaggedLV r) =>
+     t -> RTuple r
+rTuple t = mkRecord $ hFromTuple t
+
+{-| Constructs an r-tuple from a tuples of untagged values, where the labels and exact types are inferred from the context. Supports only 0 to 6-tuples.
+
+>>> pt$ ( rTuple' ("S1", "Smith", 20, "London") :: RTuple '[SNO, SName, Status, City] )
+...
+
+Result as for 'rTuple'.
+-}
+rTuple'
+  :: (RecordValues b, HTuple (RecordValuesR b) t,
+      HMapAux HList TaggedFn (RecordValuesR b) b) =>
+     t -> RTuple b
+rTuple' t = hMapTaggedFn $ hFromTuple t
+
+{-| Construct a relation value from a list of r-tuples of tagged values. Alias of 'Data.Set.fromList' with a result restricted to 'Relation', with a name from relational theory. Supports only 0 to 6-tuples.
+
+>>> :{
+pt$ relation [rTuple (sno .=. "S1", sName .=. "Smith", status .=. (20::Integer), city .=. "London"),
+              rTuple (sno .=. "S2", sName .=. "Jones", status .=. (10::Integer), city .=. "Paris")]
+:}
+┌───────────────┬─────────────────┬───────────────────┬────────────────┐
+│ sno :: String │ sName :: String │ status :: Integer │ city :: String │
+╞═══════════════╪═════════════════╪═══════════════════╪════════════════╡
+│ S1            │ Smith           │ 20                │ London         │
+│ S2            │ Jones           │ 10                │ Paris          │
+└───────────────┴─────────────────┴───────────────────┴────────────────┘
+-}
+relation :: (Ord a, a ~ Record b) => [a] -> Relation b
+relation = fromList
+
+{-| Construct a relation value from a list of tuples of untagged values, where the labels and exact types are inferred from the context. Supports only 0 to 6-tuples.
+
+>>> pt$ ( relation' [("S1", "Smith", 20, "London"), ("S2", "Jones", 10, "Paris")] :: Relation '[SNO, SName, Status, City] )
+
+Result as for 'relation'.
+-}
+relation'
+  :: (Ord (HList b), RecordValues b, HTuple (RecordValuesR b) t,
+      HMapAux HList TaggedFn (RecordValuesR b) b) =>
+     [t] -> Relation b
+relation' = fromList . map rTuple'
+
+relation''
+  :: (Ord (HList b), HLabelSet (LabelsOf b), HTuple b t,
+      HAllTaggedLV b) =>
+     [t] -> Relation b
+relation'' = fromList . map rTuple
+
+
+{-| Alias of @Data.HList.HList.hFromTuple@ with a name that is more descriptive for the purpose of constructing "Labels", which are employed as relational headings, from Haskell tuples of label values. When labels have been defined it permits expressing:
+
+>>> pt$ p `project` (undefined :: Labels '["pno","pName","color"])
+
+As:
+
+>>> pt$ p `project` (rHdr (pno,pName,color))
+
+Supports 0 to 6-tuples.
+-}
+rHdr :: HTuple v t => t -> HList v
+rHdr = hFromTuple
+
+
+-- | Synonym of '.=.', for 'rename' and 'nAs'.
+as :: Label l -> v -> Tagged l v
+as = (.=.)
+
+{-| N-adic constructor of 'as' statements, using @mkRecord . hFromTuple@. Only supports 0 to 6-tuples.
+
+>>> let pnu = Label :: Label "pnu"
+>>> let colour = Label :: Label "colour"
+>>> :t nAs (pno `as` pnu, color `as` colour)
+nAs (pno `as` pnu, color `as` colour)
+  :: Record '[Tagged "pno" (Label "pnu"), Tagged "color" (Label "colour")]
+-}
+nAs :: (HLabelSet (LabelsOf r), HTuple r t, HAllTaggedLV r) =>
+     t -> Record r
+nAs = mkRecord . hFromTuple
+
+
+-- == Supporting functions
+
+-- | Order-agnostic equality operation, which is neccessary for comparison correct for r-tuples.
+unordRecEq
+  :: (Eq (HList l), HRearrange3 (LabelsOf l) r l,
+      HLabelSet (LabelsOf l), SameLength' r l,
+      SameLength' r (LabelsOf l), SameLength' l r,
+      SameLength' (LabelsOf l) r) =>
+     RTuple l -> RTuple r -> Bool
+unordRecEq l r = l == hRearrange' r
+
+
+-- This variant is quite slow, though that should be because of type system issues and not runtime performance; replicate 10 of a comparison has much better performance than repeating it in a 10-tuple.
+unordRecEq'
+  :: (Eq (HList l), HRearrange3 (LabelsOf l) r l,
+      HLabelSet (LabelsOf l), HLabelSet (LabelsOf r),
+      H2ProjectByLabels (LabelsOf l) t r b, SameLength' r l,
+      SameLength' r (LabelsOf l), SameLength' l r,
+      SameLength' (LabelsOf l) r, HAllTaggedLV r) =>
+     RTuple l -> RTuple t -> Bool
+unordRecEq' l r = l == hProjectByLabels' r
+
+-- | Rearrange a set of HList records to context. From the perspective of relational theory this is a presentation function.
+relRearrange
+  :: (Ord (HList l), HRearrange3 (LabelsOf l) r l,
+      HLabelSet (LabelsOf l), SameLength' r l,
+      SameLength' r (LabelsOf l), SameLength' l r,
+      SameLength' (LabelsOf l) r) =>
+     Relation r -> Relation l
+relRearrange = Data.Set.map hRearrange'
+
+-- | Rearrange a set of HList records to the order of a set given by an argument. The value of the second argument will be ignored. From the perspective of relational theory this is a presentation function.
+relRearrange'
+  :: (Ord (HList l), HRearrange3 (LabelsOf l) r l,
+      HLabelSet (LabelsOf l), SameLength' r l,
+      SameLength' r (LabelsOf l), SameLength' l r,
+      SameLength' (LabelsOf l) r) =>
+     Relation r -> Relation l -> Relation l
+relRearrange' rel ord = Data.Set.map hRearrange' rel
+
+-- That ' is swapped between relRearrange and hRearrange is a work related accident and not the way it must be.
+
+rElementType :: Relation r -> RTuple r
+rElementType rel = undefined
+
+
+{-| Gives the body of a relation as a list. This will untag the values. -}
+bodyAsList :: RecordValues r => Relation r -> [HList (RecordValuesR r)]
+bodyAsList = Data.Set.foldr (\t b -> recordValues t : b ) []
+-- TODO: That doesn't work recursively, which it most likely should.
+
+
+
+-- == Constants of relational theory
+
+{- | The nullary relation with an empty body
+
+>>> pt$ tableDum
+┌──┐
+│  │
+╞══╡
+└──┘
+>>> relation [] == tableDum
+True
+-}
+tableDum :: Relation '[]
+tableDum = Data.Set.empty
+
+{- | The nullary relation of cardinality one.
+
+>>> pt$ tableDee
+┌──┐
+│  │
+╞══╡
+│  │
+└──┘
+>>> relation [rTuple ()] == tableDee
+True
+>>> relation' [()] == tableDee
+True
+-}
+tableDee :: Relation '[]
+tableDee = fromList[emptyRecord]
+
+
+-- Redefined and not just reexported to add a bit of documentation
+-- TODO: Check if it's possible to have something that'll work for both tableDum and empty.
+
+{- | The empty set without an explicit type. In a relational context this is a relation with an empty body and no defined heading.
+
+>>> relation [rTuple (sno .=. "S1", status .=. 5)] == empty
+False
+
+Note how the example for `tableDum` won't work for `empty` and vice-versa.
+-}
+empty :: Set a
+empty = Data.Set.empty
+-- TODO: Or :: Relation a?
+
+
+
+-- == Presentation
+
+
+-- | HaskRel type synonyms
+data HaskRelTS = HaskRelTS
+
+-- | HaskRel type synonyms
+instance HListTypeSynonym HaskRelTS where
+  hRecTS _ = "RTuple"
+  hRecSetTS _ = "Relation"
+  hTIPTS _ = "RTuple"
+  hTIPSetTS _ = "Relation"
+
+
+-- | Prints a tabular representation of an r-tuple or relation.
+rPrint :: HFWPresent r => r -> IO ()
+rPrint = hfwPrint
+
+-- | Prints a tabular representation of an r-tuple or relation, with type information.
+rPrintTyped :: HFWPresent r => r -> IO ()
+rPrintTyped = hfwPrintTypedTS HaskRelTS
+
+-- | Synonym of `rPrint`.
+p :: HFWPresent r => r -> IO ()
+p = rPrint
+
+-- | Synonym of `rPrintTyped`.
+pt :: HFWPresent r => r -> IO ()
+pt = rPrintTyped
+
+-- | Specialization of @Database.HaskRel.HFWTabulation.showHTypeTS@ that employs HaskRel specific type-synonyms.
+rShowType :: TypeRep -> String
+rShowType = showHTypeTS HaskRelTS
+
+
+-- Redefined for prettier signatures.
+-- | Shows a tabular representation of a relation.
+showRelTab ::
+     (Typeable a, RecordValues a,
+      HFoldr (Mapcar HPresentRecAttr) [[String]] (RecordValuesR a) [[String]]) =>
+     Relation a -> String
+showRelTab = showHRecSetTab
diff --git a/src/Database/HaskRel/Relational/Expression.hs b/src/Database/HaskRel/Relational/Expression.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/HaskRel/Relational/Expression.hs
@@ -0,0 +1,1077 @@
+{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, FlexibleContexts, FlexibleInstances, UndecidableInstances, PolyKinds #-}
+{-# LANGUAGE DataKinds, TypeOperators #-}
+
+{-|
+Module      : Database.HaskRel.Relational.Expression
+Description : Support for relational expressions
+Copyright   : © Thor Michael Støre, 2015
+License     : GPL v2 without "any later version" clause
+Maintainer  : thormichael át gmail døt com
+Stability   : experimental
+
+"Database.HaskRel.Relational.Algebra" and "Database.HaskRel.Relational.Assignment" defines the functions of the relational algebra and relational assignment, but in order to keep pertinent concerns separated it only defines functions for relational operations that reference values, not relation variables. This module redefines those functions, generalizing them such that they operate upon relation values, relation variables and relational IO (relational expressions that build upon relvars), and also adds 'HFWPresent' instances for relational IO.
+
+Running "examples/suppliersPartsExample.sh" starts a GHCi session where these examples can be run.
+-}
+module Database.HaskRel.Relational.Expression (
+  -- * Functions defined according to the definition of monadic operators in relational theory
+  {-| (Not to be confused with Haskell monads.) -}
+  -- ** The monadic operator class
+  MonOp (monOp), MonOpRes, MonOpArg,
+  -- ** The functions defined as monadic operators in the relational algebra
+  rename, extend, restrict, project, projectAllBut,
+  group, groupAllBut, ungroup,
+  -- ** Supplementary functions
+  -- *** Specializations of functions of the relational model, with relational closure
+  -- **** Not part of relational theory
+  dExtend, extendA, dExtendA, renameA, aSummarize, imageExtendL,
+  -- *** Without relational closure
+  image, member, notMember,
+  -- **** Not part of relational theory
+  rafoldr, rafoldrU, agg, aggU, count, isEmpty,
+  rAgg, rAggU,
+  -- * Functions defined according to the definition of dyadic operators in relational theory
+  -- ** The dyadic operator class
+  DyaOp, DyaOpRes, DyaOpLeft, DyaOpRight, dyaOp,
+  -- ** The functions defined as dyadic operators in the relational algebra
+  naturalJoin, nJoin, times, matching, semiJoin, notMatching,
+  semiDiff, union, dUnion, intersect, minus, xUnion, isProperSubsetOf,
+  isSubsetOf, rEq,
+  -- ** Somewhat deprecated operators of the relational algebra
+  summarize,
+  -- ** Specializations of functions of the relational model, with relational closure
+  -- **** Not part of relational theory
+  interJoin, iJoin,
+  -- * Assignment functions
+  -- ** The assignment operator class
+  RelAssign (relAssign), RelAssignArg,
+  -- ** The primitive assignment function
+  assign,
+  -- ** Specialized assignment functions
+  insert, dInsert, delete, iDelete,
+  -- update[A], updateAll[A] and deleteP only take relvars and optionally predicates as arguments, and not relation values, and are as such not re-defined in this module, but are re-exported for completeness
+  Assignment.deleteP, Assignment.update, Assignment.updateAll,
+  -- ** Further specialized and simplified forms of update
+  -- **** Not part of relational theory
+  Assignment.updateA, Assignment.updateAllA,
+  -- ** Additional classes
+  Algebra.NotEmpty
+      ) where
+
+import Data.Set (Set)
+import qualified Data.Set (member, notMember)
+
+import Data.HList.CommonMain
+
+import Database.HaskRel.HFWTabulation
+  ( HFWPresent, HListTypeSynonym, hfwPrint, hfwPrintTypedTS,
+    printHRecSetTab, printHRecSetTabTyped, printHRecSetTabTypedTS )
+
+import Database.HaskRel.Relational.Definition
+import qualified Database.HaskRel.Relational.Algebra as Algebra
+import qualified Database.HaskRel.Relational.Assignment as Assignment
+import Database.HaskRel.Relational.Variable ( Relvar, readRelvar )
+
+
+instance ( HFWPresent ( Relation r ) ) =>
+         HFWPresent ( IO ( Relation r ) )
+    where
+      hfwPrint r = r >>= hfwPrint
+      hfwPrintTypedTS ts r = r >>= hfwPrintTypedTS ts
+
+
+-- | The class of relational monadic operators
+class MonOp a where
+    type MonOpRes a res :: *
+    type MonOpRes a res = IO res
+    type MonOpArg a :: *
+    -- | Unary relational function application.
+    monOp :: (MonOpArg a -> res) -> a -> MonOpRes a res
+-- Alternatively, enforcing relational closure:
+--    monOp :: (MonOpArg a -> (Relation res)) -> a -> (MonOpRes a (Relation res))
+-- But it's convenient to also employ this for aggregating functions
+-- TODO: This resulted in IO (IO a) at some point, should GHCi warn about that? Or if main results in this, for that matter.
+
+instance MonOp (Relation a) where
+    type MonOpRes (Relation a) res = res
+    type MonOpArg (Relation a) = Relation a
+    monOp = id
+
+instance MonOp (IO (Relation a)) where
+    type MonOpArg (IO (Relation a)) = Relation a
+    monOp = fmap
+
+instance (Ord (HList b), Read (HList (RecordValuesR b)), RecordValues b,
+          HMapAux HList TaggedFn (RecordValuesR b) b) =>
+         MonOp (Relvar b) where
+    type MonOpArg (Relvar b) = Relation b
+    monOp f r = f <$> readRelvar r
+
+
+{- By always resulting in IO we get a simpler variant. -}
+class MonOp' a where
+    type MonOpArg' a :: *
+    monOp' :: (MonOpArg' a -> (Relation res)) -> a -> (IO (Relation res))
+
+instance MonOp' (Relation a) where
+    type MonOpArg' (Relation a) = Relation a
+    monOp' = (pure .)
+
+instance MonOp' (IO (Relation a)) where
+    type MonOpArg' (IO (Relation a)) = Relation a
+    monOp' = fmap
+
+instance (Ord (HList b), Read (HList (RecordValuesR b)), RecordValues b,
+          HMapAux HList TaggedFn (RecordValuesR b) b) =>
+         MonOp' (Relvar b) where
+    type MonOpArg' (Relvar b) = Relation b
+    monOp' f r = f <$> readRelvar r
+
+-- The "values in, value out" variation allows for the same functions to be used inside the functions that rename and extends takes, but this form is necessary in certain cases; see 'rename' below, and the TODO to fix this.
+
+
+
+{-| Rename given attributes of a relation.
+
+>>> let pnu = Label :: Label "pnu"
+>>> let colour = Label :: Label "colour"
+>>> rPrint$ p `rename` nAs( pno `as` pnu, color `as` colour )
+┌─────┬───────┬────────┬────────┬────────┐
+│ pnu │ pName │ colour │ weight │ city   │
+╞═════╪═══════╪════════╪════════╪════════╡
+│ P1  │ Nut   │ Red    │ 12 % 1 │ London │
+...
+
+Note that due to an implementation disorder this always results in an IO operation, even on values. This is not an intentional limit and will hopefully be removed in the future. If this is not acceptable (for instance inside 'extend' and 'restrict' functions), then one has to rely on 'renameA', which renames a single attribute.
+-}
+rename r l = monOp' (\r' -> Algebra.rename r' l) r
+{- TODO: Figure out why using monOp instead of monOp' breaks down with: Could not deduce (MonOpRes a (Relation r) ~ MonOpRes a (Relation r0))
+
+This is annoying, since applying it directly in GHCi works:
+
+import qualified Database.HaskRel.Relational.Algebra as Algebra (rename, as)
+let pnu = Label :: Label "pnu"
+let colour = Label :: Label "colour"
+rPrint$ monOp (\r' -> Algebra.rename r' ( nAs( pno `as` pnu, color `as` colour ) ) ) p 
+-> Great success printed here.
+
+This doesn't fly either:
+rename' r l = monOp (\r' -> Algebra.rename' r' l) r
+
+Still breaks down with a signature and AllowAmbiguousTypes:
+
+rename' :: forall a (a1 :: [*]) tr (r :: [*]).
+    (Ord (HList r), HLabelSet (LabelsOf r),
+     HMapAux HList (Algebra.Relabel tr) a1 r, SameLength' a1 r,
+     SameLength' r a1, HAllTaggedLV r, MonOp a,
+     MonOpArg a ~ Relation a1) =>
+    a -> tr -> MonOpRes a (Relation r)
+rename' r l = monOp (\r' -> Algebra.rename r' l) r
+
+Does this require injective type families? 'res' should be possible to deduce.
+-}
+
+{-| Renames one attribute.
+
+>>> let sCity = Label :: Label "sCity"
+>>> rPrint$ s `renameA` (city `as` sCity)
+┌────────┬─────┬───────┬────────┐
+│ sCity  │ sno │ sName │ status │
+╞════════╪═════╪═══════╪════════╡
+│ Athens │ S5  │ Adams │ 30     │
+│ London │ S1  │ Smith │ 20     │
+│ London │ S4  │ Clark │ 20     │
+│ Paris  │ S2  │ Jones │ 10     │
+│ Paris  │ S3  │ Blake │ 30     │
+└────────┴─────┴───────┴────────┘
+
+This only accepts a single pair of labels, the label to rename and the new label, in contrast to Tutorial D rename which takes a set of from-to pairs.
+
+@renameA@ can, unlike 'rename', be used by 'restrict' and 'extend':
+
+>>> :{
+  do spx <- readRelvar sp
+     rPrint$ sp `restrict` (\( image -> ii ) ->
+                            count ( ii $ renameA (renameA spx (sno `as` sn)) (pno `as` pn) )
+                            > 2)
+:}
+...
+-}
+renameA r ft = monOp (\r' -> Algebra.renameA r' ft) r
+
+
+{-|
+Extends the given relation with the r-tuple resulting from the second argument. Existing attributes with the same name will be replaced.
+
+The simplest form (aside from a no-op), extend with one attribute:
+
+>>> rPrint$ extend p (\ [pun|weight|] -> (Label :: Label "gmwt") .=. weight * 454 .*. emptyRecord )
+┌──────────┬─────┬───────┬───────┬────────┬────────┐
+│ gmwt     │ pno │ pName │ color │ weight │ city   │
+╞══════════╪═════╪═══════╪═══════╪════════╪════════╡
+│ 5448 % 1 │ P1  │ Nut   │ Red   │ 12 % 1 │ London │
+...
+│ 8626 % 1 │ P6  │ Cog   │ Red   │ 19 % 1 │ London │
+└──────────┴─────┴───────┴───────┴────────┴────────┘
+
+When replacing an attribute with extend one must take care not to cause a naming collision. Using pattern matching with @case ... of ...@ one can pass values from one context to another with Haskell tuples, and reuse variable names, although this does require some duplication. It is also possible to use @pun@ to build the output, instead of @.*.@ and @emptyRecord@. Add one attribute, replace another:
+
+>>> rPrint$ extend p (\[pun|weight color|] -> case (weight + 10, color ++ "-ish") of (weight, altColor) -> [pun|weight altColor|])
+┌────────┬───────────┬─────┬───────┬───────┬────────┐
+│ weight │ altColor  │ pno │ pName │ color │ city   │
+╞════════╪═══════════╪═════╪═══════╪═══════╪════════╡
+│ 22 % 1 │ Blue-ish  │ P5  │ Cam   │ Blue  │ Paris  │
+...
+│ 29 % 1 │ Red-ish   │ P6  │ Cog   │ Red   │ London │
+└────────┴───────────┴─────┴───────┴───────┴────────┘
+
+Lining this up with the @EXTEND@ operator of Tutorial D, we can imagine @ case (a, b) of (a', b') @ as a form of @ { a' := a , b' := b } @ (though we can hardly equate them), while @pun@ is needed to unpack and pack this from and to the r-tuples.
+
+Also note that if an attribute is replaced then the cardinality of the result will be equal or lower than that of the argument.
+
+>>> count sp
+12
+>>> count $ sp `extend` (\_ -> sno .=. "S0" .*. pno .=. "P0" .*. emptyRecord)
+4
+
+It is also notable that since HaskRel is not based on SQL but on relational theory as defined by Chris Date et al today, and explicitly does not have support for nulls and outer joins (as specified in [1] chapter 4), @extend@ is employed to assemble the information SQL assembles with @OUTER JOIN@. The following command (a variant of the first query on [1] page 154) gives a result that includes the information given by SQL @RIGHT OUTER JOIN@:
+
+>>> :{
+do sp' <- readRelvar sp
+   rPrint$ extend s (\ (image -> ii) -> pq .=. ii sp' .*. emptyRecord)
+:}
+┌───────────────┬─────┬───────┬────────┬────────┐
+│ pq            │ sno │ sName │ status │ city   │
+╞═══════════════╪═════╪═══════╪════════╪════════╡
+│ ┌─────┬─────┐ │ S5  │ Adams │ 30     │ Athens │
+│ │ pno │ qty │ │     │       │        │        │
+│ ╞═════╪═════╡ │     │       │        │        │
+│ └─────┴─────┘ │     │       │        │        │
+│ ┌─────┬─────┐ │ S1  │ Smith │ 20     │ London │
+│ │ pno │ qty │ │     │       │        │        │
+│ ╞═════╪═════╡ │     │       │        │        │
+│ │ P1  │ 300 │ │     │       │        │        │
+│ │ P2  │ 200 │ │     │       │        │        │
+...
+
+See material about extend, image relations and RVAs in [1] chapter 7 for more.
+
+Note the additional plumbing required to employ relvars inside the function @extend@ takes; the function 'imageExtendL' has been created to provide a more convenient way to express this, specializing upon @extend@ and 'image'.
+-}
+extend r f = monOp (`Algebra.extend` f) r
+
+{- TODO: Is it possible to have a quasiquoter that lets one specify roughly the same as the Tutorial D snippet mentioned in the documentation above? For instance instead of:
+(\[pun|weight color|] -> case (weight + 10, color ++ "-ish") of (weight, altColor) -> [pun|weight altColor|])
+
+Having something like:
+[rx| weight := weight + 10, altColor := color ++ "-ish" |]
+
+That would also render extendA/dExtendA obsolete, tidying things up nicely.
+-}
+
+{-| Extends the given relation with the attribute resulting from the second argument. If an attribute with the same name exists then it will be replaced. This allows for the function of the second argument to be simpler.
+
+Where @c@ is an expression yielding a single attribute:
+
+>>> extend a (\b -> c .*. emptyRecord)
+
+Is equivalent to:
+
+>>> extendA a (\b -> c)
+
+The following has the same result as the first example for 'extend':
+
+>>> let gmwt = (Label::Label "gmwt")
+>>> rPrint$ extendA p (\[pun|weight|] -> gmwt .=. weight * 454)
+
+Note that if one wants to alter the values of an existing attribute then one has to avoid a name collision. The most convenient option will most often be having a constructor function or label constant with a different name from the actual label:
+
+>>> let _weight a = (Label::Label "weight") .=. a
+>>> rPrint$ extendA p (\[pun|weight|] -> _weight $ weight + 10)
+-}
+extendA r f = monOp (`Algebra.extendA` f) r
+{-
+Alternatively, perform the pattern matching without \"pun\", which allows different variable names from the function names:
+
+>>> rPrint$ extendA p' (\ ( hProjectByLabels' -> ( Record ( ( Tagged weight' :: Tagged "weight" Rational ) `HCons` HNil ) ) ) -> weight .=. weight' )
+-}
+-- TODO: The issue mentioned above could perhaps be solved by making pun create variables that can serve both as data and as constructors. See also https://hackage.haskell.org/package/HList/docs/Data-HList-Labelable.html
+
+{-|
+Disjoint extension. Extends the given relation with the result of the second argument, as 'extend', but without deleting any that exist. 
+-}
+dExtend r f = monOp (`Algebra.dExtend` f) r
+
+{-|
+Disjoint extension of a single attribute. Extends the given relation with the result of the second argument, as 'extend', but without deleting any that exist. @l@ cannot already have any attribute @e@.
+-}
+dExtendA r f = monOp (`Algebra.dExtendA` f) r
+
+
+{-|
+Restricts the given relation according to the given predicate. Note that this is the well known @WHERE@ operator of both SQL and Tutorial D, but since "where" is a reserved keyword in Haskell it is named "restrict".
+
+>>> rPrint$ p `restrict` (\[pun|weight|] -> weight < 17.5)
+┌─────┬───────┬───────┬────────┬────────┐
+│ pno │ pName │ color │ weight │ city   │
+╞═════╪═══════╪═══════╪════════╪════════╡
+│ P1  │ Nut   │ Red   │ 12 % 1 │ London │
+...
+│ P5  │ Cam   │ Blue  │ 12 % 1 │ Paris  │
+└─────┴───────┴───────┴────────┴────────┘
+-}
+restrict r f = monOp (`Algebra.restrict` f) r
+
+
+{-| Projects the given relation on the given heading.
+
+>>> rPrint$ p `project` (rHdr (color,city))
+┌───────┬────────┐
+│ color │ city   │
+╞═══════╪════════╡
+│ Blue  │ Oslo   │
+│ Blue  │ Paris  │
+│ Green │ Paris  │
+│ Red   │ London │
+└───────┴────────┘
+-}
+project r a = monOp (`Algebra.project` a) r
+-- TODO: project/projectAllBut must fail when it is given labels that don't exist in the given relation, right now it accepts all sorts of nonesense without complaining.
+
+{-| Projects the given relation on the heading of said given relation minus the given heading.
+
+>>> rPrint$ p `projectAllBut` (rHdr (city))
+┌─────┬───────┬───────┬────────┐
+│ pno │ pName │ color │ weight │
+╞═════╪═══════╪═══════╪════════╡
+│ P1  │ Nut   │ Red   │ 12 % 1 │
+│ P2  │ Bolt  │ Green │ 17 % 1 │
+│ P3  │ Screw │ Blue  │ 17 % 1 │
+│ P4  │ Screw │ Red   │ 14 % 1 │
+│ P5  │ Cam   │ Blue  │ 12 % 1 │
+│ P6  │ Cog   │ Red   │ 19 % 1 │
+└─────┴───────┴───────┴────────┘
+-}
+projectAllBut r a = monOp (`Algebra.projectAllBut` a) r
+
+
+{-| Groups the given attributes of the given relation into a given new relation valued attribute.
+
+As the Tutorial D GROUP operator, not SQL GROUP BY.
+
+>>> let pq = (Label :: Label "pq")
+>>> pt$ group sp (rHdr (pno,qty)) (pq .=.)
+┌────────────────────────────────────┬───────────────┐
+│ pq :: Relation '["pno","qty"]      │ sno :: String │
+╞════════════════════════════════════╪═══════════════╡
+│ ┌───────────────┬────────────────┐ │ S1            │
+│ │ pno :: String │ qty :: Integer │ │               │
+│ ╞═══════════════╪════════════════╡ │               │
+│ │ P1            │ 300            │ │               │
+...
+└────────────────────────────────────┴───────────────┘
+
+Note that the last argument is a function that tags any value with a label; an attribute constructor. This is different from Tutorial D @GROUP@, which just takes the equivalent of a label, but as long as an attribute constructor is provided it will function the same way. Here is what we get if we aggregate the relation we get as the argument to the receiving function with 'agg', instead of just supplying an attribute constructor ("@(pq .=.)@" above):
+
+>>> let qtys = (Label :: Label "qtys")
+>>> pt$ group sp (rHdr (pno,qty))
+                 ((qtys .=.) . agg qty)
+┌───────────────────────────┬───────────────┐
+│ qtys :: [Integer]         │ sno :: String │
+╞═══════════════════════════╪═══════════════╡
+│ [200]                     │ S3            │
+│ [200,300,400]             │ S4            │
+│ [300,200,400,200,100,100] │ S1            │
+│ [300,400]                 │ S2            │
+└───────────────────────────┴───────────────┘
+
+"Get the quantities of items in stock for those suppliers that supply anything":
+
+>>> pt$ group sp (rHdr (pno,qty)) ((qtys .=.) . sum . agg qty)
+┌─────────────────┬───────────────┐
+│ qtys :: Integer │ sno :: String │
+╞═════════════════╪═══════════════╡
+│ 200             │ S3            │
+│ 700             │ S2            │
+│ 900             │ S4            │
+│ 1300            │ S1            │
+└─────────────────┴───────────────┘
+
+Note the difference between this and the example for 'image'. These last two examples may be more clearly expressed with 'groupAllBut', since we then specify the attributes that the resulting type will have.
+-}
+group rel attsIn fOut = monOp (\r' -> Algebra.group r' attsIn fOut) rel
+
+{-| Groups the given relation on all but the given attributes into a given new attribute.
+
+>>> pt$ groupAllBut sp (rHdr (sno)) (pq .=.)
+
+Same result as the first example for 'group'.
+
+>>> pt$ groupAllBut sp (rHdr (sno)) ((qtys .=.) . sum . agg qty )
+
+Same result as the last example for 'group'.
+-}
+groupAllBut rel attsIn attOut = monOp (\r' -> Algebra.groupAllBut r' attsIn attOut) rel
+
+{-| Ungroups the given relation valued attribute of the given relation.
+
+>>> sp `rEq` ungroup ( group sp (rHdr (pno,qty)) (pq .=.)) (undefined :: Label "pq")
+True
+-}
+ungroup r a = monOp (`Algebra.ungroup` a) r
+
+
+{-| Self-summarization, the special case of `summarize` where the source and target relations is the same. This is closer to SQL GROUP BY.
+
+>>> pt$ aSummarize sp (rHdr (pno,qty)) (\r -> qty .=. sum ( agg qty r ) .*. emptyRecord)
+
+Same result as last example for 'group'.
+-}
+aSummarize rel attsIn fOut = monOp (\r' -> Algebra.aSummarize r' attsIn fOut) rel
+
+
+
+{-| Gives the cardinality of the argument.
+
+>>> count sp
+12
+-}
+count :: (MonOp a, MonOpArg a ~ Set a1) => a -> MonOpRes a Int
+count = monOp Algebra.count
+
+{-| Gives whether the given argument is empty or not.
+
+>>> isEmpty sp
+False
+-}
+isEmpty :: (MonOp a, MonOpArg a ~ Set a1) => a -> MonOpRes a Bool
+isEmpty = monOp Algebra.isEmpty
+
+-- TODO: Figure out how all this will function when aggregating values into new relations. That'll most likely happen in an extend clause, where IO support is irrelevant.
+{-| Right-fold of an attribute of a relation (although a "right" fold doesn't make sense in the context of the relational model). Note that the value of the third argument is not used and may be "undefined".
+
+>>> rafoldr (+) 0 qty sp
+3100
+>>> rafoldr (*) 1 qty sp
+27648000000000000000000000000
+-}
+rafoldr f b a r = monOp (Algebra.rafoldr f b a) r
+
+{-| Attribute value aggregation, a specialization of 'rafoldr' that aggregates the values of a single attribute into a list of the values the attribute type wraps.
+
+Note that the value of the first argument is not used and may be "undefined".
+
+>>> :{
+ do sp' <- readRelvar sp
+    putStrLn $ show $ sum $ agg qty sp'
+:}
+3100
+-}
+agg :: (Foldable t, HasField l a1 a2, MonOp a, MonOpArg a ~ t a1) =>
+     Label l -> a -> MonOpRes a [a2]
+agg = monOp . Algebra.agg
+
+{-| Right-fold of the attribute of a unary relation.
+
+>>> rafoldrU (+) 0 $ sp `project` (rHdr (qty))
+1000
+>>> rafoldrU (*) 1 $ sp `project` (rHdr (qty))
+2400000000
+-}
+rafoldrU f b r = monOp (Algebra.rafoldrU f b) r
+
+{-| Aggregation of the single attribute of a unary relation. A specialization of 'agg', and thus in turn of 'rafoldr', that aggregates the single attribute of a unary relation, without requiring the name of that attribute.
+
+>>> :{
+ do sp' <- readRelvar sp
+    putStrLn $ show $ sum $ aggU $ sp' `project` (rHdr (qty))
+ :}
+1000
+-}
+aggU :: (Foldable t, MonOp a,
+      MonOpArg a ~ t (Record '[Tagged t1 a1])) =>
+     a -> MonOpRes a [a1]
+aggU = monOp Algebra.aggU
+
+{-| Aggregates an attribute and applies a function to the result of that. A specialization of `rafoldr`.
+
+Note that the value of the first argument is not used and may be "undefined".
+
+>>> rAgg qty sp sum
+3100
+-}
+rAgg :: (Foldable t, HasField l a1 a2, MonOp a, MonOpArg a ~ t a1) =>
+     Label l -> a -> ([a2] -> res) -> MonOpRes a res
+rAgg a r f = monOp (f . Algebra.agg a) r
+
+{-| Aggregates the attribute of a unary relation and applies a function to the result of that. A specialization of `rafoldrU`.
+
+>>> rAggU (sp `project` (rHdr (qty))) sum
+1000
+-}
+rAggU r f = monOp (f . Algebra.aggU) r
+
+-- TODO: Can this be made to work not just towards an IO(Relation a) but also from it?
+{-| The image of a relation corresponding to an r-tuple.
+
+An application of the first argument only, an r-tuple, to this function yields what is known as the @!!@ operator in Tutorial D.
+
+>>> rPrint$ rTuple (sno .=. "S2", pno .=. "P1")
+┌─────┬─────┐
+│ sno │ pno │
+├─────┼─────┤
+│ S2  │ P1  │
+└─────┴─────┘
+>>> rPrint$ rTuple (sno .=. "S2", pName .=. "Nut")
+┌─────┬───────┐
+│ sno │ pName │
+├─────┼───────┤
+│ S2  │ Nut   │
+└─────┴───────┘
+>>> rPrint$ rTuple (sno .=. "S2", pno .=. "P1") `image` sp
+┌─────┐
+│ qty │
+╞═════╡
+│ 300 │
+└─────┘
+>>> rPrint$ rTuple (sno .=. "S2", pName .=. "Nut") `image` sp
+┌─────┬─────┐
+│ pno │ qty │
+╞═════╪═════╡
+│ P1  │ 300 │
+│ P2  │ 400 │
+└─────┴─────┘
+
+Image relations give rise to summarization. Here is a form of the query, "get the quantities of items in stock for all suppliers":
+
+>>> :{
+do sp' <- readRelvar sp
+   rPrint$ s `project` (rHdr (sno))
+             `extendA` (\ (image -> ii) ->
+                          (Label::Label "qtySum") .=. ( sum $ agg qty $ ii sp' ) )
+:}
+┌────────┬─────┐
+│ qtySum │ sno │
+╞════════╪═════╡
+│ 0      │ S5  │
+│ 200    │ S3  │
+│ 700    │ S2  │
+│ 900    │ S4  │
+│ 1300   │ S1  │
+└────────┴─────┘
+
+Note how view patterns are used to build the @ii@ operator, equivalent of Tutorial D's @!!@ operator. An equivalent form of the lambda would be:
+
+@
+   (\\t -> (Label::Label "qtySum") .=. ( sum $ agg qty $ t \`image\` sp' ))
+@
+
+See `group` for a similar example.
+-}
+image t r = monOp (Algebra.image t) r
+{- With FlexibleContexts and TypeFamilies the above could be expressed:
+:{
+do sp' <- readRelvar sp
+   rPrint$ s `project` (rHdr (sno))
+             `extendA` (\t -> ( let ii = image t
+                                 in (Label::Label "qtySum") .=. ( sum $ agg qty $ ii sp' ) ) )
+:}
+-}
+
+
+{-| Gives whether a given r-tuple is member of a given relation.
+
+>>> member (rTuple(sno .=. "S3", qty .=. 200, pno .=. "P2")) sp
+True
+-}
+member e r = monOp (Data.Set.member $ hRearrange' e) r
+
+{-| Gives whether a given r-tuple is not a member of a given relation.
+
+>>> notMember (rTuple(sno .=. "S3", qty .=. 200, pno .=. "P2")) sp
+False
+-}
+notMember e r = monOp (Data.Set.notMember $ hRearrange' e) r
+
+
+
+{- TODO: Is there a way to cut down on the number of instances? Building the dyadic operator class directly on the monadic one doesn't work, the following dyaOp'' definition compiles, but using it with nJoin'' breaks down in ambiguity.
+
+dyaOp''
+  :: (MonOp a, MonOp a1, MonOpRes a1 res1 ~ (MonOpArg a -> res)) =>
+     (MonOpArg a1 -> res1) -> a1 -> a -> MonOpRes a res
+dyaOp'' f r1 r2 = monOp ( monOp f r1 ) r2
+
+-- nJoin'' :: ???
+nJoin'' r1 r2 = dyaOp'' Algebra.nJoin r1 r2
+-}
+
+-- | The class of relational dyadic operators
+class DyaOp a b where
+    type DyaOpRes a b res :: *
+    type DyaOpRes a b res = IO res
+    type DyaOpLeft  a :: *
+    type DyaOpRight b :: *
+    dyaOp' :: (DyaOpLeft a -> DyaOpRight b -> res) -> a -> b -> DyaOpRes a b res
+
+instance DyaOp (Relation a) (Relation b) where
+    type DyaOpRes (Relation a) (Relation b) res = res
+    type DyaOpLeft  (Relation a) = Relation a
+    type DyaOpRight (Relation b) = Relation b
+    dyaOp' = id
+
+instance DyaOp (IO (Relation a)) (Relation b) where
+    type DyaOpLeft  (IO (Relation a)) = Relation a
+    type DyaOpRight (Relation b) = Relation b
+    dyaOp' f r1 r2 = (`f` r2) <$> r1
+
+instance DyaOp (Relation a) (IO (Relation b)) where
+    type DyaOpLeft  (Relation a) = Relation a
+    type DyaOpRight (IO (Relation b)) = Relation b
+    dyaOp' f r1 r2 = f r1 <$> r2
+
+instance DyaOp (IO (Relation a)) (IO (Relation b)) where
+    type DyaOpLeft  (IO (Relation a)) = Relation a
+    type DyaOpRight (IO (Relation b)) = Relation b
+    dyaOp' f r1 r2 = f <$> r1 <*> r2
+
+instance (Ord (HList b), Read (HList (RecordValuesR b)), RecordValues b,
+          HMapAux HList TaggedFn (RecordValuesR b) b) =>
+         DyaOp (Relation a) (Relvar b) where
+    type DyaOpLeft  (Relation a) = Relation a
+    type DyaOpRight (Relvar b) = Relation b
+    dyaOp' f r1 r2 = f r1 <$> readRelvar r2
+
+instance (Ord (HList a), Read (HList (RecordValuesR a)), RecordValues a,
+          HMapAux HList TaggedFn (RecordValuesR a) a) =>
+         DyaOp (Relvar a) (Relation b) where
+    type DyaOpLeft  (Relvar a) = Relation a
+    type DyaOpRight (Relation b) = Relation b
+    dyaOp' f r1 r2 = (`f` r2) <$> readRelvar r1
+
+instance (Ord (HList a), Read (HList (RecordValuesR a)), RecordValues a,
+          HMapAux HList TaggedFn (RecordValuesR a) a) =>
+         DyaOp (Relvar a) (IO (Relation b)) where
+    type DyaOpLeft  (Relvar a) = Relation a
+    type DyaOpRight (IO (Relation b)) = Relation b
+    dyaOp' f r1 r2 = f <$> readRelvar r1 <*> r2
+
+instance (Ord (HList b), Read (HList (RecordValuesR b)), RecordValues b,
+          HMapAux HList TaggedFn (RecordValuesR b) b) =>
+         DyaOp (IO (Relation a)) (Relvar b) where
+    type DyaOpLeft (IO (Relation a)) = Relation a
+    type DyaOpRight (Relvar b)     = Relation b
+    dyaOp' f r1 r2 = f <$> r1 <*> readRelvar r2
+
+instance (Ord (HList a), Ord (HList b), Read (HList (RecordValuesR a)),
+          Read (HList (RecordValuesR b)), RecordValues a, RecordValues b,
+          HMapAux HList TaggedFn (RecordValuesR a) a,
+          HMapAux HList TaggedFn (RecordValuesR b) b) =>
+         DyaOp (Relvar a) (Relvar b) where
+    type DyaOpLeft  (Relvar a) = Relation a
+    type DyaOpRight (Relvar b) = Relation b
+    dyaOp' f r1 r2 = f <$> readRelvar r1 <*> readRelvar r2
+
+-- TODO: Polyvariadic forms of the dyadic functions.
+
+-- The algebra functions do relRearrange themselves, so don't do that in the class function but define a separate function for that. This is the only reason for this, so there's no need for the same with monOp, that can be exported as-is.
+
+{-| Binary relational function application.
+
+>>> let newSups = ( relation [rTuple (sno .=. "S6", sName .=. "Nena", city .=. "Berlin", status .=. 40)] )
+>>> dyaOp (/=) s newSups
+True
+-}
+dyaOp :: (Ord (HList l), HRearrange3 (LabelsOf l) r l,
+          HLabelSet (LabelsOf l), SameLength' r l,
+          SameLength' r (LabelsOf l), SameLength' l r,
+          SameLength' (LabelsOf l) r, DyaOp a b,
+          DyaOpRight b ~ Relation r) =>
+     (DyaOpLeft a -> Relation l -> res) -> a -> b -> DyaOpRes a b res
+dyaOp f r1 r2 = dyaOp' (\r1' r2' -> f r1' ( relRearrange r2' )) r1 r2
+
+{-| Relational equality.
+
+>>> sp `rEq` (relation [rTuple(sno .=. "S2", qty .=. 400, pno .=. "P2")])
+False
+-}
+rEq :: (Ord (HList l), HRearrange3 (LabelsOf l) r l,
+        HLabelSet (LabelsOf l), SameLength' r l,
+        SameLength' r (LabelsOf l), SameLength' l r,
+        SameLength' (LabelsOf l) r, DyaOp a b,
+        DyaOpLeft a ~ Relation l, DyaOpRight b ~ Relation r) =>
+     a -> b -> DyaOpRes a b Bool
+rEq = dyaOp (==)
+-- TODO: Oh great, now I need an IO version of restrict. This is tricky, my first thought is that a predicate for 'filter' will still take a regular value as before but may result in an IO Bool instead of Bool, so perhaps you need to do something like :: ( a -> f b ) -> f ( a -> b )
+
+{-| The natural join of the two given relations.
+
+>>> rPrint$ sp `naturalJoin` s
+┌─────┬─────┬─────┬───────┬────────┬────────┐
+│ sno │ pno │ qty │ sName │ status │ city   │
+╞═════╪═════╪═════╪═══════╪════════╪════════╡
+│ S1  │ P1  │ 300 │ Smith │ 20     │ London │
+...
+│ S4  │ P5  │ 400 │ Clark │ 20     │ London │
+└─────┴─────┴─────┴───────┴────────┴────────┘
+-}
+naturalJoin r1 r2 = dyaOp' Algebra.naturalJoin r1 r2
+
+-- | Alias of 'naturalJoin'.
+nJoin r1 r2 = dyaOp' Algebra.nJoin r1 r2
+
+
+{-| The cartesian product of two relations. A specialized natural join; the natural join between two relations with disjoint headings.
+
+>>> rPrint$ ( sp `projectAllBut` (rHdr (city)) ) `times` ( s `projectAllBut` (rHdr (city)) )
+...
+    No instance for (Fail (DuplicatedLabel (Label "sno")))
+      arising from a use of ‘times’
+
+>>> rPrint$ ( sp `projectAllBut` (rHdr (sno)) ) `times` ( s `projectAllBut` (rHdr (sno)) )
+┌─────┬─────┬───────┬────────┬────────┐
+│ pno │ qty │ sName │ status │ city   │
+╞═════╪═════╪═══════╪════════╪════════╡
+│ P1  │ 300 │ Adams │ 30     │ Athens │
+│ P1  │ 300 │ Blake │ 30     │ Paris  │
+...
+│ P6  │ 100 │ Jones │ 10     │ Paris  │
+│ P6  │ 100 │ Smith │ 20     │ London │
+└─────┴─────┴───────┴────────┴────────┘
+-}
+times r1 r2 = dyaOp' Algebra.times r1 r2
+
+{-| The natural join between two relations with intersecting headings. A specialized natural join.
+
+A join upon relations r1, r2 where the intersection of the heading of r1 and of r2 is not empty; the headings are not disjoint. This is a complement of 'times' within natural join; all that would be disallowed for @times@ is allowed here and vice-versa. The name is what I quickly settled on, suggestions for a better one would be welcome. (Attribute-Intersecting Natural Join is another candidate.)
+
+This function doesn't have a specific identity value, although it holds that @r \`interJoin\` r = r@
+
+>>> rPrint$ ( sp `projectAllBut` (rHdr (sno)) ) `interJoin` ( s `projectAllBut` (rHdr (sno)) )
+...
+    Overlapping instances for NotEmpty '[]
+      arising from a use of ‘interJoin’
+
+>>> rPrint$ sp `interJoin` s
+┌─────┬─────┬─────┬───────┬────────┬────────┐
+│ sno │ pno │ qty │ sName │ status │ city   │
+╞═════╪═════╪═════╪═══════╪════════╪════════╡
+│ S1  │ P1  │ 300 │ Smith │ 20     │ London │
+│ S1  │ P2  │ 200 │ Smith │ 20     │ London │
+...
+│ S4  │ P4  │ 300 │ Clark │ 20     │ London │
+│ S4  │ P5  │ 400 │ Clark │ 20     │ London │
+└─────┴─────┴─────┴───────┴────────┴────────┘
+-}
+interJoin r1 r2 = dyaOp' Algebra.interJoin r1 r2
+-- | Alias of 'interJoin'
+iJoin r1 r2 = dyaOp' Algebra.iJoin r1 r2
+
+
+{- | Extends the first given relation with an attribute resulting from imaging each tuple of said relation against the second given relation. The following command gives a result that includes the information given by SQL @RIGHT OUTER JOIN@:
+
+>>> rPrint$ imageExtendL s sp pq
+┌───────────────┬─────┬───────┬────────┬────────┐
+│ pq            │ sno │ sName │ status │ city   │
+╞═══════════════╪═════╪═══════╪════════╪════════╡
+│ ┌─────┬─────┐ │ S5  │ Adams │ 30     │ Athens │
+│ │ pno │ qty │ │     │       │        │        │
+│ ╞═════╪═════╡ │     │       │        │        │
+│ └─────┴─────┘ │     │       │        │        │
+│ ┌─────┬─────┐ │ S1  │ Smith │ 20     │ London │
+│ │ pno │ qty │ │     │       │        │        │
+│ ╞═════╪═════╡ │     │       │        │        │
+│ │ P1  │ 300 │ │     │       │        │        │
+│ │ P2  │ 200 │ │     │       │        │        │
+...
+
+See also 'extend', which this function specializes, and 'image', which it uses to perform this specialization.
+-}
+imageExtendL
+  :: (Eq (HList l), Ord (HList l1), Ord (HList r'),
+      HLabelSet (LabelsOf l), HLabelSet (Label t ': LabelsOf l1),
+      HDeleteLabels (LabelsOf l1) r r',
+      H2ProjectByLabels (LabelsOf l) r l b1,
+      H2ProjectByLabels (LabelsOf r) l1 l b2, HAllTaggedLV l1,
+      HAllTaggedLV l, DyaOp a b, DyaOpLeft a ~ Set (Record l1),
+      DyaOpRight b ~ Relation r) =>
+     a
+     -> b
+     -> Label t
+     -> DyaOpRes a b (Set (Record (Tagged t (Relation r') ': l1)))
+imageExtendL r1 r2 l = dyaOp' (\r1 r2 -> Algebra.imageExtendL r1 r2 l) r1 r2
+
+
+{-| The semi-join of the first given relation against the second given relation.
+
+>>> rPrint$ s `matching` sp
+┌─────┬───────┬────────┬────────┐
+│ sno │ sName │ status │ city   │
+╞═════╪═══════╪════════╪════════╡
+│ S1  │ Smith │ 20     │ London │
+│ S2  │ Jones │ 10     │ Paris  │
+│ S3  │ Blake │ 30     │ Paris  │
+│ S4  │ Clark │ 20     │ London │
+└─────┴───────┴────────┴────────┘
+-}
+matching r1 r2 = semiJoin r1 r2
+
+-- | Alias of 'matching'.
+semiJoin r1 r2 = dyaOp' Algebra.semiJoin r1 r2
+
+
+{-| The semi-difference of the first given relation against the second given relation. Aka. antijoin.
+
+>>> rPrint$ s `notMatching` sp
+┌─────┬───────┬────────┬────────┐
+│ sno │ sName │ status │ city   │
+╞═════╪═══════╪════════╪════════╡
+│ S5  │ Adams │ 30     │ Athens │
+└─────┴───────┴────────┴────────┘
+-}
+notMatching r1 r2 = semiDiff r1 r2
+{- Don't name this "antijoin":
+
+Also known, a trifle inappropriately, as antijoin.
+   - Chris Date 2011, SQL and Relational Theory 2nd ed. p. 133
+-}
+
+-- | Alias of 'notMatching'.
+semiDiff r1 r2 = dyaOp' Algebra.semiDiff r1 r2
+
+
+{-| The union of two relations.
+
+>>> let newSups = ( relation [rTuple (sno .=. "S6", sName .=. "Nena", city .=. "Berlin", status .=. 40)] )
+>>> rPrint$ s `union` newSups
+┌─────┬───────┬────────┬────────┐
+│ sno │ sName │ status │ city   │
+╞═════╪═══════╪════════╪════════╡
+│ S1  │ Smith │ 20     │ London │
+│ S2  │ Jones │ 10     │ Paris  │
+│ S3  │ Blake │ 30     │ Paris  │
+│ S4  │ Clark │ 20     │ London │
+│ S5  │ Adams │ 30     │ Athens │
+│ S6  │ Nena  │ 40     │ Berlin │
+└─────┴───────┴────────┴────────┘
+-}
+union r1 r2 = dyaOp' Algebra.union r1 r2
+
+{-| The disjoint union between the relations. This is a union of disjoint relations, where a runtime error is raised if the arguments are not disjoint.
+
+>>> :{
+  rPrint$ ( p' `project` (rHdr (city)) )
+          `dUnion`
+          ( s' `project` (rHdr (city)) )
+:}
+┌─*** Exception: Arguments to dUnion are not disjoint, intersection:
+┌────────┐
+│ city   │
+╞════════╡
+│ London │
+│ Paris  │
+└────────┘
+-}
+dUnion r1 r2 = dyaOp' Algebra.dUnion r1 r2
+
+{-| The intersection of two relations.
+
+Note how the name is different from Data.Set, where it is named "intersection". This is due to it being referred to as "intersect" in material describing the relational model; specifically named \"INTERSECT\" in Tutorial D.
+
+>>> let sX = ( relation [rTuple (sno .=. "S2", sName .=. "Jones", city .=. "Paris", status .=. 10), rTuple (sno .=. "S6", sName .=. "Nena", city .=. "Berlin", status .=. 40)] )
+>>> rPrint$ s `intersect` sX
+┌─────┬───────┬────────┬───────┐
+│ sno │ sName │ status │ city  │
+╞═════╪═══════╪════════╪═══════╡
+│ S2  │ Jones │ 10     │ Paris │
+└─────┴───────┴────────┴───────┘
+
+Notably, for any given relation values r1 and r2 that are of the same type it holds that:
+
+@r1 \`intersect\` r2 == r1 \`naturalJoin\` r2@
+
+Within relational theory the natural join generalizes as such both intersection and cartesian product.
+-}
+intersect r1 r2 = dyaOp' Algebra.intersect r1 r2
+
+{-| The difference of two relations.
+
+The "minus" term is used in material describing relational theory; specifically Tutorial D names the operator \"MINUS\".
+
+>>> rPrint$ s `minus` sX
+┌─────┬───────┬────────┬────────┐
+│ sno │ sName │ status │ city   │
+╞═════╪═══════╪════════╪════════╡
+│ S1  │ Smith │ 20     │ London │
+│ S3  │ Blake │ 30     │ Paris  │
+│ S4  │ Clark │ 20     │ London │
+│ S5  │ Adams │ 30     │ Athens │
+└─────┴───────┴────────┴────────┘
+-}
+minus r1 r2 = dyaOp' Algebra.minus r1 r2
+
+{- The difference of two relations. This differs from 'minus' in that the attribute order of the second argument takes precedence. This function is as such equal to 'minus' as far as relational theory is concerned, the difference is on a lower level of abstraction.
+
+>>> rPrint$ s `minus_` sX
+┌─────┬───────┬────────┬────────┐
+│ sno │ sName │ city   │ status │
+╞═════╪═══════╪════════╪════════╡
+│ S1  │ Smith │ London │ 20     │
+│ S3  │ Blake │ Paris  │ 30     │
+│ S4  │ Clark │ London │ 20     │
+│ S5  │ Adams │ Athens │ 30     │
+└─────┴───────┴────────┴────────┘
+-}
+-- minus_ r1 r2 = dyaOp' Algebra.minus_ r1 r2
+-- TODO: Should minus_ be exported? I don't see a big reason to, Algebra.minus is used directly by Assignment...
+
+
+{-| Exclusive union, aka. symmetric difference
+
+>>> rPrint$ s `xUnion` sX
+┌─────┬───────┬────────┬────────┐
+│ sno │ sName │ status │ city   │
+╞═════╪═══════╪════════╪════════╡
+│ S1  │ Smith │ 20     │ London │
+│ S3  │ Blake │ 30     │ Paris  │
+│ S4  │ Clark │ 20     │ London │
+│ S5  │ Adams │ 30     │ Athens │
+│ S6  │ Nena  │ 40     │ Berlin │
+└─────┴───────┴────────┴────────┘
+-}
+xUnion r1 r2 = dyaOp' Algebra.xUnion r1 r2
+
+
+{-| The summarization of the relations by the given function.
+
+>>> let pct = Label :: Label "pct"
+>>> rPrint$ summarize sp (s `project` (rHdr (sno))) (rHdr (pno)) (\r -> pct .=. count r .*. emptyRecord)
+┌─────┬─────┐
+│ pct │ sno │
+╞═════╪═════╡
+│ 0   │ S5  │
+│ 1   │ S3  │
+│ 2   │ S2  │
+│ 3   │ S4  │
+│ 6   │ S1  │
+└─────┴─────┘
+
+>>> rPrint$ summarize sp (s `project` (rHdr (sno))) (rHdr (qty)) (\r -> qty .=. sum ( agg qty r ) .*. emptyRecord)
+┌──────┬─────┐
+│ qty  │ sno │
+╞══════╪═════╡
+│ 0    │ S5  │
+│ 200  │ S3  │
+│ 700  │ S2  │
+│ 900  │ S4  │
+│ 1300 │ S1  │
+└──────┴─────┘
+-}
+summarize r1 r2 attsIn fOut = dyaOp' (\r1' r2' -> Algebra.summarize r1' r2' attsIn fOut) r1 r2
+
+{-| Tests whether the second argument is a proper subset of the first.
+
+>>> let spX = relation [rTuple (sno .=. "S1", pno .=. "P4", qty .=. 200), rTuple (sno .=. "S2", pno .=. "P2", qty .=. 400)]
+>>> spX `isProperSubsetOf` sp
+True
+-}
+isProperSubsetOf r1 r2 = dyaOp' Algebra.isProperSubsetOf r1 r2
+
+{-| Tests whether the second argument is a subset of the first.
+
+>>> spX `isSubsetOf` sp
+True
+-}
+isSubsetOf r1 r2 = dyaOp' Algebra.isProperSubsetOf r1 r2
+
+
+
+-- | The class of relational assignment
+class RelAssign a where
+    type RelAssignArg a :: *
+    -- | Relational IO function application.
+    relAssign :: (RelAssignArg a -> IO ()) -> a -> IO ()
+
+instance RelAssign (Relation a) where
+    type RelAssignArg (Relation a) = (Relation a)
+    relAssign = id
+
+instance RelAssign (IO (Relation a)) where
+    type RelAssignArg (IO (Relation a)) = Relation a
+    relAssign = (=<<)
+
+instance (Ord (HList b), Read (HList (RecordValuesR b)), RecordValues b,
+          HMapAux HList TaggedFn (RecordValuesR b) b) =>
+         RelAssign (Relvar b) where
+    type RelAssignArg (Relvar b) = Relation b
+    relAssign f r = f =<< readRelvar r
+
+
+-- TODO: What is the correct fixity? (Should most likely be thought through for the whole library.)
+infix 1 `assign`
+{-| Writes a relation value to a relvar file, replacing the existing value.
+
+>>> assign s s'
+Value assigned to SuppliersPartsDB/S.rv
+-}
+assign rv r = relAssign ( Assignment.assign rv ) r
+
+
+infix 1 `insert`
+{-|
+Inserts a relation into a relvar. This differs from SQLs INSERT; the relvar is updated to the union of the relvar and the relation value given as arguments.
+
+>>> let newSups = relation [rTuple (sno .=. "S6", sName .=. "Nena", city .=. "Berlin", status .=. 40)]
+>>> insert s newSups
+Inserted 1 of 1 tuples into SuppliersPartsDB/S.rv
+>>> insert s newSups
+Inserted 0 of 1 tuples into SuppliersPartsDB/S.rv
+>>> rPrint$ s
+┌─────┬───────┬────────┬────────┐
+│ sno │ sName │ status │ city   │
+╞═════╪═══════╪════════╪════════╡
+...
+│ S6  │ Nena  │ 40     │ Berlin │
+└─────┴───────┴────────┴────────┘
+-}
+insert rv r = relAssign ( Assignment.insert rv ) r
+
+
+infix 1 `dInsert`
+{-| Disjoint insert. Closer to SQL INSERT, except that this will never insert a
+duplicate tuple.
+
+>>> dInsert sp $ relation [rTuple (sno .=. "S6", pno .=. "P7", qty .=. 99)]
+Inserted 1 tuples into SuppliersPartsDB/SP.rv
+>>> dInsert sp $ relation [rTuple (sno .=. "S6", pno .=. "P7", qty .=. 99), rTuple (sno .=. "S4", pno .=. "P4", qty .=. 300), rTuple (sno .=. "S7", pno .=. "P8", qty .=. 200)]
+*** Exception: Unique constraint violation, tuples already present in SuppliersPartsDB/SP.rv:
+┌─────┬─────┬─────┐
+│ sno │ pno │ qty │
+╞═════╪═════╪═════╡
+│ S4  │ P4  │ 300 │
+│ S6  │ P7  │ 99  │
+└─────┴─────┴─────┘
+-}
+dInsert rv r = relAssign ( Assignment.dInsert rv ) r
+
+
+infix 1 `delete`
+{-| Deletes a specified subset of a relvar. Note that this is not SQL DELETE, but instead a generalization thereof.
+
+>>> delete s newSups
+Deleted 1 tuples from SuppliersPartsDB/S.rv
+-}
+delete rv r = relAssign ( Assignment.delete rv ) r
+
+infix 1 `iDelete`
+{-| Performs an inclusive delete against a relvar. Also not SQL DELETE. This will fail if the second argument is not a subset of the relation variable.
+
+>>> iDelete sp $ relation [rTuple (sno .=. "S6", pno .=. "P7", qty .=. 99), rTuple (sno .=. "S4", pno .=. "P4", qty .=. 300), rTuple (sno .=. "S7", pno .=. "P8", qty .=. 200)]
+*** Exception: Tuples not found in relvar SuppliersPartsDB/SP.rv:
+┌─────┬─────┬─────┐
+│ sno │ pno │ qty │
+╞═════╪═════╪═════╡
+│ S7  │ P8  │ 200 │
+└─────┴─────┴─────┘
+-}
+iDelete rv r = relAssign ( Assignment.iDelete rv ) r
diff --git a/src/Database/HaskRel/Relational/Unicode.hs b/src/Database/HaskRel/Relational/Unicode.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/HaskRel/Relational/Unicode.hs
@@ -0,0 +1,261 @@
+{-# LANGUAGE TypeFamilies, FlexibleContexts, ScopedTypeVariables #-}
+
+{-|
+Module      : Database.HaskRel.Relational.Unicode
+Description : Functions pertaining to relational theory or set theory named with unicode characters
+Copyright   : © Thor Michael Støre, 2015
+License     : GPL v2 without "any later version" clause
+Maintainer  : thormichael át gmail døt com
+Stability   : experimental
+
+Functions pertaining to relational theory or set theory named with non-ASCII unicode characters, primarily infix operators. Each of these is a synonym for an alphabetically named prefix function.
+
+See also: http://hackage.haskell.org/package/base-unicode-symbols
+
+TODO: Fix operator precedence, right now one may need to apply more parenthesis than should be necessary.
+-}
+
+module Database.HaskRel.Relational.Unicode (
+  -- * Relational algebra operators
+  (⋈), (⋉), (⋊), (◅), (▻), (×), (∣), (∪), (∩), (∖), π,
+  (⊂), (⊆), (⊃), (⊇), 
+  -- * Relational assignment operators
+  (≔),
+  -- * Supplementary relational operators
+  -- **** Not part of relational theory
+  (⊠), 
+  -- * Set theoretic operators
+  (#), (∈), (∉), (∋), (∌), (∅)
+) where
+
+import Database.HaskRel.Relational.Definition ( Relation, bodyAsList, empty )
+import Database.HaskRel.Relational.Expression
+import Database.HaskRel.Relational.Variable ( Relvar, writeRelvarBody' )
+
+
+import Data.Set ( Set )
+import Data.HList.CommonMain
+
+{-| Natural join.
+
+>>> rPrint$ sp ⋈ s
+...
+
+As 'Database.HaskRel.Relational.Expression.naturalJoin'.
+-}
+r1 ⋈ r2 = naturalJoin r1 r2
+
+{-| Semijoin.
+
+>>> rPrint$ s ⋉ sp
+...
+
+As 'Database.HaskRel.Relational.Expression.matching'.
+-}
+r1 ⋉ r2 = semiJoin r1 r2
+
+-- | Left semijoin. As @(flip 'Database.HaskRel.Relational.Expression.matching')@.
+r1 ⋊ r2 = semiJoin r2 r1
+
+
+{-| Semidifference.
+
+>>> rPrint$ s ◅ sp
+...
+
+As 'Database.HaskRel.Relational.Expression.notMatching'.
+-}
+r1 ◅ r2 = notMatching r1 r2
+
+-- | Left semidifference. As @(flip 'Database.HaskRel.Relational.Expression.notMatching')@.
+r1 ▻ r2 = notMatching r2 r1
+
+{-| Times. The special case of natural join where the headings of the relations are disjoint.
+
+>>> rPrint$ ( sp `projectAllBut` (rHdr (sno)) ) × ( s `projectAllBut` (rHdr (sno)) )
+...
+
+As 'Database.HaskRel.Relational.Expression.times'.
+-}
+l × r = times l r
+
+{-| Attribute intersecting natural join. The special case of natural join where the headings of the relations are not disjoint.
+
+Using the "box times" or "squared times" (U+22A0) symbol is my own solution. As with the name "(attribute) intersecting natural join" suggestions are welcome.
+
+As mentioned in "Database.HaskRel.Relational.Algebra", this operation doesn't have a single identity value, although it holds that for any given relation value @r@, @r ⊠ r = r@
+
+>>> rPrint$ sp ⊠ s
+...
+
+As 'Database.HaskRel.Relational.Expression.interJoin'.
+-}
+l ⊠ r = interJoin l r
+
+
+{-| Restriction.
+
+Note that the symbol used here is the divisor symbol, which looks the same but is distinct from the vertical bar, or pipe. However, since the vertical bar is used in Haskell for different purposes and is for that reason not a valid infix operator symbol, this is used instead.
+
+>>> rPrint$ p ∣ (\[pun|weight|] -> weight < 17.5)
+...
+
+As 'Database.HaskRel.Relational.Expression.restrict'.
+-}
+r ∣ p = restrict r p
+
+{-| Union.
+
+>>> rPrint$ s ∪ ( relation [rTuple (sno .=. "S6", sName .=. "Nena", status .=. 40, city .=. "Berlin")] )
+...
+
+As 'Database.HaskRel.Relational.Expression.union'.
+-}
+l ∪ r = l `union` r
+
+{-| Intersection.
+
+>>> let sX = ( relation [rTuple (sno .=. "S2", sName .=. "Jones", status .=. 10, city .=. "Paris"), rTuple (sno .=. "S6", sName .=. "Nena", status .=. 40, city .=. "Berlin")] )
+>>> rPrint$ s ∩ sX
+...
+
+As 'Database.HaskRel.Relational.Expression.intersect'.
+-}
+l ∩ r = l `intersect` r
+
+{-| Minus.
+
+Note that this is the difference symbol, not a backslash.
+
+>>> rPrint$ s ∖ sX
+...
+
+As 'Database.HaskRel.Relational.Expression.minus'.
+-}
+l ∖ r = minus l r
+
+{-| Projection.
+
+Note that no matter how greek it is π is still a character, and Haskell therefore treats it as a prefix operator, which is in line with how it is employed.
+
+>>> rPrint$ π (rHdr (color,city)) p
+...
+
+As 'Database.HaskRel.Relational.Expression.project', but note how the operands are reversed.
+-}
+π a r  = project r a
+
+infix 1 ≔
+
+{-|
+Relational assignment operator.
+
+This uses the COLON EQUALS UTF-8 character (\&\#8788;), the ASCII variant := wouldn't be allowed in Haskell since it starts with a colon.
+
+>>> s ≔ s'
+>>>
+
+As 'Database.HaskRel.Relational.Expression.assign'.
+-}
+(≔) rv r = assign rv r
+
+
+{-| Is proper subset.
+
+>>> let spX = relation [rTuple (sno .=. "S1", pno .=. "P4", qty .=. 200), rTuple (sno .=. "S2", pno .=. "P2", qty .=. 400)]
+>>> spX ⊂ sp
+True
+
+As 'Database.HaskRel.Relational.Expression.isProperSubsetOf'.
+-}
+l ⊂ r = isProperSubsetOf l r
+
+{-| Is subset of.
+
+>>> spX ⊆ sp
+True
+
+As 'Database.HaskRel.Relational.Expression.isSubsetOf'.
+-}
+l ⊆ r = isSubsetOf l r
+
+-- | Left is proper subset of. As @(flip 'Database.HaskRel.Relational.Expression.isProperSubsetOf')@.
+l ⊃ r = isProperSubsetOf r l
+
+-- | Left is subset of. As @(flip 'Database.HaskRel.Relational.Expression.isSubsetOf')@.
+l ⊇ r = isSubsetOf r l
+
+{-| Cardinality.
+
+>>> (#) sp
+12
+
+As 'Database.HaskRel.Relational.Expression.count'.
+-}
+(#) r = count r
+
+
+{-| Is member of.
+
+>>> let spX = rTuple(sno .=. "S3", qty .=. 200, pno .=. "P2")
+>>> spX ∈ sp
+True
+
+As 'Database.HaskRel.Relational.Expression.member'.
+-}
+l ∈ r = member l r
+
+{-| Is not member of.
+
+>>> spX ∉ sp
+False
+
+As 'Database.HaskRel.Relational.Expression.notMember'.
+-}
+l ∉ r = notMember l r
+
+-- | Is member of left. As @(flip 'Database.HaskRel.Relational.Expression.member')@.
+r ∋ e = member e r
+
+-- | Is not member of left. As @(flip 'Database.HaskRel.Relational.Expression.notMember')@.
+r ∌ e = notMember e r
+
+{- | The empty set. Note that this is neither 'tableDum' nor 'tableDee'.
+
+>>> (relation [] :: Relation '[]) == (∅)
+True
+>>> relation [rTuple (sno .=. "S1", status .=. 5)] == (∅)
+False
+-}
+(∅) = empty
+
+{-
+Other infix operators
+∖ minus/relative complement/set-theoretic difference - don't confuse with blackslash - \ - you may need to use a different font to see the difference.
+ # cardinality - prefix, needs parenthesis
+∅ empty set
+∆ or ⊖ symmetric difference
+π relational projection
+◅ ▻ antijoin
+σ selection
+‼ image relation
+:= or ≔ relational assignment
+
+Predicate logic, although the Haskell library http://hackage.haskell.org/package/base-unicode-symbols already uses them:
+∀ Forall
+∃ Exists
+
+Other common and useful operators of arithmetry and whatnot:
+≤
+≥
+±
+∑
+≬ between
+≺ preceeds
+≻ suceeds
+
+See also:
+http://en.wikipedia.org/wiki/List_of_mathematical_symbols
+http://www.fileformat.info/info/unicode/block/mathematical_operators/images.htm
+-}
+          
diff --git a/src/Database/HaskRel/Relational/Variable.hs b/src/Database/HaskRel/Relational/Variable.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/HaskRel/Relational/Variable.hs
@@ -0,0 +1,124 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE UndecidableInstances, FlexibleContexts, ScopedTypeVariables #-}
+
+{-|
+Module      : Database.HaskRel.Relational.Variable
+Description : Relation variable definition and support functions
+Copyright   : © Thor Michael Støre, 2015
+License     : GPL v2 without "any later version" clause
+Maintainer  : thormichael át gmail døt com
+Stability   : experimental
+
+Relation variable definition, along with IO level support functions.
+-}
+module Database.HaskRel.Relational.Variable (
+  -- * Relation variable definitions
+  Relvar (Relvar, relvarPath), relvarType,
+  -- * Relational input
+  readRel, readRelvar, hListsToRel,
+  -- * Relational output
+  writeRelvarBody, writeRelvarBody', showRelStr
+  ) where
+
+import Data.HList.CommonMain
+
+import Data.Set ( Set, fromList )
+import Data.Typeable ( Typeable )
+
+import Database.HaskRel.HFWTabulation
+  ( HFWPresent, HPresentTypedRecAttr, HPresentRecAttr, showHListSetType,
+    hfwPrint, hfwPrintTyped, hfwPrintTypedTS )
+import Database.HaskRel.Relational.Definition ( Relation, bodyAsList )
+
+
+-- == Relation variable reference == --
+
+{-| Relation variable reference. This type has a phantom type variable, which generally calls for the type to be explicity specified:
+
+@ s = Relvar "SuppliersPartsDB/S.rv" :: Relvar '[SNO, SName, Status, City]@
+-}
+data Relvar (a::[*]) = Relvar { relvarPath :: FilePath }
+
+-- | Gives the type a relvar results in. Note that the value this results in will always be @undefined@.
+relvarType :: Relvar a -> Relation a
+relvarType rv = undefined
+
+
+-- TODO: It should be enforced that a given relvar has a given type
+-- TODO: This is also afflicted by the issue that showHListSetType was developed for TIPs
+
+instance Typeable a => Show ( Relvar a ) where
+    show a = "Relvar \"" ++ relvarPath a ++ "\" :: Relvar" ++ showHListSetType ( relvarType a )
+
+
+-- | Converts a list of HLists into a relation value.
+hListsToRel
+  :: (Ord (HList b), RecordValues b,
+      HMapAux HList TaggedFn (RecordValuesR b) b) =>
+     [HList (RecordValuesR b)] -> Relation b
+hListsToRel = fromList . map hMapTaggedFn
+
+
+{-| Reads a relation value from a string containing HLists of unpacked attribues.
+
+>>> pt$ ( readRel "H[\"S1\",10],H[\"S2\",50]" :: Relation '[SNO,Status])
+┌───────────────┬───────────────────┐
+│ sno :: String │ status :: Integer │
+╞═══════════════╪═══════════════════╡
+│ S1            │ 10                │
+│ S2            │ 50                │
+└───────────────┴───────────────────┘
+-}
+readRel :: forall b .
+     (Ord (HList b), Read (HList (RecordValuesR b)), RecordValues b,
+      HMapAux HList TaggedFn (RecordValuesR b) b) =>
+     String -> Relation b
+readRel s = hListsToRel $ read $ "[" ++ s ++ "]"
+
+-- | Reads a relation value of a given type from a string.
+readRel' :: forall b .
+     (Ord (HList b), Read (HList (RecordValuesR b)), RecordValues b,
+      HMapAux HList TaggedFn (RecordValuesR b) b) =>
+     String -> Relation b -> Relation b
+readRel' s rt = hListsToRel $ read $ "[" ++ s ++ "]"
+
+-- | Read a relation variable from the file referenced by the first argument
+readRelvar
+  :: (Ord (HList b), Read (HList (RecordValuesR b)), RecordValues b,
+      HMapAux HList TaggedFn (RecordValuesR b) b) =>
+     Relvar b -> IO (Relation b)
+readRelvar rv = do
+    relStr <- readFile ( relvarPath rv )
+    return $ readRel relStr
+
+
+-- | Prints a relation as a list without the outer brackets.
+showRelStr :: (Show (HList (RecordValuesR r)), RecordValues r) =>
+     Relation r -> String
+showRelStr = init . tail . show . bodyAsList
+
+-- TODO: This uses text-processing on the result of a call to show, fix so that
+-- it doesn't break if the show-format is changed.
+-- | Writes a body of a relvar to a given file
+writeRelvarBody :: Show r => FilePath -> r -> IO ()
+writeRelvarBody n hll = writeFile n ( init $ tail $ show hll )
+
+-- | Writes a body of a relvar to a given relvar file reference
+writeRelvarBody' :: Show r => Relvar rv -> r -> IO ()
+writeRelvarBody' rv hll = writeFile ( relvarPath rv ) ( init $ tail $ show hll )
+
+-- == HFWPresent instance for relvars
+
+instance (Ord (HList b), Read (HList (RecordValuesR b)), Typeable b,
+      RecordValues b, HMapAux HList TaggedFn (RecordValuesR b) b,
+      HFoldr (Mapcar HPresentTypedRecAttr) [[String]] (RecordValuesR b) [[String]],
+      HFoldr (Mapcar HPresentRecAttr) [[String]] (RecordValuesR b) [[String]]) =>
+         HFWPresent ( Relvar b )
+    where
+      hfwPrint r' = do
+          r <- readRelvar r'
+          hfwPrint r
+      hfwPrintTypedTS ts r' = do
+          r <- readRelvar r'
+          hfwPrintTypedTS ts r
diff --git a/src/Database/HaskRel/Support.hs b/src/Database/HaskRel/Support.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/HaskRel/Support.hs
@@ -0,0 +1,207 @@
+
+{-|
+Module      : Support
+Description : Predicates and aggregates useful to relational querying
+Copyright   : © Thor Michael Støre, 2015
+License     : GPL v2 without "any later version" clause
+Maintainer  : thormichael át gmâïl døt cöm
+Stability   : experimental
+
+Predicates and aggregates useful to relational querying. These are not part of the relational algebra but are useful in relational queries in restriction predicates, and extension and summarization expressions. It also has great utility in non-relational queries, such as when performing aggregations.
+-}
+
+module Database.HaskRel.Support
+       ( -- * Predicates
+         (&=), plusminus, (+-), (±),
+         between, (>=<=), (≥≤), xBetween, (><), (>=<), (≥<), (><=), (>≤),
+         (≤), (≥), (≠),
+         -- * Aggregates
+         avg, minx, maxx )
+       where
+
+import Data.List (genericLength)
+
+
+infix 5 &=
+
+-- | Reverse predicate application. As "Data.Function.&", the reverse function application operator, but restricted to a boolean result.
+(&=) :: a -> ( a -> Bool ) -> Bool
+(&=) x f = f x
+
+{-
+-- TODO: Perhaps congruence (or a variation thereof?) is useful?
+(≅) :: Eq a => t -> t -> (t -> a) -> Bool
+(≅) a b f = f a == f b
+
+>>> 38 ≅ 58 $ ( `mod` 10 )
+True
+-}
+
+
+-- |>>> plusminus 9 3 10
+--True
+plusminus :: (Ord a, Num a) => a -> a -> a -> Bool
+plusminus x y c = c >= ( x - y ) && c <= ( x + y )
+
+infix 7 ±
+infix 7 +-
+
+{-| >>> 10 &= 9 ± 3
+True
+>>> rPrint$ p ∣ (\[pun|weight|] -> weight &= 9 ± 3)
+┌─────┬───────┬───────┬────────┬────────┐
+│ pno │ pName │ color │ weight │ city   │
+╞═════╪═══════╪═══════╪════════╪════════╡
+│ P1  │ Nut   │ Red   │ 12 % 1 │ London │
+│ P5  │ Cam   │ Blue  │ 12 % 1 │ Paris  │
+└─────┴───────┴───────┴────────┴────────┘
+-}
+(±) :: (Ord a, Num a) => a -> a -> a -> Bool
+(±) = plusminus
+
+-- |>>> 10 &= 9 +- 3
+--True
+(+-) :: (Ord a, Num a) => a -> a -> a -> Bool
+(+-) = plusminus
+
+
+-- |>>> 5 `between` (5,9)
+--True
+between :: Ord a => a -> (a, a) -> Bool
+between c (l,h) = c >= l && c <= h
+
+
+{-| >>> 5 &= 5 >=<= 9
+True
+-}
+(>=<=) :: Ord a => a -> a -> a -> Bool
+(>=<=) l h c = c >= l && c <= h
+
+{-| >>> 5 &= 5 ≥≤ 9
+True
+>>> rPrint$ p ∣ (\[pun|weight|] -> weight &= 11 ≥≤ 14)
+┌─────┬───────┬───────┬────────┬────────┐
+│ pno │ pName │ color │ weight │ city   │
+╞═════╪═══════╪═══════╪════════╪════════╡
+│ P1  │ Nut   │ Red   │ 12 % 1 │ London │
+│ P4  │ Screw │ Red   │ 14 % 1 │ London │
+│ P5  │ Cam   │ Blue  │ 12 % 1 │ Paris  │
+└─────┴───────┴───────┴────────┴────────┘
+-}
+(≥≤) :: Ord a => a -> a -> a -> Bool
+(≥≤) l h c = c >= l && c <= h
+
+{-|
+Between exclusive
+
+>>> 5 `xBetween` (5,9)
+False
+-}
+xBetween :: Ord a => a -> (a, a) -> Bool
+xBetween c (l,h) = c > l && c < h
+
+{-| >>> 5 &= 5 >< 9
+False
+>>> rPrint$ p ∣ (\[pun|weight|] -> weight &= 11 >< 14)
+┌─────┬───────┬───────┬────────┬────────┐
+│ pno │ pName │ color │ weight │ city   │
+╞═════╪═══════╪═══════╪════════╪════════╡
+│ P1  │ Nut   │ Red   │ 12 % 1 │ London │
+│ P5  │ Cam   │ Blue  │ 12 % 1 │ Paris  │
+└─────┴───────┴───────┴────────┴────────┘
+-}
+(><) :: Ord a => a -> a -> a -> Bool
+(><) l h c = c > l && c < h
+
+-- |>>> 5 &= 5 >=< 9
+--True
+(>=<) :: Ord a => a -> a -> a -> Bool
+(>=<) l h c = c >= l && c < h
+
+-- |>>> 5 &= 5 ≥< 9
+--True
+(≥<) :: Ord a => a -> a -> a -> Bool
+(≥<) l h c = c >= l && c < h
+
+-- |>>> 5 &= 5 ><= 9
+--False
+(><=) :: Ord a => a -> a -> a -> Bool
+(><=) l h c = c > l && c <= h
+
+-- |>>> 5 &= 5 >≤ 9
+--False
+(>≤) :: Ord a => a -> a -> a -> Bool
+(>≤) l h c = c > l && c <= h
+
+-- | Synonym for <=
+(≤) :: Ord a => a -> a -> Bool
+(≤) x y = x <= y
+
+-- | Synonym for >=
+(≥) :: Ord a => a -> a -> Bool
+(≥) x y = x >= y
+
+-- | Synonym for /=
+(≠) :: Eq a => a -> a -> Bool
+(≠) x y = x /= y
+
+
+{-| Average of a list of values
+
+>>> let _qtys a = Label .=. a :: Tagged "qtys" Double
+>>> pt$ group sp (rHdr (pno,qty)) (_qtys . avg . agg qty)
+┌────────────────────┬───────────────┐
+│ qtys :: Double     │ sno :: String │
+╞════════════════════╪═══════════════╡
+│ 200.0              │ S3            │
+│ 216.66666666666666 │ S1            │
+│ 300.0              │ S4            │
+│ 350.0              │ S2            │
+└────────────────────┴───────────────┘
+
+Note the explicit type in the definition of @_qtys@; it is neccessary to provide a specific type for 'pt' to format it as a table, even when an expression would otherwise be correct without this. The following would blow up if prefixed with "pt$":
+
+>>> group sp (rHdr (pno,qty)) ((qtys .=.) . avg . agg qty)
+fromList [Record{qtys=200.0,sno="S3"},Record{qtys=216.66666666666666,sno="S1"},Record{qtys=300.0,sno="S4"},Record{qtys=350.0,sno="S2"}]
+-}
+avg :: (Fractional a, Real a1) => [a1] -> a
+avg xs = realToFrac (sum xs) / genericLength xs
+
+
+{- | Minimum of several values, defaulting to the second argument if there are no elements.
+
+>>> pt$ group sp (rHdr (pno,qty)) ((qtys .=.) . (`minx` 0) . agg qty)
+┌─────────────────┬───────────────┐
+│ qtys :: Integer │ sno :: String │
+╞═════════════════╪═══════════════╡
+│ 100             │ S1            │
+│ 200             │ S3            │
+│ 200             │ S4            │
+│ 300             │ S2            │
+└─────────────────┴───────────────┘
+-}
+minx :: Ord a => [a] -> a -> a
+minx [] d = d
+minx xs _ = minimum xs
+
+{- Or perhaps with Foldable:
+minx :: (Ord a, Foldable t) => t a -> a -> a
+minx fl d = if F.null fl then d
+                         else F.minimum fl
+-}
+
+{- | Maximum of several values, defaulting to the second argument if there are no elements
+
+>>> pt$ group sp (rHdr (pno,qty)) ((qtys .=.) . (`maxx` 0) . agg qty)
+┌─────────────────┬───────────────┐
+│ qtys :: Integer │ sno :: String │
+╞═════════════════╪═══════════════╡
+│ 200             │ S3            │
+│ 400             │ S1            │
+│ 400             │ S2            │
+│ 400             │ S4            │
+└─────────────────┴───────────────┘
+-}
+maxx :: Ord a => [a] -> a -> a
+maxx [] d = d
+maxx xs _ = maximum xs
