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:

Better motivate the ADT
Better integrate this case study into the evolving textbook
Add student outcomes, exercises, better references, etc.

Labeled Digraph ADT in Haskell

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 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 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 ADT to refer to an abstract data type. We also use an 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:

specify a Labeled Digraph abstract data type using a constructive model (sets and interface invariant for the, preconditions/postconditions for each operation)
implement the abstract data type as a module in Haskell with at least two distinct implementations, giving appropriate implementation invariants for each

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

Specification

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.)

(ForAll x, y :: p(x,y)) is true if and only if predicate p(x,y) is true for all values of x and y.
(Exists x, y :: p(x,y)) is true if and only if there is at least one pair of values x and y for which p(x,y) is true.
(# x, y :: p(x,y)) yields a count of pairs (x,y) for which p(x,y) is true.
<=> denotes logical equivalence. p <=> q is true if and only if the logical (Boolean) values p and q are equal (i.e., both true or both false).
x IN C is true if and only if value x is member of a collection C (such as a set, bag, or sequence). Similarly, x NOT_IN C denotes the negation of x IN C.
A type consists of a set of values and a set of operations. We sometimes say a value is IN a type to mean the value is IN the set associated with the type.
For sets C and D, C UNION D denotes set union, that is, a set that includes all the element of both C and D.
For sets C and D, C INTERSECT D denotes set intersection, that is, a set that includes all elements that are both in C and in D.
For sets C and D, C - D denotes set difference, that is, the set C with all elements of set D removed.
For sets C and D, C SUBSET_OF D denotes that C is subset of D, that is, all the elements of C also occur in D.
A tuple such as (x,*) appearing in a collection such as { (x,*) } denotes element x grouped with all possible values of the second component. Note: We could also write { (x,*) } using q quantification as:
```
{ (x,c) :: c IN some_domain }
```
A function is a special case of a relation and relation is a set of ordered pairs (tuples). We sometimes manipulate functions or relations using set notation for convenience.
A total function is defined for all elements of its domain. A partial function is defined for a subset of the elements of its domain.

Abstract model

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

VertexType is the set of possible vertices (i.e., vertex identifiers).
VertexLabelType is the set of possible labels on vertices. (Values of this type may have several components.)
EdgeLabelType is the set of possible labels on edges. (Values of this type may have several components.)

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

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

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

Interface invariant

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

Any valid labeled digraph instance G, appearing in either the arguments or return value of a public ADT operation, must satisfy the Labeled Digraph Properties.

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 g that satisfies the invariants, G(g) denotes its abstract model(V,E,VL,EL) as described above. The value Result denotes the return value of function.

Constructor new_graph creates and returns a new instance of the graph ADT.
- Precondition:
```
True
```
- Postcondition:
```
G(Result) == ({},{},{},{})
```
Accessor is_empty g returns true if and only if graph g is empty.
- Precondition:
```
G(g) = (V,E,VL,EL)
```
- Postcondition:
```
Result == (V == {} && E == {})
```
Mutator add_vertex g nv nl inserts vertex nv with label nl into graph g and returns the resulting graph.
- Precondition:
```
G(g) = (V,E,VL,EL) && nv NOT_IN V
```
- Postcondition:
```
G(Result) == (V UNION {nv}, E, VL UNION {(nv,nl)}, EL)
```

Mutator remove_vertex g ov deletes vertex ov from graph g and returns the resulting graph.

Precondition:
```
G(g) =  (V,E,VL,EL) && ov IN V
```

Postcondition:

G(Result) == (V', E', VL', EL') 
    where V'  = V  - {ov}
          E'  = E  - {(ov,*),(*,ov)}
          VL' = VL - {(ov,*)}
          EL' = EL - {((ov,*),*),((*,ov),*)}

Mutator update_vertex g ov nl changes the label on vertex ov in graph g to be nl and returns the resulting graph.
- Precondition:
```
G(g) =  (V,E,VL,EL) && ov IN V 
```
- Postcondition:
```
G(Result) == (V - {ov}, E, VL', EL) 
    where VL' = (VL - {(ov,VL(ov))}) UNION {(ov,nl)}
```
Accessor get_vertex g ov returns the label from vertex ov in graph g
- Precondition:
```
G(g) = (V,E,VL,EL) && ov IN V 
```
- Postcondition:
```
Result == VL(ov) 
```
Accessor has_vertex g ov returns true if and only if ov is a vertex of graph g.
- Precondition:
```
G(g) = (V,E,VL,EL) && ov IN VertexLabelType 
```
- Postcondition:
```
G(Result) == ov IN V 
```

Mutator add_edge g v1 v2 nl inserts an edge from vertex v1 to vertex v2 in graph g and returns the resulting graph.

Precondition:

G(g) = (V,E,VL,EL) && v1 IN V && v2 IN V && 
(v1,v2) NOT_IN E

Postcondition:

G(Result) == (V, E', VL, EL') 
    where E'  = E  UNION {(v1,v2)}
          EL' = EL UNION {((v1,v2),nl)}

Mutator remove_edge g v1 v2 deletes the edge from vertex v1 to vertex v2 from graph g and returns the resulting graph.
- Precondition:
```
G(g) =  (V,E,VL,EL) V - {ov} && (v1,v2) IN E
```
- Postcondition:
```
G(Result) == (V, E - {(v1,v2)}, VL, EL - { ((v1,v2),*) }
```
Mutator update_edge g v1 v2 nl changes the label on the edge from vertex v1 to vertex v2 in graph g to have label nl and returns the resulting graph.
- Precondition:
```
G(g) = (V,E,VL,EL) && (v1,v2) IN E
```
- Postcondition:
```
G(Result) == (V, E, VL, EL') 
    where EL' == (EL - {((v1,v2),*)}) UNION {((v2,v2),nl) 
```
Accessor get_edge g v1 v2 returns the label on the edge from vertex v1 to vertex v2 in graph g.
- Precondition:
```
G(g) = (V,E,VL,EL) && (v1,v2) IN E
```
- Postcondition:
```
Result == EL((v1,v2)) 
```
Accessor has_edge g v1 v2 returns true if and only if there is an edge from a vertex v1 to a vertex v2 in graph g.
- Precondition:
```
G(g) = (V,E,VL,EL)
```
- Postcondition:
```
Result == (v1,v2) IN E 
```
Accessor all_vertices g returns a sequence of all the vertices in graph g. The returned sequence is represented by a builtin Haskell list.
- Precondition:
```
G(g) = (V,E,VL,EL) 
```
- Postcondition:
```
(ForAll ov: ov IN Result <=> ov IN V) && 
length(Result) == size(V) 
```
Accessor from_edges g v1 returns a sequence of all vertices v2 such that there is an edge from vertex v1 to vertex v2 in graph g. The returned sequence is represented by a builtin Haskell list.
- Precondition:
```
G(g) = (V,E,VL,EL) && v1 IN V 
```
- Postcondition:
```
(ForAll v2: v2 IN Result <=> (v1,v2) IN E) &&
length(Result) == (# v2 :: (v1,v2) IN E) 
```
Function from_edges g v1 should return [] when v1 does not appear in g, so that it can work well with the Wizard's Adventure game.
Accessor all_vertices_labels g returns a sequence of all pairs (v,l) such that v is a vertex and l is it's label in graph g. The returned sequence is represented by a builtin Haskell list.
- Precondition:
```
G(g) = (V,E,VL,EL)
```
- Postcondition:
```
(ForAll v, l: (v,l) IN Result <=> (v,l) IN VL) && 
length(Result) == size(VL) 
```
Accessor from_edges_labels g v1 returns a sequence of all pairs (v2,l) such that there is an edge (v1,v2) labeled with l in graph g.
- Precondition:
```
G(g) = (V,E,VL,EL) && v1 IN V
```
- Postcondition:
```
(ForAll v2, l :: (v2,l) IN Result <=> ((v1,v2),l) IN EL) &&
length(Result) == (# v2 :: (v1,v2 ) IN E) 
```
Function from_edges_labels g v1 should return [] when v1 does not appear in g, so that it can work well with the Wizard's Adventure game.

Haskell module abstract interface

Below we state the header for a Haskell module Digraph_XXX that implements the Labeled Digraph ADT. The module name suffix 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 Digraph, but its constructors are not exported. This allows modules that import Digraph_XXX to use the data type without revealing how the data type is implemented. (If we had Digraph(..) in the export list, then the data type and all its constructors would be exported.)

    module DigraphADT_XXX 
      ( Digraph             -- constrain ops (Eq a, Show a, Show b, Show c) 
      , new_graph           -- Digraph a b c 
      , is_empty            -- Digraph a b c -> Bool 
      , add_vertex          -- Digraph a b c -> a -> b -> Digraph a b c 
      , remove_vertex       -- Digraph a b c -> a -> Digraph a b c 
      , update_vertex       -- Digraph a b c -> a -> b -> Digraph a b c 
      , get_vertex          -- Digraph a b c -> a -> b 
      , has_vertex          -- Digraph a b c -> a -> Bool 
      , add_edge            -- Digraph a b c -> a -> a -> c -> Digraph a b c 
      , remove_edge         -- Digraph a b c -> a -> a -> Digraph a b c 
      , update_edge         -- Digraph a b c -> a -> a -> c -> Digraph a b c 
      , get_edge            -- Digraph a b c -> a -> a -> c 
      , has_edge            -- Digraph a b c -> a -> a -> Bool 
      , all_vertices        -- Digraph a b c -> [a]
      , from_edges          -- Digraph a b c -> a -> [a]
      , all_vertices_labels -- Digraph a b c -> [(a,b)]
      , from_edges_labels   -- Digraph a b c -> a -> [(a,c)]
      )
    where  -- definitions for the types and functions

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.

List Implementation

Type parameters

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

VertexType is an instance of Haskell classes Eq and Show (i.e., can be compared for equality and converted to strings),
VertexLabelType is an instance of Haskell class Show,
EdgeLabelType is an instance of Haskell class Show.

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 VertexType to be from class Ord (totally ordered) and VertexLabelType and EdgeLabelType to be from class Eq. These were not necessary for the List implementation, but were necessary for the Map implementation.

Labeled digraph representation

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

In an instance (Graph vs es):

vs is a list of tuples (v,vl) where
- v has VertexType and represents a vertex of the digraph
- vl has VertexLabelType and is the unique label associated with vertex v
- a vertex v occurs at most once in vs (i.e., vs encodes a function from vertices to vertex labels)
es is a list of tuples ((v1,v2),el) where
- v1 and v2 are vertices occurring in vs, representing a directed edge from v1 to v2
- el has EdgeLabelType and is the unique label associated with edge (v1,v2)
- an edge (v1,v2) occurs at most once in vs (i.e., es encodes a function from edges to edge labels)

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

Implementation invariant

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

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

    (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 )

Haskell module

The Haskell module for the list representation of the labeled digraph graph ADT is in file DigraphADT_List.hs. Its test driver module is in file DigraphADT_TestList.hs.

Map Implementation

Type parameters

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

VertexType is an instance of Haskell classes Ord and Show (i.e., can be compared and also converted to strings)
VertexLabelType is an instance of Haskell classes Eq and Show.
EdgeLabelType is an instance of Haskell classes Eq and Show.

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

Labeled digraph representation

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

An instance of (Graph m) corresponds to the abstract model as follows:

The keys for Map m are from VertexLabelType.
Map m is defined for all keys v1 in vertex set V and undefined for all other keys.
For some vertex v1, the value of m at key v1 is a pair (l,es) where
l is an element of VertexLabelType and is the unique label associated with v1, that is, l = VL(v1).
- es is the list of all tuples (v2,el) such that (v1,v2) IN E, el IN EdgeLabelType, and el = EL((v1,v2)). That is, (v1,v2) is an edge and el is its unique 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:

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

    (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) ) )

