\documentclass[]{article}
\usepackage{lmodern}
\usepackage{amssymb,amsmath}
\usepackage{ifxetex,ifluatex}
\usepackage{fixltx2e} % provides \textsubscript
\ifnum 0\ifxetex 1\fi\ifluatex 1\fi=0 % if pdftex
  \usepackage[T1]{fontenc}
  \usepackage[utf8]{inputenc}
\else % if luatex or xelatex
  \ifxetex
    \usepackage{mathspec}
  \else
    \usepackage{fontspec}
  \fi
  \defaultfontfeatures{Ligatures=TeX,Scale=MatchLowercase}
\fi
% use upquote if available, for straight quotes in verbatim environments
\IfFileExists{upquote.sty}{\usepackage{upquote}}{}
% use microtype if available
\IfFileExists{microtype.sty}{%
\usepackage[]{microtype}
\UseMicrotypeSet[protrusion]{basicmath} % disable protrusion for tt fonts
}{}
\PassOptionsToPackage{hyphens}{url} % url is loaded by hyperref
\usepackage[unicode=true]{hyperref}
\hypersetup{
            pdftitle={CSci 450: Org. of Programming Languages Labeled Digraph ADT in Haskell},
            pdfauthor={H. Conrad Cunningham},
            pdfborder={0 0 0},
            breaklinks=true}
