Modeling heterogenous graphs in Haskell

Question

How can I model what I will call "heterogenous graphs" in haskell, such that the type-correctness of the graph can be verified at compile time?

For this purpose, a heterogenous graph is a set of nodes, each with a certain type label, and a set of edges, each with a source type label and a destination type label.

We wish to statically ensure that, when an edge is added to a graph, the source type label of that edge matches the type label of the source node, and the destination type label of that edge matches the type label of the destination node. But we don't wish to do that in the trivial way (by forcing the entire graph to contain only nodes with one particular type label).

Answer 1

I’m not sure how I would go about enforcing this at compile time—I think it requires that your graphs be completely static?—but it’s relatively straightforward to enforce at runtime using Typeable. Here’s a sketch of what that would look like. First, I’ll start with typed Node and Edge types:

data Node a = Node a
data Edge a b = Edge !Int !Int

Wrap them in existentials:

{-# LANGUAGE ExistentialQuantification #-}

import Data.Typeable

data SomeNode
  = forall a. (Typeable a)
  => SomeNode (Node a)

data SomeEdge
  = forall a b. (Typeable a, Typeable b)
  => SomeEdge (Edge a b)

Have a heterogeneous graph data type that uses the existentially quantified types:

import Data.IntMap (IntMap)

-- Not a great representation, but simple for illustration.
data Graph = Graph !(IntMap SomeNode) [SomeEdge]

And then operations that perform dynamic type checks:

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

import qualified Data.IntMap as IntMap

addNode
  :: forall a. (Typeable a)
  => Int -> a -> Graph -> Maybe Graph
addNode i x (Graph ns es) = case IntMap.lookup i ns of

  -- If a node already exists at a given index:
  Just (SomeNode (existing :: Node e)) -> case eqT @e @a of

    -- Type-preserving replacement is allowed, but…
    Just Refl -> Just $ Graph ns' es

    -- …*type-changing* replacement is *not* allowed,
    -- since it could invalidate existing edges.
    Nothing -> Nothing

  -- Insertion is of course allowed.
  Nothing -> Just $ Graph ns' es

  where
    ns' = IntMap.insert i (SomeNode (Node x)) ns

-- To add an edge:
addEdge
  :: forall a b. (Typeable a, Typeable b)
  => Edge a b -> Graph -> Maybe Graph
addEdge e@(Edge f t) (Graph ns es) = do

  -- The ‘from’ node must exist…
  SomeNode (fn :: Node tfn) <- IntMap.lookup f ns
  -- …and have the correct type; and
  Refl <- eqT @a @tfn

  -- The ‘to’ node must exist…
  SomeNode (tn :: Node ttn) <- IntMap.lookup t ns
  -- …and have the correct type.
  Refl <- eqT @b @ttn

  pure $ Graph ns $ SomeEdge e : es

Now this succeeds:

pure (Graph mempty mempty)
  >>= addNode 0 (1 :: Int)
  >>= addNode 1 ('x' :: Char)
  >>= addEdge (Edge 0 1 :: Edge Int Char)

But changing Int/Char in Edge Int Char to invalid types, or 0/1 to invalid indices, will fail and return Nothing.