TheoriesAndDataStructures.ltx

% %\documentclass[twoside,runningheads,envcountsame,envcountsect,oribibl]{llncs}
% %\documentclass[12pt,twoside]{report}
% %
% \documentclass[twoside,fontsize=9pt,paper=letter]{scrreprt}
% \usepackage[landscape,hmargin=2mm,includehead,top=0mm,bottom=4mm]{geometry}
% \usepackage{multicol}

% Following AContext-2

\documentclass[11pt,twoside]{article} % {report}
\usepackage[letterpaper,hmargin=15mm,includehead,includefoot,top=8mm,bottom=8mm]{geometry}

%%% NAME=TheoriesAndDataStructures
%%% export TEXINPUTS=.:ltx:
%%% ln -s $NAME.ltx $NAME.lagda
%%% bibtex $NAME && lhs2TeX --agda $NAME.lagda > $NAME.tex && time pdflatex $NAME.tex


%%% 2015-07-22, adapted from RATHAgda-2.1
%% pdftops $NAME.pdf;  pstops -pletter '2:0@0.73L(21.2cm,-1.0cm)+1@0.73L(21.2cm,13.0cm)' $NAME.ps > $NAME''_2up_letter.ps; ps2pdf $NAME''_2up_letter.ps

%% mupdf -r155 $NAME''_2up_letter.pdf &


\usepackage{etex}
\usepackage{graphicx}
\usepackage{textgreek}


%\usepackage[cjkbg5]{ucs}

%include polycode.fmt
%include agda.fmt
%format {          = "\{\mskip0.5mu "
%format }          = "\mskip0.5mu\}"
%include ltx/RathAgdaChars.sty

%% \def\fcmp{\fatsemi}

\renewcommand{\hscodestyle}{\small}

% %\spnewtheorem{Def}{Definition}[section]{\bfseries}{\rmfamily}
% \newtheorem{Def}{Definition}[section]
% 
% \usepackage{theref}
% \def\TheRefWithPageRef#1{}
% \newref{Def}{Def.\null{}}

\def\Version{TheoriesAndDataStructures-0.0%
%\input{TheoriesAndDataStructures_Version.txt}%
}


\makeatletter
\def\mkcommand#1{\expandafter\gdef\csname #1\endcsname}
%\@input{RathAgda1.ups}
\makeatother

%{{{ Title
\title{Theories and Data Structures
  \\
  {\small ``Two-Sides of the Same Coin'', or ``Library Design by Adjunction''}
}


%\titlerunning{}
%\toctitle{}

\author{Jacques Carette, Musa Al-hassy, Wolfram Kahl}

%%% \institute{McMaster University,
%%% %1280 Main St. West,
%%% Hamilton, Ontario, Canada,
%%% % L8S 4K1
%%% \email{kahl@@cas.mcmaster.ca}
%%% }

\date{\today}
%}}}

%{{{ \usepackage{hyperref}
\usepackage[pdfauthor={Jacques Carette, Musa Al-hassy, Wolfram Kahl},
  pdftitle={Theories and Data Structures},
%  pdfsubject={},
%  pdfkeywords={},
%   a4paper=true,
%   colorlinks,
   bookmarksnumbered
 ]{hyperref}
%}}}

%{{{ packages, macros, and settings
\usepackage[round]{natbib} % replaces {harvard}

%       \usepackage{tree-dvips}
       \usepackage{latexsym,amssymb}
%       \usepackage{graphicx}

\usepackage{comment}

\def\sectionname{Sect.\null{}}
\usepackage{sectref}

\def\modref#1{{\hbox{\small $\Conid{#1}$} (\sectref{#1})}}

\long\def\ignore#1{}

\renewcommand{\arraystretch}{1.1}

\input diagram-2.2
\usepackage{color}
\definecolor{grey}{gray}{0.6}

\def\etal{\textsl{et al.\null{}}}

\usepackage{edcomms}

%{{{ % docstyle overriding
% currently not available
%\usepackage{lmodern}
%\usepackage[T1]{fontenc}

%\usepackage{mathptmx}
%\usepackage{euler}

\makeatletter
%% Orig:
%% \def\@listI{\leftmargin\leftmargini
%%             \parsep 0\p@ \@plus1\p@ \@minus\p@
%%             \topsep 8\p@ \@plus2\p@ \@minus4\p@
%%             \itemsep0\p@}
%% WK:
\setlength\leftmargini  {0.93em}
\def\@@listI{\leftmargin\leftmargini
            \labelsep 0.3em
            \labelwidth\leftmargini
            \advance\labelwidth-\labelsep
            \parsep 0\p@@ \@@plus1\p@@ \@@minus\p@@
            \topsep 2\p@@ \@@plus1\p@@ \@@minus1\p@@
            \itemsep1\p@@}
\let\@@listi\@@listI
\@@listi
\makeatother
%}}}

\def\bbbone{{\mathchoice {\rm 1\mskip-4mu l} {\rm 1\mskip-4mu l}
{\rm 1\mskip-4.5mu l} {\rm 1\mskip-5mu l}}}
%
%\def\triv{\mathbf{1}}
\def\triv{\bbbone}

\makeindex
%}}}