\urlstyle{same}  % don't use monospace font for urls
\usepackage{color}
\usepackage{fancyvrb}
\newcommand{\VerbBar}{|}
\newcommand{\VERB}{\Verb[commandchars=\\\{\}]}
\DefineVerbatimEnvironment{Highlighting}{Verbatim}{commandchars=\\\{\}}
% Add ',fontsize=\small' for more characters per line
\newenvironment{Shaded}{}{}
\newcommand{\KeywordTok}[1]{\textcolor[rgb]{0.00,0.44,0.13}{\textbf{#1}}}
\newcommand{\DataTypeTok}[1]{\textcolor[rgb]{0.56,0.13,0.00}{#1}}
\newcommand{\DecValTok}[1]{\textcolor[rgb]{0.25,0.63,0.44}{#1}}
\newcommand{\BaseNTok}[1]{\textcolor[rgb]{0.25,0.63,0.44}{#1}}
\newcommand{\FloatTok}[1]{\textcolor[rgb]{0.25,0.63,0.44}{#1}}
\newcommand{\ConstantTok}[1]{\textcolor[rgb]{0.53,0.00,0.00}{#1}}
\newcommand{\CharTok}[1]{\textcolor[rgb]{0.25,0.44,0.63}{#1}}
\newcommand{\SpecialCharTok}[1]{\textcolor[rgb]{0.25,0.44,0.63}{#1}}
\newcommand{\StringTok}[1]{\textcolor[rgb]{0.25,0.44,0.63}{#1}}
\newcommand{\VerbatimStringTok}[1]{\textcolor[rgb]{0.25,0.44,0.63}{#1}}
\newcommand{\SpecialStringTok}[1]{\textcolor[rgb]{0.73,0.40,0.53}{#1}}
\newcommand{\ImportTok}[1]{#1}
\newcommand{\CommentTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textit{#1}}}
\newcommand{\DocumentationTok}[1]{\textcolor[rgb]{0.73,0.13,0.13}{\textit{#1}}}
\newcommand{\AnnotationTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textbf{\textit{#1}}}}
\newcommand{\CommentVarTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textbf{\textit{#1}}}}
\newcommand{\OtherTok}[1]{\textcolor[rgb]{0.00,0.44,0.13}{#1}}
\newcommand{\FunctionTok}[1]{\textcolor[rgb]{0.02,0.16,0.49}{#1}}
\newcommand{\VariableTok}[1]{\textcolor[rgb]{0.10,0.09,0.49}{#1}}
\newcommand{\ControlFlowTok}[1]{\textcolor[rgb]{0.00,0.44,0.13}{\textbf{#1}}}
\newcommand{\OperatorTok}[1]{\textcolor[rgb]{0.40,0.40,0.40}{#1}}
\newcommand{\BuiltInTok}[1]{#1}
\newcommand{\ExtensionTok}[1]{#1}
\newcommand{\PreprocessorTok}[1]{\textcolor[rgb]{0.74,0.48,0.00}{#1}}
\newcommand{\AttributeTok}[1]{\textcolor[rgb]{0.49,0.56,0.16}{#1}}
\newcommand{\RegionMarkerTok}[1]{#1}
\newcommand{\InformationTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textbf{\textit{#1}}}}
\newcommand{\WarningTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textbf{\textit{#1}}}}
\newcommand{\AlertTok}[1]{\textcolor[rgb]{1.00,0.00,0.00}{\textbf{#1}}}
\newcommand{\ErrorTok}[1]{\textcolor[rgb]{1.00,0.00,0.00}{\textbf{#1}}}
\newcommand{\NormalTok}[1]{#1}
\IfFileExists{parskip.sty}{%
\usepackage{parskip}
}{% else
\setlength{\parindent}{0pt}
\setlength{\parskip}{6pt plus 2pt minus 1pt}
}
\setlength{\emergencystretch}{3em}  % prevent overfull lines
\providecommand{\tightlist}{%
  \setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}}
\setcounter{secnumdepth}{0}
% Redefines (sub)paragraphs to behave more like sections
\ifx\paragraph\undefined\else
\let\oldparagraph\paragraph
\renewcommand{\paragraph}[1]{\oldparagraph{#1}\mbox{}}
\fi
\ifx\subparagraph\undefined\else
\let\oldsubparagraph\subparagraph
\renewcommand{\subparagraph}[1]{\oldsubparagraph{#1}\mbox{}}
\fi

% set default figure placement to htbp
\makeatletter
\def\fps@figure{htbp}
\makeatother

\usepackage{caption}
\DeclareCaptionLabelFormat{nolabel}{}
\captionsetup{labelformat=nolabel}

\title{CSci 450: Org. of Programming Languages\\
Labeled Digraph ADT in Haskell}
\author{H. Conrad Cunningham}
\date{27 October 2017}

\begin{document}
\maketitle

{
\setcounter{tocdepth}{4}
\tableofcontents
}
Copyright (C) 2017, H. Conrad Cunningham

\textbf{Advisory}: The HTML version of this document may require use of
a browser that supports the display of MathML. A good choice as of
October 2017 is a recent version of Firefox from Mozilla.

TODO:

\begin{itemize}
\tightlist
\item
  Better motivate the ADT
\item
  Better integrate this case study into the evolving textbook
\item
  Add student outcomes, exercises, better references, etc.
\end{itemize}

\section{Labeled Digraph ADT in
Haskell}\label{labeled-digraph-adt-in-haskell}

\subsection{Introduction}\label{introduction}

In this case study, we seek to develop a family of graph data structures
that can support the implementation of Adventure games similar to the
Wizard's Adventure game given in Chapter 5 of the book \emph{Land of
Lisp: Learn to Program in Lisp, One Game at a Time} {[}Barski 2011{]}.
We develop this family as an abstract data type and implement it as
modules in Haskell.

This abstract data type represents \emph{doubly labeled directed
graphs}. A directed graph (digraph) includes vertices (nodes) and edges
directed from one node to another. The graph allows arbitrary data
(i.e., labels) to be attached to both vertices and edges in the directed
graph.

Note: In this case study we use the acronym \emph{ADT} to refer to an
\emph{abstract data type}. We also use an \emph{algebraic data type} to
denote the graph type provided by a Haskell module and perhaps use other
algebraic data types in implementing the module.

The objectives of this case study are to:

\begin{enumerate}
\def\labelenumi{\alph{enumi}.}
\item
  specify a Labeled Digraph abstract data type using a constructive
  model (sets and interface invariant for the,
  preconditions/postconditions for each operation)
\item
  implement the abstract data type as a module in Haskell with at least
  two distinct implementations, giving appropriate implementation
  invariants for each
\end{enumerate}

One source of information on digraphs and their specification we
referenced is Chapter 10 of the book \emph{Abstract Data Types:
Specifications, Implementations, and Applications} {[}Dale-Walker
1996{]}.

\subsection{Specification}\label{specification}

\subsubsection{Notation}\label{notation}

We use the following notation and terminology to describe the abstract
data type's model and its semantics. (We choose notation that can
readily be used in comments in the Haskell program.)

\begin{itemize}
\item
  \texttt{(ForAll\ x,\ y\ ::\ p(x,y))} is true if and only if predicate
  \texttt{p(x,y)} is true for all values of \texttt{x} and \texttt{y}.
\item
  \texttt{(Exists\ x,\ y\ ::\ p(x,y))} is true if and only if there is
  at least one pair of values \texttt{x} and \texttt{y} for which
  \texttt{p(x,y)} is true.
\item
  \texttt{(\#\ x,\ y\ ::\ p(x,y))} yields a count of pairs
  \texttt{(x,y)} for which \texttt{p(x,y)} is true.
\item
  \texttt{\textless{}=\textgreater{}} denotes logical equivalence.
  \texttt{p\ \textless{}=\textgreater{}\ q} is true if and only if the
  logical (Boolean) values \texttt{p} and \texttt{q} are equal (i.e.,
  both true or both false).
\item
  \texttt{x\ IN\ C} is true if and only if value \texttt{x} is member of
  a collection \texttt{C} (such as a set, bag, or sequence). Similarly,
  \texttt{x\ NOT\_IN\ C} denotes the negation of \texttt{x\ IN\ C}.
\item
  A type consists of a set of values and a set of operations. We
  sometimes say a value is \texttt{IN} a type to mean the value is
  \texttt{IN} the set associated with the type.
\item
  For sets \texttt{C} and \texttt{D}, \texttt{C\ UNION\ D} denotes set
  union, that is, a set that includes all the element of both \texttt{C}
  and \texttt{D}.
\item
  For sets \texttt{C} and \texttt{D}, \texttt{C\ INTERSECT\ D} denotes
  set intersection, that is, a set that includes all elements that are
  both in \texttt{C} and in \texttt{D}.
\item
  For sets \texttt{C} and \texttt{D}, \texttt{C\ -\ D} denotes set
  difference, that is, the set \texttt{C} with all elements of set
  \texttt{D} removed.
\item
  For sets \texttt{C} and \texttt{D}, \texttt{C\ SUBSET\_OF\ D} denotes
  that \texttt{C} is subset of \texttt{D}, that is, all the elements of
  \texttt{C} also occur in \texttt{D}.
\item
  A tuple such as \texttt{(x,*)} appearing in a collection such as
  \texttt{\{\ (x,*)\ \}} denotes element \texttt{x} grouped with all
  possible values of the second component. Note: We could also write
  \texttt{\{\ (x,*)\ \}} using q quantification as:

\begin{verbatim}
{ (x,c) :: c IN some_domain }
\end{verbatim}
\item
  A \emph{function} is a special case of a \emph{relation} and relation
  is a set of ordered pairs (tuples). We sometimes manipulate functions
  or relations using set notation for convenience.
\item
  A \emph{total function} is defined for all elements of its domain. A
  \emph{partial function} is defined for a subset of the elements of its
  domain.
\end{itemize}

\subsubsection{Abstract model}\label{abstract-model}

We parameterize the abstract model for the Labeled Digraph ADT with the
following types.

\begin{itemize}
\item
  \texttt{VertexType} is the set of possible vertices (i.e., vertex
  identifiers).
\item
  \texttt{VertexLabelType} is the set of possible labels on vertices.
  (Values of this type may have several components.)
\item
  \texttt{EdgeLabelType} is the set of possible labels on edges. (Values
  of this type may have several components.)
\end{itemize}

We model the state of the instance of the Labeled Digraph ADT with an
abstract value \texttt{G} such that \texttt{G\ =\ (V,E,VL,EL)} with
\texttt{G}'s components satisfying the following \emph{Labeled Digraph
Properties}.

\begin{itemize}
\item
  \texttt{V} is a finite subset of values from the set
  \texttt{VertexType}. \texttt{V} denotes the vertices (or nodes) of the
  digraph.
\item
  \texttt{E} is a binary relation on the set \texttt{V}. A pair
  \texttt{(v1,v2)\ IN\ E} denotes that there is a directed edge from
  \texttt{v1} to \texttt{v2} in the digraph.

  Note that this model allows at most one (directed) edge from a vertex
  \texttt{v1} to vertex \texttt{v2}.
\item
  \texttt{VL} is a total function from set \texttt{V} to the set
  \texttt{VertexLabelType}.
\item
  \texttt{EL} is a total function from set \texttt{E} to the set
  \texttt{EdgeLabelType}.
\end{itemize}

\subsubsection{Interface invariant}\label{interface-invariant}

We define the following interface invariant for the Labeled Digraph ADT:

\begin{quote}
\emph{Any valid labeled digraph instance \texttt{G}, appearing in either
the arguments or return value of a public ADT operation, must satisfy
the Labeled Digraph Properties.}
\end{quote}

\subsubsection{Constructive semantics}\label{constructive-semantics}

We specify the various ADT operations below using their type signatures,
preconditions, and postconditions. Along with the interface invariant,
these comprise the (implementation-independent) specification of the
ADT.

In these assertions, for a digraph \texttt{g} that satisfies the
invariants, \texttt{G(g)} denotes its abstract model\texttt{(V,E,VL,EL)}
as described above. The value \texttt{Result} denotes the return value
of function.

\begin{itemize}
\item
  Constructor \texttt{new\_graph} creates and returns a new instance of
  the graph ADT.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
True
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
G(Result) == ({},{},{},{})
\end{verbatim}
  \end{itemize}
\item
  Accessor \texttt{is\_empty\ g} returns true if and only if graph
  \texttt{g} is empty.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(g) = (V,E,VL,EL)
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
Result == (V == {} && E == {})
\end{verbatim}
  \end{itemize}
\item
  Mutator \texttt{add\_vertex\ g\ nv\ nl} inserts vertex \texttt{nv}
  with label \texttt{nl} into graph \texttt{g} and returns the resulting
  graph.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(g) = (V,E,VL,EL) && nv NOT_IN V
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
G(Result) == (V UNION {nv}, E, VL UNION {(nv,nl)}, EL)
\end{verbatim}
  \end{itemize}
\item
  Mutator \texttt{remove\_vertex\ g\ ov} deletes vertex \texttt{ov} from
  graph \texttt{g} and returns the resulting graph.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(g) =  (V,E,VL,EL) && ov IN V
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
G(Result) == (V', E', VL', EL') 
    where V'  = V  - {ov}
          E'  = E  - {(ov,*),(*,ov)}
          VL' = VL - {(ov,*)}
          EL' = EL - {((ov,*),*),((*,ov),*)}
\end{verbatim}
  \end{itemize}
\item
  Mutator \texttt{update\_vertex\ g\ ov\ nl} changes the label on vertex
  \texttt{ov} in graph \texttt{g} to be \texttt{nl} and returns the
  resulting graph.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(g) =  (V,E,VL,EL) && ov IN V 
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
G(Result) == (V - {ov}, E, VL', EL) 
    where VL' = (VL - {(ov,VL(ov))}) UNION {(ov,nl)}
\end{verbatim}
  \end{itemize}
\item
  Accessor \texttt{get\_vertex\ g\ ov} returns the label from vertex
  \texttt{ov} in graph \texttt{g}

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(g) = (V,E,VL,EL) && ov IN V 
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
Result == VL(ov) 
\end{verbatim}
  \end{itemize}
\item
  Accessor \texttt{has\_vertex\ g\ ov} returns true if and only if
  \texttt{ov} is a vertex of graph \texttt{g}.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(g) = (V,E,VL,EL) && ov IN VertexLabelType 
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
G(Result) == ov IN V 
\end{verbatim}
  \end{itemize}
\item
  Mutator \texttt{add\_edge\ g\ v1\ v2\ nl} inserts an edge from vertex
  \texttt{v1} to vertex \texttt{v2} in graph \texttt{g} and returns the
  resulting graph.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(g) = (V,E,VL,EL) && v1 IN V && v2 IN V && 
(v1,v2) NOT_IN E
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
G(Result) == (V, E', VL, EL') 
    where E'  = E  UNION {(v1,v2)}
          EL' = EL UNION {((v1,v2),nl)}
\end{verbatim}
  \end{itemize}
\item
  Mutator \texttt{remove\_edge\ g\ v1\ v2} deletes the edge from vertex
  \texttt{v1} to vertex \texttt{v2} from graph \texttt{g} and returns
  the resulting graph.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(g) =  (V,E,VL,EL) V - {ov} && (v1,v2) IN E
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
G(Result) == (V, E - {(v1,v2)}, VL, EL - { ((v1,v2),*) }
\end{verbatim}
  \end{itemize}
\item
  Mutator \texttt{update\_edge\ g\ v1\ v2\ nl} changes the label on the
  edge from vertex \texttt{v1} to vertex \texttt{v2} in graph \texttt{g}
  to have label \texttt{nl} and returns the resulting graph.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(g) = (V,E,VL,EL) && (v1,v2) IN E
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
G(Result) == (V, E, VL, EL') 
    where EL' == (EL - {((v1,v2),*)}) UNION {((v2,v2),nl) 
\end{verbatim}
  \end{itemize}
\item
  Accessor \texttt{get\_edge\ g\ v1\ v2} returns the label on the edge
  from vertex \texttt{v1} to vertex \texttt{v2} in graph \texttt{g}.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(g) = (V,E,VL,EL) && (v1,v2) IN E
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
Result == EL((v1,v2)) 
\end{verbatim}
  \end{itemize}
\item
  Accessor \texttt{has\_edge\ g\ v1\ v2} returns true if and only if
  there is an edge from a vertex \texttt{v1} to a vertex \texttt{v2} in
  graph \texttt{g}.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(g) = (V,E,VL,EL)
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
Result == (v1,v2) IN E 
\end{verbatim}
  \end{itemize}
\item
  Accessor \texttt{all\_vertices\ g} returns a sequence of all the
  vertices in graph \texttt{g}. The returned sequence is represented by
  a builtin Haskell list.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(g) = (V,E,VL,EL) 
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
(ForAll ov: ov IN Result <=> ov IN V) && 
length(Result) == size(V) 
\end{verbatim}
  \end{itemize}
\item
  Accessor \texttt{from\_edges\ g\ v1} returns a sequence of all
  vertices \texttt{v2} such that there is an edge from vertex
  \texttt{v1} to vertex \texttt{v2} in graph \texttt{g}. The returned
  sequence is represented by a builtin Haskell list.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(g) = (V,E,VL,EL) && v1 IN V 
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
(ForAll v2: v2 IN Result <=> (v1,v2) IN E) &&
length(Result) == (# v2 :: (v1,v2) IN E) 
\end{verbatim}
  \end{itemize}

  Function \texttt{from\_edges\ g\ v1} should return \texttt{{[}{]}}
  when \texttt{v1} does not appear in \texttt{g}, so that it can work
  well with the Wizard's Adventure game.
\item
  Accessor \texttt{all\_vertices\_labels\ g} returns a sequence of all
  pairs \texttt{(v,l)} such that \texttt{v} is a vertex and \texttt{l}
  is it's label in graph \texttt{g}. The returned sequence is
  represented by a builtin Haskell list.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(g) = (V,E,VL,EL)
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
(ForAll v, l: (v,l) IN Result <=> (v,l) IN VL) && 
length(Result) == size(VL) 
\end{verbatim}
  \end{itemize}
\item
  Accessor \texttt{from\_edges\_labels\ g\ v1} returns a sequence of all
  pairs \texttt{(v2,l)} such that there is an edge \texttt{(v1,v2)}
  labeled with \texttt{l} in graph \texttt{g}.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(g) = (V,E,VL,EL) && v1 IN V
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
(ForAll v2, l :: (v2,l) IN Result <=> ((v1,v2),l) IN EL) &&
length(Result) == (# v2 :: (v1,v2 ) IN E) 
\end{verbatim}
  \end{itemize}

  Function \texttt{from\_edges\_labels\ g\ v1} should return
  \texttt{{[}{]}} when \texttt{v1} does not appear in \texttt{g}, so
  that it can work well with the Wizard's Adventure game.
\end{itemize}

\subsubsection{Haskell module abstract
interface}\label{haskell-module-abstract-interface}

Below we state the header for a Haskell module \texttt{Digraph\_XXX}
that implements the Labeled Digraph ADT. The module name suffix
\texttt{XXX} denotes the particular implementation for a data
representation, but the signatures and semantics of the operations are
the same regardless of representation.

The module exports data type \texttt{Digraph}, but its constructors are
not exported. This allows modules that import \texttt{Digraph\_XXX} to
use the data type without revealing how the data type is implemented.
(If we had \texttt{Digraph(..)} in the export list, then the data type
and all its constructors would be exported.)

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{module} \DataTypeTok{DigraphADT_XXX} 
\NormalTok{      ( }\DataTypeTok{Digraph}             \CommentTok{-- constrain ops (Eq a, Show a, Show b, Show c) }
\NormalTok{      , new_graph           }\CommentTok{-- Digraph a b c }
\NormalTok{      , is_empty            }\CommentTok{-- Digraph a b c -> Bool }
\NormalTok{      , add_vertex          }\CommentTok{-- Digraph a b c -> a -> b -> Digraph a b c }
\NormalTok{      , remove_vertex       }\CommentTok{-- Digraph a b c -> a -> Digraph a b c }
\NormalTok{      , update_vertex       }\CommentTok{-- Digraph a b c -> a -> b -> Digraph a b c }
\NormalTok{      , get_vertex          }\CommentTok{-- Digraph a b c -> a -> b }
\NormalTok{      , has_vertex          }\CommentTok{-- Digraph a b c -> a -> Bool }
\NormalTok{      , add_edge            }\CommentTok{-- Digraph a b c -> a -> a -> c -> Digraph a b c }
\NormalTok{      , remove_edge         }\CommentTok{-- Digraph a b c -> a -> a -> Digraph a b c }
\NormalTok{      , update_edge         }\CommentTok{-- Digraph a b c -> a -> a -> c -> Digraph a b c }
\NormalTok{      , get_edge            }\CommentTok{-- Digraph a b c -> a -> a -> c }
\NormalTok{      , has_edge            }\CommentTok{-- Digraph a b c -> a -> a -> Bool }
\NormalTok{      , all_vertices        }\CommentTok{-- Digraph a b c -> [a]}
\NormalTok{      , from_edges          }\CommentTok{-- Digraph a b c -> a -> [a]}
\NormalTok{      , all_vertices_labels }\CommentTok{-- Digraph a b c -> [(a,b)]}
\NormalTok{      , from_edges_labels   }\CommentTok{-- Digraph a b c -> a -> [(a,c)]}
\NormalTok{      )}
    \KeywordTok{where}  \CommentTok{-- definitions for the types and functions}
\end{Highlighting}
\end{Shaded}

Note: The Glasgow Haskell Compiler (GHC) release 8.2 (July 2017) and the
Cabal-Install package manager release 2.0 (August 2017) support a new
mixin package system called Backpack. This extension would enable us to
define an abstract module ``DigraphADT'' as a signature file with the
above interface. Other modules can then implement this abstract
interface thus giving a more explicit and flexible definition of this
abstract data type.

\subsection{List Implementation}\label{list-implementation}

\subsubsection{Type parameters}\label{type-parameters}

The Haskell List representation uses the following values for the type
parameters:

\begin{itemize}
\item
  \texttt{VertexType} is an instance of Haskell classes \texttt{Eq} and
  \texttt{Show} (i.e., can be compared for equality and converted to
  strings),
\item
  \texttt{VertexLabelType} is an instance of Haskell class
  \texttt{Show},
\item
  \texttt{EdgeLabelType} is an instance of Haskell class \texttt{Show}.
\end{itemize}

That is, vertices can be compared for equality. Vertices and both the
vertex and edge labels can be displayed as strings.

Note: It may be desirable to require \texttt{VertexType} to be from
class \texttt{Ord} (totally ordered) and \texttt{VertexLabelType} and
\texttt{EdgeLabelType} to be from class \texttt{Eq}. These were not
necessary for the List implementation, but were necessary for the Map
implementation.

\subsubsection{Labeled digraph
representation}\label{labeled-digraph-representation}

The List implementation represents a labeled digraph as an instance of
the Haskell algebraic data type \texttt{Digraph}, in particular data
constructor \texttt{(Graph\ vs\ es)}.

In an instance \texttt{(Graph\ vs\ es)}:

\begin{itemize}
\item
  \texttt{vs} is a list of tuples \texttt{(v,vl)} where

  \begin{itemize}
  \tightlist
  \item
    \texttt{v} has \texttt{VertexType} and represents a vertex of the
    digraph
  \item
    \texttt{vl} has \texttt{VertexLabelType} and is the unique label
    associated with vertex \texttt{v}
  \item
    a vertex \texttt{v} occurs at most once in \texttt{vs} (i.e., vs
    encodes a function from vertices to vertex labels)
  \end{itemize}
\item
  \texttt{es} is a list of tuples \texttt{((v1,v2),el)} where

  \begin{itemize}
  \tightlist
  \item
    \texttt{v1} and \texttt{v2} are vertices occurring in \texttt{vs},
    representing a directed edge from \texttt{v1} to \texttt{v2}
  \item
    \texttt{el} has \texttt{EdgeLabelType} and is the unique label
    associated with edge \texttt{(v1,v2)}
  \item
    an edge \texttt{(v1,v2)} occurs at most once in \texttt{vs} (i.e.,
    es encodes a function from edges to edge labels)
  \end{itemize}
\end{itemize}

In terms of the abstract model, \texttt{vs} encodes \texttt{VL} directly
and, because \texttt{VL} is a total function on \texttt{V}, it encodes
\texttt{V} indirectly. Similarly, es encodes \texttt{EL} directly and
\texttt{E} indirectly.

\subsubsection{Implementation invariant}\label{implementation-invariant}

Given the above description, we then define the following implementation
(representation) invariant for the list-based version of the Labeled
Digraph ADT:

\begin{quote}
\emph{Any Haskell \texttt{Digraph} value \texttt{(Graph\ vs\ es)} with
abstract model \texttt{G\ =\ (V,E,VL,EL)}, appearing in either the
arguments or return value of an operation, must also satisfy the
following:}
\end{quote}

\begin{verbatim}
    (ForAll v, l :: (v,l) IN vs  <=> (v,l) IN VL ) &&
    (ForAll v1, v2, m :: (v1,v2,m) IN es  <=> ((v1,v2),m) IN EL )
\end{verbatim}

\subsubsection{Haskell module}\label{haskell-module}

The Haskell module for the list representation of the labeled digraph
graph ADT is in \href{DigraphADT_List.hs}{file
\texttt{DigraphADT\_List.hs}}. Its test driver module is in
\href{DigraphADT_TestList.hs\%3E}{file
\texttt{DigraphADT\_TestList.hs}}.

\subsection{Map Implementation}\label{map-implementation}

\subsubsection{Type parameters}\label{type-parameters-1}

The Haskell Map representation uses the following values for the type
parameters:

\begin{itemize}
\item
  \texttt{VertexType} is an instance of Haskell classes \texttt{Ord} and
  Show (i.e., can be compared and also converted to strings)
\item
  \texttt{VertexLabelType} is an instance of Haskell classes \texttt{Eq}
  and \texttt{Show}.
\item
  \texttt{EdgeLabelType} is an instance of Haskell classes \texttt{Eq}
  and \texttt{Show}.
\end{itemize}

Note: In the List version of this ADT, \texttt{VertexType} is required
to be in classes \texttt{Show} and \texttt{Eq} (instead of
\texttt{Ord}). The two label types did not require \texttt{Eq}. However,
the use of the Map module for implementation in this version requires
the new type constraints.

\subsubsection{Labeled digraph
representation}\label{labeled-digraph-representation-1}

This implementation represents a labeled digraph as an instance of the
Haskell algebraic data type \texttt{Digraph}, in particular data
constructor \texttt{(Graph\ m)}, where \texttt{m} is from the
\texttt{Data.Map.Strict} collection. (This collection is implemented as
a balanced tree.)

An instance of \texttt{(Graph\ m)} corresponds to the abstract model as
follows:

\begin{itemize}
\item
  The keys for \texttt{Map\ m} are from \texttt{VertexLabelType}.
\item
  \texttt{Map\ m} is defined for all keys \texttt{v1} in vertex set
  \texttt{V} and undefined for all other keys.
\item
  For some vertex \texttt{v1}, the value of \texttt{m} at key
  \texttt{v1} is a pair \texttt{(l,es)} where
\item
  \texttt{l} is an element of \texttt{VertexLabelType} and is the unique
  label associated with \texttt{v1}, that is, \texttt{l\ =\ VL(v1)}.

  \begin{itemize}
  \tightlist
  \item
    \texttt{es} is the list of all tuples \texttt{(v2,el)} such that
    \texttt{(v1,v2)\ IN\ E}, \texttt{el\ IN\ EdgeLabelType}, and
    \texttt{el\ =\ EL((v1,v2))}. That is, \texttt{(v1,v2)} is an edge
    and \texttt{el} is its unique label.
  \end{itemize}
\end{itemize}

\subsubsection{Implementation
invariant}\label{implementation-invariant-1}

Given the above description, we then define the following implementation
(representation) invariant for the list-based version of the Labeled
Digraph ADT:

\begin{quote}
\emph{Any Haskell \texttt{Digraph} value \texttt{(Graph\ m)} with
abstract model \texttt{G\ =\ (V,E,VL,EL)}, appearing in either the
arguments or return value of an operation, must also satisfy the
following:}
\end{quote}

\begin{verbatim}
    (ForAll v1, l, es :: 
        ( m(v1) defined && m(v1) == (l,es) ) <=> 
        ( VL(v1) == l && 
            (ForAll v2, el :: (v2,el) IN es <=> 
                              EL((v1,v2)) == el) ) )
\end{verbatim}

\subsubsection{Haskell module}\label{haskell-module-1}

The Haskell module for the Map representation of the labeled digraph
graph ADT is in \href{DigraphADT_Map.hs}{file
\texttt{DigraphADT\_Map.hs}}. Its test driver module is in
\href{DigraphADT_TestMap.hs\%3E}{file \texttt{DigraphADT\_TestMap.hs}}.

\subsection{Acknowledgements}\label{acknowledgements}

In Spring 2017, I adapted and revised this document from comments in my
Spring 2015 Haskell implementations of the Labeled Digraph abstract data
type. (In addition to the list- and map-based Haskell implementations, I
also developed a list-based implementation in Elixir in Spring 2015 and
two Scala-based implementations in Spring 2016.)

In Summer and Fall 2017, I continue to revise this document. I plan
eventually to integrate it into evolving textbook ``Introduction to
Functional Programming Using Haskell.''

I maintain these notes as text in Pandoc's dialect of Markdown using
embedded LaTeX markup for the mathematical formulas and then translate
the notes to HTML, PDF, and other forms as needed. The HTML version of
this document requires use of a browser that supports the display of
MathML.

\subsection{References}\label{references}

\begin{description}
\tightlist
\item[{[}Barski 2011{]}]
Conrad Barski. ``Building a Text Game Engine,'' \emph{Land of Lisp:
Learn to Program in Lisp, One Game at a Time}, pp.~69-84, No Starch
Press, 2011. (The Common Lisp example in this chapter is similar to the
classic Adventure game; the underlying data structure is a labeled
digraph.)
\item[{[}Bird-Wadler 1998{]}]
Richard Bird and Philip Wadler. \emph{Introduction to Functional
Programming}, Second Edition, Addison Wesley, 1998.
{[}\href{https://usi-pl.github.io/lc/sp-2015/doc/Bird_Wadler.\%20Introduction\%20to\%20Functional\%20Programming.1ed.pdf}{First
Edition, 1988}{]}
\item[{[}Cunningham 2017{]}]
H. Conrad Cunningham. \href{../../DataAbstraction.html}{\emph{Notes on
Data Abstraction}}, 1996-2017.
\item[{[}Dale-Walker 1996{]}]
Nell Dale and Henry M. Walker. ``Directed Graphs or Digraphs,'' Chapter
10, In \emph{Abstract Data Types: Specifications, Implementations, and
Applications}, pp.~439-469, D. C. Heath \& Co, 1996.
\end{description}

\subsection{Terms and Concepts}\label{terms-and-concepts}

Use of Haskell module hiding features to implement the abstract data
type's interface, applying specification concepts, using mathematical
concepts to model the data abstraction (graphs, sets, sequences, bags,
functions, relations), graph data structure.

The specification model for the abstract data type uses a constructive
semantics -- an abstract model, invariants, preconditions, and
postconditions.

\end{document}