Haskell module

The Haskell module for the Map representation of the labeled digraph graph ADT is in file DigraphADT_Map.hs. Its test driver module is in file DigraphADT_TestMap.hs.

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.

References

[Barski 2011]: Conrad Barski. "Building a Text Game Engine," 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.)
[Bird-Wadler 1998]: Richard Bird and Philip Wadler. Introduction to Functional Programming, Second Edition, Addison Wesley, 1998. [First Edition, 1988]
[Cunningham 2017]: H. Conrad Cunningham. Notes on Data Abstraction, 1996-2017.
[Dale-Walker 1996]: Nell Dale and Henry M. Walker. "Directed Graphs or Digraphs," Chapter 10, In Abstract Data Types: Specifications, Implementations, and Applications, pp. 439-469, D. C. Heath & Co, 1996.

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.

CSci 450: Org. of Programming Languages
Labeled Digraph ADT in Haskell

H. Conrad Cunningham

27 October 2017

Labeled Digraph ADT in Haskell

Introduction

Specification

Notation

Abstract model

Interface invariant

Constructive semantics

Haskell module abstract interface

List Implementation

Type parameters

Labeled digraph representation

Implementation invariant

Haskell module

Map Implementation

Type parameters

Labeled digraph representation

Implementation invariant

Haskell module

Acknowledgements

References

Terms and Concepts

CSci 450: Org. of Programming Languages Labeled Digraph ADT in Haskell

H. Conrad Cunningham

27 October 2017

Labeled Digraph ADT in Haskell

Introduction

Specification

Notation

Abstract model

Interface invariant

Constructive semantics

Haskell module abstract interface

List Implementation

Type parameters

Labeled digraph representation

Implementation invariant

Haskell module

Map Implementation

Type parameters

Labeled digraph representation

Implementation invariant

Haskell module

Acknowledgements

References

Terms and Concepts

CSci 450: Org. of Programming Languages
Labeled Digraph ADT in Haskell