%{{{ .lagda conventions
\def\module#1{\message{#1}\section{#1}\sectlabel{#1}}

\newenvironment{ModuleHead}{\par\begingroup\tiny}{\endgroup\par\medskip}

%\usepackage{comment}
%\specialcomment{ModuleHead}{\par\begingroup\tiny}{\endgroup}
%\excludecomment{ModuleHead}
%}}}


\DeclareUnicodeCharacter{7472}{\ensuremath{^\mathsf{D}}} % MODIFIER LETTER CAPITAL D
\DeclareUnicodeCharacter{9723}{\ensuremath{\square}} % WHITE MEDIUM SQUARE
\DeclareUnicodeCharacter{119920}{\ensuremath{\mathbf{I}}} % MATHEMATICAL BOLD ITALIC CAPITAL I
\DeclareUnicodeCharacter{119991}{\ensuremath{_\mathsf{B}}} % MATHEMATICAL SCRIPT SMALL B
\DeclareUnicodeCharacter{120008}{\ensuremath{_\mathsf{S}}} % MATHEMATICAL SCRIPT SMALL S
\DeclareUnicodeCharacter{120001}{\ensuremath{_\mathsf{L}}} % MATHEMATICAL SCRIPT SMALL L
\DeclareUnicodeCharacter{119997}{\ensuremath{_\mathsf{H}}} % MATHEMATICAL SCRIPT SMALL H
\DeclareUnicodeCharacter{8348}{\ensuremath{_\mathsf{t}}} % MATHEMATICAL SCRIPT SMALL T
\DeclareUnicodeCharacter{8339}{\ensuremath{_\mathsf{x}}} % MATHEMATICAL SCRIPT SMALL X
\DeclareUnicodeCharacter{119925}{\ensuremath{\mathcal{N}}} % MATHEMATICAL BOLD ITALIC CAPITAL N
\DeclareUnicodeCharacter{119924}{\ensuremath{\mathcal{M}}} % MATHEMATICAL BOLD ITALIC CAPITAL M
\DeclareUnicodeCharacter{7484}{\ensuremath{\mathsf{O}}} % MODIFIER LETTER CAPITAL O
\DeclareUnicodeCharacter{9678}{\ensuremath{\mathsf{BULLSEYE}}} % BULLSEYE
\DeclareUnicodeCharacter{8667}{\ensuremath{\Rrightarrow}} % rightwards triple arrow
\DeclareUnicodeCharacter{8255}{\ensuremath{\smile}} % undertie, subscript-converse
\DeclareUnicodeCharacter{8265}{\ensuremath{! \! ? }} % exclamation question mark
\DeclareUnicodeCharacter{9632}{\ensuremath{ \square }} % black square
\DeclareUnicodeCharacter{9679}{\ensuremath{ \boldsymbol{\cdot} }} % black circle
\DeclareUnicodeCharacter{9675}{\ensuremath{ \boldsymbol{\circ} }} % white circle

\pagestyle{headings}
\parskip4pt
\parindent0pt
\mathindent0pt
\begin{document}
\maketitle

\ignore{
%{{{ Title
\begin{center}
\huge\bf Theories and Data Structures
\\[2ex]
\Version%
%\thanks{This research is supported by NSERC (National Science and
% Engineering Research Council of Canada).}
\end{center}

\kern6ex
\begin{center}
%{{{ \author{}
\def\affaddr#1{{\normalsize #1}}
\def\email#1{{\normalsize \textsf{#1}}}

{\Large\sc Wolfram Kahl%
%\footnote{This research has been supported by the National Science and
%  Engineering Research Council (NSERC), Canada}
}
\\[2ex]
\email{kahl@@cas.mcmaster.ca}
%}}}

\kern3ex
\affaddr{Department of Computing and Software, McMaster University}
\\
\affaddr{Hamilton, Ontario, Canada L8S 4K1}
\\[6ex]
16 January 2017
\end{center}
%}}}
}%ignore

\pagestyle{headings}
%\pagestyle{empty}
\thispagestyle{empty}

