Verites / verigraph

Software specification and verification system based on graph rewriting
https://verites.github.io/verigraph/
Apache License 2.0
37 stars 4 forks source link

Make graph payloads mandatory #12

Closed ggazzi closed 7 years ago

ggazzi commented 7 years ago

Rationale

Currently, the payloads of graph nodes and edges are optional. That is, in a Graph n e, nodes contain payloads of type Maybe n and edges, of type Maybe e. There is currently, however, no use for these payloads in Verigraph, not even to allow metadata such as graph layout (since payloads are not handled and propagated by pullbacks, pushouts, overlappings and similar operations).

One of the possible uses would be to store attributes and typing information, which would reduce the number of dictionary lookups necessary to handle typed attributed graphs, simplifying code and improving performance. This, however, is not possible with optional payloads, since all nodes and edges need to have this information.

In order to allow this, graphs would need to have mandatory payloads. That is, in a Graph n e, nodes would contain payloads of type n and edges, of type e. Then, typed attributed graphs could be implemented simply as follows.

import qualified Graph as G

type AttributedGraph n e = 
  G.Graph (NodeType, Map AttrName AttrValue, n) (EdgeType, Map AttrName AttrValue, e)

type Node n =
  G.Node (NodeType, Map AttrName AttrValue, n)

type Edge e =
  G.Edge (EdgeType, Map AttrName AttrValue, e)

nodeType :: Node n -> NodeType
nodeType = fst . G.nodeInfo

edgeType :: Edge n -> EdgeType
edgeType = fst . G.edgeInfo

nodeInfo :: Node n -> n
nodeInfo = third . G.nodeInfo

edgeInfo :: Edge e -> e
edgeInfo = third . G.edgeInfo

This implementation pattern has the following advantages:

Proposed Changes

First, change the implementation of Graph so its has mandatory payloads. The impact of this change in the rest of Verigraph could be handled in two ways, based on Graph () () (unit-based) or on Graph (Maybe n) (Maybe e) (maybe-based).

Unit-Based Solution

Since no part of verigraph currently uses the payloads, they could be replaced with unit types whenever they are "ignored" by functions. We'd have, for example:

insertNode :: NodeId -> Graph () e -> Graph () e
insertNodeWithPayload :: NodeId -> n -> Graph n e -> Graph n e

instance Morphism (GraphMorphism () ())

instance Morphism (TypedGraphMorphism () ())

Maybe-Based Solution

Alternatively, we could displace the assumption of optional payloads to the function signature. That is, whenever Nothing is required to be a possible node payload, the type signature contains Graph (Maybe n) e (analogously for edges). We'd have, for example:

insertNode :: NodeId -> Graph (Maybe n) e -> Graph (Maybe n) e
insertNodeWithPayload :: NodeId -> n -> Graph n e -> Graph n e

instance Morphism (GraphMorphism (Maybe n) (Maybe e))

instance Morphism (TypedGraphMorphism (Maybe n) (Maybe e))
ggazzi commented 7 years ago

The Maybe-based solution interacts better with issue #13. Since the following instance exists, it would allow the use and propagation of metadata by the current implementation.

instance Monoid a => Monoid (Maybe a)
ggazzi commented 7 years ago

I'm choosing the Maybe-based solution because of issue #13.

ggazzi commented 7 years ago

Solved and merged to master.