\kern6ex
%{{{ abstract
\centerline{\bf Abstract}

\kern0.6ex
\noindent


We aim to show how common data-structures naturally arise from elementary mathematical theories.

In particular, we answer the following questions:
\begin{itemize}
\item Why do lists pop-up more frequently to the average programmer than, say, their duals: bags?
\item More simply, why do unit and empty types occur so naturally? What about enumerations/sums and records/products?
\item Why is it that dependent sums and products do not pop-up expicitly to the average programmer?
  They arise naturally all the time as tuples and as classes.
\item How do we get the usual toolbox of functions and helpful combinators for a particular data type? Are they ``built into'' the type?
\item Is it that the average programmer works in the category of classical Sets, with functions and propositional equality? Does this result in some ``free constructions'' not easily made computable since mathematicians usually work in the category of Setoids but tend to quotient to arrive in |Sets?| ---where quotienting is not computably feasible, in |Sets| at-least; and why is that?
\end{itemize}


\unfinished
%\end{abstract}
%}}}

\ignore{%
%{{{ Keywords:
\begin{keywords}
\unfinished
\end{keywords}
%}}}
}%ignore

\kern1.4ex
\hrule height0.2pt width70mm depth0pt

\noindent
{\footnotesize This research is supported by the National Science and
  Engineering Research Council (NSERC), Canada}

%{{{ remaining frontmatter
\vfill
\pagebreak
{%\small
\parskip2.9pt
%\setcounter{tocdepth}{2}
%\baselineskip14pt
\tableofcontents
}
\vfill
\pagebreak
%}}}

%{{{ \section{Introduction}
\section{Introduction}

\unfinished

%{{{ \section{Overview}
\section{Overview}

\unfinished
%}}}

\bigskip
%{{{ The Agda source code for this development is available on-line
The Agda source code for this development is available on-line
at the following URL:

\kern1ex
\centerline{\scalebox{0.95}[0.99]{\url{https://github.com/JacquesCarette/TheoriesAndDataStructures}}}
%}}}
%}}}

\part{Helpers}

%include Forget.lagda
%include EqualityCombinators.lagda
%include DataProperties.lagda
%% %include RATH.lagda  %% ‼ This module is not being called from anywhere ‼  June 9, 2017.

\part{Variations on Sets}

%include Structures/TwoSorted.lagda
%include Structures/Rel.lagda
%include Structures/Pointed.lagda

%include Structures/Dependent.lagda
%%
%% MA: We do not want to include the experiements; perhaps.
%% 
%% %include Structures/Experiments/Dependent2.lagda
%% %include Structures/Experiments/Dependent3.lagda

%include Structures/DistinguishedSubset.lagda

\part{Unary Algebras}

%include Structures/UnaryAlgebra.lagda
%include Structures/InvolutiveAlgebra.lagda
%include Structures/IndexedUnaryAlgebra.lagda

\part{Boom Hierarchy}

%include Structures/Magma.lagda
%include Structures/Semigroup.lagda
%include Structures/Monoid.lagda
%include Structures/CommMonoid.lagda
%include Structures/CommMonoidTerm.lagda
%include Structures/AbelianGroup.lagda
%%
%% %include Structures/BagEquivalence.agda
%include Structures/Multiset.lagda

\part{Setoids}

%include SetoidEquiv.lagda
%include SetoidOfIsos.lagda
%include SetoidSetoid.lagda
%include SetoidFamilyUnion.lagda

\part{Equiv}

%include Equiv.lagda
%include ISEquiv.lagda
%include TypeEquiv.lagda

\part{Misc}

%include Function2.lagda
%include ParComp.lagda
%include Belongs.lagda
%include Some.lagda
%include CounterExample.lagda

%{{{ \section{Conclusion and Outlook}\chaptlabel{Conclusion}
\section{Conclusion and Outlook}\chaptlabel{Conclusion}
 
\unfinished
%}}}

%%\bibliographystyle{relmics-alpha}
%%\bibliographystyle{kluwer}
\bibliographystyle{plainnat} % (natbib)
\bibliography{strings,ref,crossrefs}

\end{document}

\begin{spec}

\end{spec}

%{{{ EMACS local variables
% Local Variables:
% compile-command: "NAME=TheoriesAndDataStructures ; export TEXINPUTS=.:ltx: ; ln -s $NAME.ltx $NAME.lagda ; lhs2TeX --agda $NAME.lagda > $NAME.tex && time pdflatex $NAME.tex"
% folded-file: t
% eval: (fold-set-marks "%{{{ " "%}}}")
% eval: (fold-whole-buffer)
% fold-internal-margins: 0
% end:
%}}}